From c8ee04268800a5b14dd565032dc969d7a2f621cc Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Fri, 4 Jul 2025 12:45:09 +1000
Subject: [PATCH] manual/README.md: include API doc generation

Migrate documentation of the API docs generation process here from the
docsite where it is too much out of view. Here it is closer to where it
is needed an more likely to get updated when things change.

Compared to the docsite version, this has applied:

- standard wrap column
- markdown lints
- adjusted headings
- `object-api-sel4-arch.xml` etc renames
- include RISC-V in structure

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 manual/README.md | 191 ++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 188 insertions(+), 3 deletions(-)

diff --git a/manual/README.md b/manual/README.md
index 01241c057..cc89b32c1 100644
--- a/manual/README.md
+++ b/manual/README.md
@@ -4,14 +4,199 @@
      SPDX-License-Identifier: CC-BY-SA-4.0
 -->
 
-seL4 Reference Manual
-=====================
+# seL4 Reference Manual
+
+## Build
 
 To build a PDF use
 
     make
 
-You will need recent version of `LaTeX` and `doxygen`.
+You will need recent version of `LaTeX` and `doxygen` as well as the seL4 python
+dependencies.
 
 The main source file is `manual.tex`, most of the text is in `parts/`,
 and most of the API reference is generated with `doxygen`.
