Update tutorials for better docsite presentation

This commit should be read together with PR seL4/docs#231

The aim of both PRs was to arrange the tutorial material on the docsite
such that it is clear and easy to follow. Inspired by the Rust book
https://doc.rust-lang.org/book/, the user can see the chapters in the
index on the left, and go straight to the corresponding tutorial
sections.

Specifically, the updates on the docsite provide:

- a streamlined guide to completing the tutorials
- a streamlined "setting up your machine" page
- a how-to page with solutions to tutorial questions
- more organised landing page
- The tutorials have been slightly rewritten to correct minor errors and
  provide inline solutions for readers wishing to understand the
  material and/or get quick solutions

General changes in most files:

- Make language and bullet points consistent; and, where required, add
  headers that can be referred to from how-to page
- Add section on how to get tutorial solutions
- Add inline tutorial solutions
- Where necessary, add note that tutorial requires CapDL Loader, and
  instructions on how to get it.

Specific files:

macros.py:
Remove help block, which was pointing to a list of contacts and
resources. These are accessible via the updated tutorials nav sidebar.

Rename get-the-code with the more specific get-the-tutorials.
Add definition for accessing a tutorial with completed solutions.

template.py:
Add code to replace links to docsite (when tutorials are run in the
docsite) with relative links.

hello-world.md:
Add more details on containers, builds and QEMU to ease the user into
the tutorials.

C Libraries:
Generic change for C Libraries in the tutorials repo: C Libraries were
previously called Dynamic Libraries, and filenames were dynamic-1 etc.
There are now libraries-1 etc.

hello-camkes-0.md:
Add link to CAmkES tutorial slides

camkes-vm-crossvm.md:
Add note that tutorial instructions for this tutorial are only for
Linux.

Signed-off-by: Signed-off-by: Birgit Brecknell <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>

.github/workflows/test.yml

@@ -43,10 +43,10 @@ jobs:
       matrix:
         app:
         - capabilities
-        - dynamic-1
-        - dynamic-2
-        - dynamic-3
-        - dynamic-4
+        - libraries-1
+        - libraries-2
+        - libraries-3
+        - libraries-4
         - hello-camkes-0
         - hello-camkes-1
         - hello-camkes-2

README.md

@@ -1,5 +1,5 @@
 <!--
-     Copyright 2017, Data61, CSIRO (ABN 41 687 119 230).
+     Copyright 2024, seL4 Project a Series of LF Projects, LLC..
 
      SPDX-License-Identifier: CC-BY-SA-4.0
 -->

common.py

