Skip to content

docs: trivial fixes #533

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
yf13 wants to merge 1 commit into
base: main
Choose a base branch
from
+4 −3
Open

docs: trivial fixes #533

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 4 additions & 3 deletions docs/manual.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1177,9 +1177,9 @@ To boot a Microkit image, use a GDB prompt via openOCD per [seL4 Docs](https://d

2. Set the `a0` and `a1` registers for OpenSBI

# tell OpenSBI where DTB is (there is none)
(gdb) # tell OpenSBI where DTB is (there is none)

@midnightveil midnightveil Jun 22, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'd rather these be placed in backticks ``` and indentation removed, I think.

IDK why the markdown parswr would be parsing headings when its indented for a coxe block...

@midnightveil midnightveil Jun 22, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It seems that the manual PDF and GitHub both parse this correctly?

I don't understand this change.

@lsf37 lsf37 Jun 22, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Standard markdown specs would definitely not parse this as heading. Indented code blocks are not an exotic feature, but putting it into a fenced code block like @midnightveil suggests would fix any ambiguity if you want to be extra sure.

Adding (gdb) seems not good to me, because (gdb) is the prompt and the line is supposed to be a comment between prompts.

(gdb) set $a0=0
# tell OpenSBI that the default hart is #0
(gdb) # tell OpenSBI that the default hart is #0
(gdb) set $a1=0

3. Load OpenSBI's FW_JUMP payload targeted at `0x90000000`, implicitly setting the program counter.
Expand Down Expand Up @@ -1811,6 +1811,7 @@ At build-time, the Microkit tool embeds the capDL specification that describe
all kernel objects that needs to be created. Then for each kernel object, the spec
describe what state they need to be in and what capabilities exist to that object
(i.e. who has access to this kernel object). For example, the spec would specify the:

- starting Instruction Pointer (IP), Stack Pointer (SP) and IPC buffer pointer of a Thread Control Block (TCB),
- page table structure and mapping attributes of an address space (VSpace),
- interrupts (IRQ),
Expand Down Expand Up @@ -1862,7 +1863,7 @@ In order to do this however, the Microkit tool needs to emulate how the seL4 ker
to obtain the list of free untyped objects that the kernel would give to the initial task.

While this is non-trivial to do, it comes with the useful property that if the tool
produces a valid image, there should be no errors upon initialising the system
produces a valid image, there should be no errors upon initialising the system.
If there are any errors with configuring the system (e.g running out of memory),
they will be caught at build-time. This can only reasonably be done due to the
static-architecture of Microkit systems.
Loading