+
+## API Generation
+
+The documentation of the seL4 API is automatically generated from
+comments in the source code. This section documents the process.
+
+### Types of API
+
+seL4 has two types of API, system calls and object invocations.
+
+- Top-level system calls are generally for message passing, for example `Call`,
+  `Send`, and `Recv`. In addition there are also debugging and benchmarking
+  system calls which can be enabled with a build flag.
+- Object invocations are regular message-passing system calls, usually `Call`,
+  where the recipient is effectively the kernel itself and the message encodes
+  some operation on a kernel object. Some examples are `TCB_Resume` and
+  `CNode_Copy`. Some kernel objects and object invocations are specific to a
+  particular processor architecture, for instance `X86_Page_Map`, and
+  `ARM_VCPU_InjectIrq`.
+
+Almost all system calls, including `Call`, `Send`, and `Recv`, are in fact
+object invocations under the hood, for instance on endpoint or notification
+objects -- they just provide a top-level API for message passing. The only
+"true" system calls are `Yield`, debug and benchmark operations.
+
+The API documentation in the manual is divided into the following hierarchy:
+
+- System Calls
+  - General System Calls
+  - Debugging System Calls
+  - Benchmarking System Calls
+- Architecture-Independent Object Methods
+- x86-Specific Object Methods
+  - General x86 Object Methods
+  - IA32 Object Methods
+  - x86_64 Object Methods
+- ARM-Specific Object Methods
+  - General ARM Object Methods
+  - aarch32 Object Methods
+  - aarch64 Object Methods
+- RISC-V-Specific Object Methods
+
+The process of generating API docs is different between System Calls and Object
+Invocations, though each process has some parts in common.
+
+### Common
+
+#### Approach
+
+Documentation for each seL4 API is written in the form of doxygen comments in C
+header files. The rest of the seL4 manual is written in LaTeX. To generate API
+documentation for the manual, we generate LaTeX files from doxygen comments
+which are then included in the manual.
+
+Rather than using doxygen's LaTeX output directly, we use doxygen to generate
+XML files. A custom script then parses the XML and produces the final LaTeX
+output. This is because we already have an established style for API
+documentation in our manual, and it was easier to generate LaTeX in this style
+ourselves from some simple (ie. easy to parse) intermediate format (ie. XML)
+rather than try to coerce doxygen into generating perfectly-styled LaTeX.
+
+The script that translates doxygen-generated xml into LaTeX is in:
+[manual/tools/parse_doxygen_xml.py](https://github.com/seL4/seL4/blob/master/manual/tools/parse_doxygen_xml.py).
+
+#### Custom Notation in Doxygen Comments
+
+Some parts of the API documentation reference other parts of the manual.
+Additionally, there are some custom formatting rules we'd like to apply to the
+API docs in the manual that aren't understood by doxygen. To achieve both these
+goals, we introduce some additional XML tags which we explicitly add to doxygen
+comments inside @xmlonly ... @endxmlonly blocks.
+
+Here's a description of all the custom tags:
+
+```xml
+<!--
+Introduces documentation for a new function.
+The title of the section documenting the function will be NAME.
+Other parts of the manual can refer to this function's documentation with \autoref{sec:LABEL}
+-->
+<manual name="NAME" label="LABEL"/>
+
+<!-- Translated to the latex \autoref{sec:SEC} -->
+<autoref sec="SEC"/>
+
+<!-- Translated to the latex \ref{sec:SEC} -->
+<shortref sec="SEC"/>
+
+<!-- Translated to the latex \errorenumdesc, a custom command defined in manual/parts/api.tex <https://github.com/seL4/seL4/blob/master/manual/parts/api.tex> -->
+<errorenumdesc/>
+
+<!-- Translated to the latex \obj{NAME}, a custom command defined in manual/manual.tex <https://github.com/seL4/seL4/blob/master/manual/manual.tex> -->
+<obj name="NAME"/>
+
+<!-- Translated to the latex \texttt{TEXT} -->
+<texttt text="TEXT"/>
+```
+
+Note that these must appear within `@xmlonly` ... `@endxmlonly` blocks in
+order to function.
+
+#### Required Documentation
+
+Each function in the API must have the following documentation:
+
+- a `@xmlonly <manual name="..." label=".../> @endxmlonly` tag with the `name`
+  for use in the manual's text, and a `label` for creating references within the
+  manual
+- a `@brief` description
+- a detailed description
+- a `@param` description of each argument
+- a `@return` description of the return value, unless the function is `void`
+
+#### Detecting Missing Documentation
+
+If a required part of a function's documentation is empty, the translation
+script will insert the LaTeX command `\todo`, defined in
+[manual/parts/api.tex](https://github.com/seL4/seL4/blob/master/manual/parts/api.tex).
+It generates the text "TODO" to help readers of the manual identify which parts
+of the API are undocumented.
+
+#### Generated LaTeX Files
+
+The LaTeX files generated by the translation script are placed in
+`manual/generated`. Doxygen-generated XML files are placed in
+`manual/doxygen-output/xml`.
+
+Each API is documented in a separate file. The separation of APIs is implemented
+using doxygen's `@defgroup` directive. Specifically, each API is defined in a
+separate named group. In the doxygen-generated XML, each group's documentation
+is in a separate file. The XML-to-LaTeX script then transforms each relevant XML
+file into the corresponding LaTeX file.
+
+#### Doxygen Configuration
+
+The correct behaviour of the manual build system depends on a specific doxygen
+configuration. A `Doxyfile` containing this configuration is checked into the
+kernel repo at
+[manual/Doxyfile](https://github.com/seL4/seL4/blob/master/manual/Doxyfile)
+
+### System Calls
+
+A prototype for each system call is declared in
+[libsel4/include/sel4/syscalls.h](https://github.com/seL4/seL4/blob/master/libsel4/include/sel4/syscalls.h).
+Each function is documented with a comment of the form described above.
+
+### Object Invocations
+
+#### Stub Generation
+
+These are more complicated, as the C source code implementing the user-level
+object invocations functions is generated from interface descriptions in XML.
+The following XML files contain object invocation interface descriptions:
+
+- [libsel4/include/interfaces/object-api.xml](https://github.com/seL4/seL4/blob/master/libsel4/include/interfaces/object-api.xml)
+- [libsel4/arch_include/x86/interfaces/object-api-arch.xml](https://github.com/seL4/seL4/blob/master/libsel4/arch_include/x86/interfaces/object-api-arch.xml)
+- [libsel4/arch_include/arm/interfaces/object-api-arch.xml.xml](https://github.com/seL4/seL4/blob/master/libsel4/arch_include/arm/interfaces/object-api-arch.xml)
+- [libsel4/sel4_arch_include/ia32/interfaces/object-api-sel4-arch.xml](https://github.com/seL4/seL4/blob/master/libsel4/sel4_arch_include/ia32/interfaces/object-api-sel4-arch.xml)
+- [libsel4/sel4_arch_include/x86_64/interfaces/object-api-sel4-arch.xml](https://github.com/seL4/seL4/blob/master/libsel4/sel4_arch_include/x86_64/interfaces/object-api-sel4-arch.xml)
+- [libsel4/sel4_arch_include/aarch32/interfaces/object-api-sel4-arch.xml](https://github.com/seL4/seL4/blob/master/libsel4/sel4_arch_include/aarch32/interfaces/object-api-sel4-arch.xml)
+- [libsel4/sel4_arch_include/aarch64/interfaces/object-api-sel4-arch.xml](https://github.com/seL4/seL4/blob/master/libsel4/sel4_arch_include/aarch64/interfaces/object-api-sel4-arch.xml)
+
+There is a script in the sel4 repo for generating C header files from a given
+interface description:
+[libsel4/tools/syscall_stub_gen.py](https://github.com/seL4/seL4/blob/master/libsel4/tools/syscall_stub_gen.py).
+Note that despite its name, the script generates object invocation stubs - not
+syscall stubs.
+
+#### Documentation
+
+Object invocation API documentation is located inline with the interface
+descriptions in the XML files listed above. The XML language with which the
+interfaces are described contains tags for documenting functions. For the
+purpose of validation, the XML schema defining this language is in:
+[libsel4/tools/sel4_idl.xsd](https://github.com/seL4/seL4/blob/master/libsel4/tools/sel4_idl.xsd).
+This is a superset of the XML tags used in doxygen comments. The doxygen comment
+tags described above have the same meaning in the interface description files.
+Additional tags are used for the description and documentation of object
+invocation interfaces.
+
+When C code is generated from an interface description file, the documentation
+inlined in that file is converted into doxygen comments of the form described
+above.