@@ -26,10 +26,10 @@
 TUTORIALS = {
     'hello-world': ALL_CONFIGS,
     'ipc': ALL_CONFIGS,
-    'dynamic-1': ALL_CONFIGS,
-    'dynamic-2': ALL_CONFIGS,
-    'dynamic-3': ALL_CONFIGS,
-    'dynamic-4': ALL_CONFIGS,
+    'libraries-1': ALL_CONFIGS,
+    'libraries-2': ALL_CONFIGS,
+    'libraries-3': ALL_CONFIGS,
+    'libraries-4': ALL_CONFIGS,
     'hello-camkes-0': ALL_CONFIGS,
     'hello-camkes-1': ALL_CONFIGS,
     'hello-camkes-2': ALL_CONFIGS,

template.py

@@ -19,6 +19,8 @@
 except ImportError:
     from yaml import Loader, Dumper
 
+from io import StringIO
+
 
 def build_render_list(args):
     '''
@@ -64,6 +66,7 @@ def render_file(args, env, state, file):
     is for dependency tracking
     '''
     filename = os.path.join(args.out_dir, file)
+
     # Create required directories
     if not os.path.exists(os.path.dirname(filename)):
         os.makedirs(os.path.dirname(filename))
@@ -80,6 +83,18 @@ def render_file(args, env, state, file):
         input = in_stream.read()
         template = env.from_string(input)
 
+        if (args.__getattribute__("docsite")):
+            s = StringIO(input)
+            lines = input.split('\n')
+
+            i = 0
+            for line in s:
+                lines[i] = line.replace("https://docs.sel4.systems/Tutorials/", "/Tutorials/")
+                i = i + 1
+
+            new_text = ''.join(lines)
+            template = env.from_string(str(new_text))
+
         out_stream.write(template.render(context.get_context(args, state)))
 
 

tools/macros.py

@@ -34,20 +34,6 @@ def ninja_simulate_block():
 ```'''
 
 
-def help_block():
-    return '''
----
-## Getting help
-Stuck? See the resources below.
-* [FAQ](https://docs.sel4.systems/FrequentlyAskedQuestions)
-* [seL4 Manual](http://sel4.systems/Info/Docs/seL4-manual-latest.pdf)
-* [Debugging guide](https://docs.sel4.systems/DebuggingGuide.html)
-* [seL4 Discourse forum](https://sel4.discourse.group)
-* [Developer's mailing list](https://lists.sel4.systems/postorius/lists/devel.sel4.systems/)
-* [Mattermost Channel](https://mattermost.trustworthy.systems/sel4-external/)
-'''
-
-
 def cmake_check_script(state):
     return '''set(FINISH_COMPLETION_TEXT "%s")
 set(START_COMPLETION_TEXT "%s")
@@ -59,7 +45,7 @@ def cmake_check_script(state):
 
 def tutorial_init(name):
     return '''```sh
-# For instructions about obtaining the tutorial sources see https://docs.sel4.systems/Tutorials/#get-the-code
+# For instructions about obtaining the tutorial sources see https://docs.sel4.systems/Tutorials/get-the-tutorials
 #
 # Follow these instructions to initialise the tutorial
 # initialising the build directory with a tutorial exercise
@@ -69,3 +55,17 @@ def tutorial_init(name):
 ninja
 ```
 ''' % (name, name)
+
+
+def tutorial_init_with_solution(name):
+    return '''```sh
+# For instructions about obtaining the tutorial sources see https://docs.sel4.systems/Tutorials/get-the-tutorials
+#
+# Follow these instructions to initialise the tutorial
+# initialising the build directory with a tutorial exercise
+./init --solution --tut %s
+# building the tutorial exercise
+cd %s_build
+ninja
+```
+''' % (name, name)

tutorials/camkes-vm-crossvm/camkes-vm-crossvm.md

@@ -8,21 +8,32 @@
     'crossvm'
 ]) ?*/
 
-# CAmkES VM: Cross VM Connectors
+# CAmkES Cross VM Connectors
 
 This tutorial provides an introduction to using the cross virtual machine (VM) connector mechanisms
 provided by seL4 and Camkes in order to connect processes in a guest Linux instance to Camkes components.
 
+In this tutorial you will learn how to:
+
+* Configure processes in a Linux guest VM to communicate with CAmkES components
+
 ## Prerequisites
+1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up)
+2. [CAmkES VM Linux tutorial](https://docs.sel4.systems/Tutorials/camkes-vm-linux)
 
-1. [Set up your machine](https://docs.sel4.systems/HostDependencies#camkes-build-dependencies).
-1. [Camkes VM](https://docs.sel4.systems/Tutorials/camkes-vm-linux)
+*Note that the instructions for this tutorial are only for Linux.*
 
-## Outcomes
+## Initialising
 
-By the end of this tutorial, you should be able to:
+/*? macros.tutorial_init("camkes-vm-crossvm") ?*/
 
-* Configure processes in a Linux guest VM to communicate with CAmkES components
+<details markdown='1'>
+<summary><em>Hint:</em> tutorial solutions</summary>
+<br>
+All tutorials come with complete solutions. To get solutions run:
+
+/*? macros.tutorial_init_with_solution("camkes-vm-crossvm") ?*/
+</details>
 
 ## Background
 

tutorials/camkes-vm-linux/camkes-vm-linux.md

@@ -6,21 +6,52 @@
 
 /*? declare_task_ordering(['vm-cmake-start','vm-pkg-hello-c','vm-pkg-hello-cmake','vm-cmake-hello','vm-module-poke-c','vm-module-poke-make','vm-module-poke-cmake','vm-cmake-poke','vm-init-poke']) ?*/
 
-# CAmkES VM: Adding a Linux Guest
+# CAmkES VM Linux
 
 This tutorial provides an introduction to creating VM guests and applications on seL4 using CAmkES.
 
+You will become familiar with:
+
+* Creating, configuring and building guest Linux VM components in CAmkES.
+* Building and installing your own Linux VM user-level programs and kernel modules.
+
+*Note that the instructions for this tutorial are only for Linux.*
+
 ## Prerequisites
+1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up)
+2. [CAmkES timer tutorial](https://docs.sel4.systems/Tutorials/hello-camkes-timer)
 
-1. [Set up your machine](https://docs.sel4.systems/HostDependencies#camkes-build-dependencies).
-1. [Camkes VM](https://docs.sel4.systems/Tutorials/camkes-vm-linux)
+## CapDL Loader
 
-## Outcomes
+This tutorial uses the *capDL loader*, a root task which allocates statically
+ configured objects and capabilities.
 
-By the end of this tutorial, you should be familiar with:
+<details markdown='1'>
+<summary>Get CapDL</summary>
+The capDL loader parses
+a static description of the system and the relevant ELF binaries.
+It is primarily used in [Camkes](https://docs.sel4.systems/CAmkES/) projects
+but we also use it in the tutorials to reduce redundant code.
+The program that you construct will end up with its own CSpace and VSpace, which are separate
+from the root task, meaning CSlots like `seL4_CapInitThreadVSpace` have no meaning
+in applications loaded by the capDL loader.
+<br>
+More information about CapDL projects can be found [here](https://docs.sel4.systems/CapDL.html).
+<br>
+For this tutorial clone the [CapDL repo](https://github.com/sel4/capdl). This can be added in a directory that is adjacent to the tutorials-manifest directory.
+</details>
 
-* Creating, configuring and building guest Linux VM components in CAmkES.
-* Building and installing your own Linux VM user-level programs and kernel modules.
+## Initialising
+
+/*? macros.tutorial_init("camkes-vm-linux") ?*/
+
+<details markdown='1'>
+<summary><em>Hint:</em> tutorial solutions</summary>
+<br>
+All tutorials come with complete solutions. To get solutions run:
+
+/*? macros.tutorial_init_with_solution("camkes-vm-linux") ?*/
+</details>
 
 ## Background
 
@@ -30,7 +61,7 @@ The starting application should boot a single, very basic Linux guest.
 To build the tutorial, run:
 /*? macros.ninja_block() ?*/
 
-You can boot the tutorial on an x86 hardware platform with a multiboot boot loader, 
+You can boot the tutorial on an x86 hardware platform with a multiboot boot loader,
 or use the [QEMU](https://www.qemu.org) simulator. **Note if you are using QEMU
 it is important to ensure that your host machine has VT-x support and [KVM](https://www.linux-kvm.org/page/Main_Page)
 installed. You also need to ensure you have enabled nested virtulisation with KVM guests as described
@@ -55,7 +86,7 @@ buildroot login:
 
 You can login with the username `root` and the password `root`.
 
-The Linux guest was built using [buildroot](https://buildroot.org/), which 
+The Linux guest was built using [buildroot](https://buildroot.org/), which
 creates a compatible kernel and minimal root filesystem containing busybox and a in-memory file system (a ramdisk).
 
 ## VM Components
@@ -121,7 +152,7 @@ strings specifying:
  - boot arguments to the guest Linux,
  - the name of the guest Linux kernel image file,
  - and the name of the guest Linux initrd file (the root filesystem to use during system initialization).
- 
+
 The kernel command-line is defined in the `VM_GUEST_CMDLINE` macro. The kernel image
 and rootfs names are defined in the applications `CMakeLists.txt` file.
 These are the names of files in a CPIO archive that gets created by the build system, and
@@ -178,7 +209,7 @@ GenerateCAmkESRootserver()
 /*- endfilter -*/
 ```
 
-The file `projects/camkes/vm/camkes_vm_helpers.cmake` provides helper functions for the VM projects, 
+The file `projects/camkes/vm/camkes_vm_helpers.cmake` provides helper functions for the VM projects,
 including  `DeclareCAmkESVM(Init0)`, which is used to define the `Init0` VM component.
 Each Init component requires a corresponding `DeclareCAmkESVM` function.
 
@@ -188,25 +219,25 @@ in the `projects/vm-linux` folder, which contains some tools for building new li
 and root filesystem images, as well as the images that these tools
 produce. A fresh checkout of this project will contain some pre-built
 images (`bzimage` and `rootfs.cpio`), to speed up build times.
- 
-`DecompressLinuxKernel` is used to extract the vmlinux image, which `AddToFileServer` then places 
+
+`DecompressLinuxKernel` is used to extract the vmlinux image, which `AddToFileServer` then places
 in the fileserver along with the rootfs.
- 
+
 ## Adding to the guest
 
 In the simple buildroot guest image, the
 initrd (rootfs.cpio) is also the filesystem you get access to after
 logging in. To make new programs available to the guest you need to add them to the
 rootfs.cpio archive. Similarly, to make new kernel modules available to
-the guest they must be added to the rootfs.cpio archive also. 
+the guest they must be added to the rootfs.cpio archive also.
 
 In this tutorial you will  install new programs into the guest VM.
 
 ### vm-linux-helpers.cmake
 
 The `projects/camkes/vm-linux` directory contains CMake helpers to
 overlay rootfs.cpio archives with a desired set of programs, modules
-and scripts. 
+and scripts.
 
 #### `AddFileToOverlayDir(filename file_location root_location overlay_name)`
 This helper allows you to overlay specific files onto a rootfs image. The caller specifies
@@ -244,7 +275,7 @@ This is a helper function for downloading the linux source. This is needed if we
 This helper function is used for configuring downloaded linux source with a given Kbuild defconfig (`linux_config_location`)
 and symvers file (`linux_symvers_location`).
 
-## Exercises 
+## Exercises
 
 ### Adding a program
 
@@ -278,7 +309,7 @@ add_executable(hello hello.c)
 target_link_libraries(hello -static)
 /*-- endfilter -*/
 ```
-Now integrate the new program with the build system. 
+Now integrate the new program with the build system.
 Update the VM apps `CMakeLists.txt` to declare the hello application as an
 external project and add it to our overlay.
  Do this by replacing the line `AddToFileServer("rootfs.cpio" ${default_rootfs_file})` with the following:
@@ -314,7 +345,7 @@ AddToFileServer("rootfs.cpio" ${rootfs_file} DEPENDS rootfs_target)
 Now rebuild the project...
 /*? macros.ninja_block() ?*/
 ..and run it (use `root` as username and password).
-You should be able to use the new program. 
+You should be able to use the new program.
 
 ```
 Welcome to Buildroot
@@ -403,7 +434,7 @@ DefineLinuxModule(${CMAKE_CURRENT_LIST_DIR}/poke poke-module poke-target KERNEL_
 /*-- endfilter -*/
 ```
 Update the VM `CMakeLists.txt` file to declare the new poke module as an
-external project and add it to the overlay. 
+external project and add it to the overlay.
 
 At the top of the file include our linux helpers, add the following:
 
@@ -447,7 +478,7 @@ AddExternalProjFilesToOverlay(poke-module ${CMAKE_CURRENT_BINARY_DIR}/poke-modul
 /*-- endfilter -*/
 ```
 
-Write a custom init script that loads the new module during initialization. 
+Write a custom init script that loads the new module during initialization.
 Create a file called `init` in our tutorial directory with the following:
 
 ```bash
@@ -491,7 +522,7 @@ Password:
 -sh: write error: Bad address    # the shell complains, but our module is being invoked!
 ```
 
-### Create a hypercall
+### Creating a hypercall
 
 In `modules/poke/poke.c`, replace `printk("hi\n");` with `kvm_hypercall1(4, 0);`.
 The choice of 4 is because 0..3 are already used by existing hypercalls.