From a7290dce551f2fe37e04502646d30e98e15f4476 Mon Sep 17 00:00:00 2001
From: Birgit Brecknell <b@brck.nl>
Date: Mon, 6 Jan 2025 16:27:43 +1100
Subject: [PATCH] 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 <b@brck.nl>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 .github/workflows/test.yml                    |    8 +-
 README.md                                     |    2 +-
 common.py                                     |    8 +-
 template.py                                   |   15 +
 tools/macros.py                               |   30 +-
 .../camkes-vm-crossvm/camkes-vm-crossvm.md    |   23 +-
 tutorials/camkes-vm-linux/camkes-vm-linux.md  |   75 +-
 tutorials/capabilities/capabilities.md        |   45 +-
 tutorials/fault-handlers/fault-handlers.md    |  155 ++-
 tutorials/hello-camkes-0/hello-camkes-0.md    |   23 +-
 tutorials/hello-camkes-1/hello-camkes-1.md    |  161 ++-
 tutorials/hello-camkes-2/hello-camkes-2.md    | 1092 +++++++++++------
 tutorials/hello-camkes-timer/CMakeLists.txt   |    5 +-
 .../hello-camkes-timer/hello-camkes-timer.md  |  559 ++++++---
 tutorials/hello-world/hello-world.md          |   97 +-
 tutorials/interrupts/interrupts.md            |   90 +-
 tutorials/ipc/ipc.md                          |   94 +-
 .../{dynamic-1 => libraries-1}/CMakeLists.txt |   10 +-
 .../libraries-1.md}                           |  203 ++-
 .../{dynamic-2 => libraries-2}/CMakeLists.txt |   10 +-
 .../libraries-2.md}                           |  200 ++-
 .../{dynamic-3 => libraries-3}/CMakeLists.txt |   10 +-
 .../libraries-3.md}                           |  125 +-
 .../{dynamic-4 => libraries-4}/CMakeLists.txt |   10 +-
 .../libraries-4.md}                           |   92 +-
 tutorials/mapping/mapping.md                  |   43 +-
 tutorials/mcs/mcs.md                          |  275 +++--
 tutorials/notifications/notifications.md      |  115 +-
 tutorials/threads/threads.md                  |  196 ++-
 tutorials/untyped/untyped.md                  |   80 +-
 30 files changed, 2744 insertions(+), 1107 deletions(-)
 rename tutorials/{dynamic-1 => libraries-1}/CMakeLists.txt (70%)
 rename tutorials/{dynamic-1/dynamic-1.md => libraries-1/libraries-1.md} (91%)
 rename tutorials/{dynamic-2 => libraries-2}/CMakeLists.txt (70%)
 rename tutorials/{dynamic-2/dynamic-2.md => libraries-2/libraries-2.md} (94%)
 rename tutorials/{dynamic-3 => libraries-3}/CMakeLists.txt (76%)
 rename tutorials/{dynamic-3/dynamic-3.md => libraries-3/libraries-3.md} (92%)
 rename tutorials/{dynamic-4 => libraries-4}/CMakeLists.txt (76%)
 rename tutorials/{dynamic-4/dynamic-4.md => libraries-4/libraries-4.md} (90%)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 9e0eefc1..f2569c4f 100644
--- a/.github/workflows/test.yml
+++ b/.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
diff --git a/README.md b/README.md
index 8f7b2023..64be8566 100644
--- a/README.md
+++ b/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
 -->
diff --git a/common.py b/common.py
index efc4df6d..dd10ff38 100644
--- a/common.py
+++ b/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,
diff --git a/template.py b/template.py
index b6337517..2df060ea 100755
--- a/template.py
+++ b/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)))
 
 
diff --git a/tools/macros.py b/tools/macros.py
index 17c39d92..529e0848 100644
--- a/tools/macros.py
+++ b/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)
diff --git a/tutorials/camkes-vm-crossvm/camkes-vm-crossvm.md b/tutorials/camkes-vm-crossvm/camkes-vm-crossvm.md
index 19232a79..8cca7aff 100644
--- a/tutorials/camkes-vm-crossvm/camkes-vm-crossvm.md
+++ b/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
 
diff --git a/tutorials/camkes-vm-linux/camkes-vm-linux.md b/tutorials/camkes-vm-linux/camkes-vm-linux.md
index f053c2bc..39ef12a5 100644
--- a/tutorials/camkes-vm-linux/camkes-vm-linux.md
+++ b/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,17 +219,17 @@ 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.
 
@@ -206,7 +237,7 @@ In this tutorial you will  install new programs into the guest VM.
 
 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.
diff --git a/tutorials/capabilities/capabilities.md b/tutorials/capabilities/capabilities.md
index 500e9fea..93afbf60 100644
--- a/tutorials/capabilities/capabilities.md
+++ b/tutorials/capabilities/capabilities.md
@@ -6,27 +6,31 @@
 
 /*? declare_task_ordering(['cnode-start', 'cnode-size', 'cnode-copy', 'cnode-delete', 'cnode-invoke']) ?*/
 
-
 # Capabilities
 
-This tutorial provides a basic introduction to seL4 capabilities.
+You will learn:
+1. The jargon CNode, CSpace, CSlot.
+2. How to invoke a capability.
+3. How to delete and copy CSlots.
 
 ## Prerequisites
 
-1. [Set up your machine](https://docs.sel4.systems/HostDependencies).
+1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up)
 2. [Hello world](https://docs.sel4.systems/Tutorials/hello-world)
 
 ## Initialising
 
 /*? macros.tutorial_init("capabilities") ?*/
 
-## Outcomes
+<details markdown='1'>
+<summary><em>Hint:</em> tutorial solutions</summary>
+<br>
+All tutorials come with complete solutions. To get solutions run:
 
-By the end of this tutorial, you should be familiar with:
+/*? macros.tutorial_init_with_solution("capabilities") ?*/
 
-1. The jargon CNode, CSpace, CSlot.
-2. Know how to invoke a capability.
-3. Know how to delete and copy CSlots.
+Answers are also available in drop down menus under each section.
+</details>
 
 ## Background
 
@@ -235,7 +239,8 @@ The third line stating the number of slots in the CSpace, is incorrect, and your
 /*-- endfilter -*/
 ```
 
-/*-- filter ExcludeDocs() -*/
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
 
 ```c
 /*-- filter TaskContent("cnode-size", TaskContentType.COMPLETED, subtask='size', completion='The CNode is [0-9]+ bytes in size') -*/
@@ -244,7 +249,7 @@ The third line stating the number of slots in the CSpace, is incorrect, and your
 /*-- endfilter -*/
 ```
 
-/*-- endfilter -*/
+</details>
 
 ### Copy a capability between CSlots
 
@@ -278,7 +283,8 @@ The error occurs as the existing code tries to set the priority of the initial t
 /*-- endfilter -*/
 ```
 
-/*-- filter ExcludeDocs() -*/
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
 
 ```c
 /*-- filter TaskContent("cnode-copy", TaskContentType.COMPLETED, subtask='copy', completion='first_free_slot is not empty') -*/
@@ -299,8 +305,8 @@ The error occurs as the existing code tries to set the priority of the initial t
     ZF_LOGF_IF(error, "Failed to set priority");
 /*-- endfilter -*/
 ```
+</details>
 
-/*-- endfilter -*/
 On success, you will now see the output:
 
 ```
@@ -339,8 +345,8 @@ by a neat hack: by attempting to move the CSlots onto themselves. This should fa
     ZF_LOGF_IF(error != seL4_FailedLookup, "last_slot is not empty");
 /*-- endfilter -*/
 ```
-
-/*-- filter ExcludeDocs() -*/
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
 
 ```c
 /*-- filter TaskContent("cnode-delete", TaskContentType.COMPLETED, subtask='delete', completion='Failed to suspend current thread') -*/
@@ -359,7 +365,7 @@ by a neat hack: by attempting to move the CSlots onto themselves. This should fa
 /*-- endfilter -*/
 ```
 
-/*-- endfilter -*/
+</details>
 
 On success, the output will now show:
 
@@ -370,7 +376,7 @@ Suspending current thread
 main@main.c:56 Failed to suspend current thread
 ```
 
-#### Invoking capabilities
+#### Suspend a thread
 
 **Exercise** Use `seL4_TCB_Suspend` to try and suspend the current thread.
 
@@ -382,7 +388,8 @@ main@main.c:56 Failed to suspend current thread
 /*-- endfilter -*/
 ```
 
-/*-- filter ExcludeDocs() -*/
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
 
 ```c
 /*-- filter TaskContent("cnode-invoke", TaskContentType.COMPLETED, subtask='invoke', completion='Suspending current thread') -*/
@@ -391,8 +398,7 @@ main@main.c:56 Failed to suspend current thread
     ZF_LOGF("Failed to suspend current thread\n");
 /*-- endfilter -*/
 ```
-
-/*-- endfilter -*/
+</details>
 
 On success, the output will be as follows:
 
@@ -411,7 +417,6 @@ to become more familiar with CSpaces.
 * Make copies of the entire CSpace described by `seL4_BootInfo`
 * Experiment with other [CNode invocations](https://docs.sel4.systems/projects/sel4/api-doc.html#sel4_cnode).
 
-/*? macros.help_block() ?*/
 /*-- filter ExcludeDocs() -*/
 
 ```c
diff --git a/tutorials/fault-handlers/fault-handlers.md b/tutorials/fault-handlers/fault-handlers.md
index aacbf68f..87fefaab 100644
--- a/tutorials/fault-handlers/fault-handlers.md
+++ b/tutorials/fault-handlers/fault-handlers.md
@@ -10,24 +10,54 @@
         ['fault-badge', 'fault-ep-setup', 'fault-ipc-recv', 'fault-handle', 'fault-resume'])
 ?*/
 
+This tutorial covers fault handling in seL4.
+
+You will learn:
+1. About thread faults.
+2. That a thread fault is different from a processor hardware fault.
+3. About fault handlers.
+4. What the kernel does to a thread which has faulted.
+5. How to set the endpoint that the kernel will deliver fault messages on (master vs MCS).
+6. How to resume threads after they have faulted.
+
 ## Prerequisites
 
-1. [Set up your machine](https://docs.sel4.systems/HostDependencies).
-2. [Capabilities tutorial](https://docs.sel4.systems/Tutorials/capabilities).
-3. [IPC Tutorial](https://docs.sel4.systems/Tutorials/ipc).
+1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up)
+2. [Capabilities tutorial](https://docs.sel4.systems/Tutorials/capabilities)
+3. [IPC tutorial](https://docs.sel4.systems/Tutorials/ipc)
 
 ## Initialising
 
 /*? macros.tutorial_init("fault-handlers") ?*/
 
-## Outcomes
+<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("fault-handlers") ?*/
+
+</details>
+
+## CapDL Loader
+
+This tutorial uses the *capDL loader*, a root task which allocates statically
+ configured objects and capabilities.
 
-1. Learn what a thread fault is.
-2. Understand that a thread fault is different from a processor hardware fault.
-3. Learn what a fault handler is.
-4. Understand what the kernel does to a thread which has faulted.
-5. Learn how to set the endpoint that the kernel will deliver fault messages on (master vs MCS).
-6. Learn how to resume threads after they have faulted.
+<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>
 
 ## Background: What is a fault, and what is a fault handler?
 
@@ -81,7 +111,7 @@ If the fault handler did not properly rectify the anomaly in the faulting
 thread, resuming the faulting thread will simply cause the kernel to re-generate
 the fault.
 
-## Reasons for thread faults:
+## Reasons for thread faults
 
 Thread faults can be generated for different reasons. When a fault occurs the
 kernel will pass information describing the cause of the fault as an IPC
@@ -97,7 +127,7 @@ In addition, the following fault types are added by the MCS kernel:
 
 * Timeout fault: Triggered when a thread consumes all of its budget and still has further execution to do in the current period.
 
-## Thread fault messages:
+## Thread fault messages
 
 When a fault is generated, the kernel will deliver an IPC message across the
 fault endpoint. This IPC message contains information that tells the fault
@@ -112,7 +142,7 @@ the [seL4 Manual](https://sel4.systems/Info/Docs/seL4-manual-latest.pdf).
 The rest of this tutorial will attempt to teach the reader how to receive and
 handle seL4 thread faults.
 
-## Setting up a fault endpoint for a thread:
+## Setting up a fault endpoint for a thread
 
 In the scenario where a fault message is being delivered on a fault endpoint,
 the kernel acts as the IPC "sender" and the fault handler acts as a receiver.
@@ -121,7 +151,7 @@ This implies that when caps are being handed out to the fault endpoint object,
 one cap to the object must be given to the kernel and one cap to the object must
 be given to the handler.
 
-### Kernel end vs handler end:
+### Kernel end vs handler end
 
 Programmers specify the capability to use a fault handler for a thread when
 configuring a TCB. As a result the programmer can also set a badge on the
@@ -138,7 +168,7 @@ faults from multiple threads. Please see the
 [IPC Tutorial](https://docs.sel4.systems/Tutorials/ipc) for a refresher on how
 badged fault endpoints work.
 
-### Differences between MCS and Master kernel:
+### Differences between MCS and Master kernel
 
 There is a minor difference in the way that the kernel is informed of the
 cap to a fault endpoint, between the master and MCS kernels.
@@ -160,7 +190,7 @@ You will be guided through the following broad steps:
 3. Handling the fault in the fault handler.
 4. Resuming the execution of the faulting thread.
 
-### Description of the tutorial program:
+### Description of the tutorial program
 
 The tutorial features two threads in different virtual address spaces. One
 thread is the "`faulter`" and the other is the "`handler`". The `faulter` is going to
@@ -241,6 +271,35 @@ kernel can deliver fault IPC messages to the `handler`. Since we're
 using the Master kernel, we need to pass a CPtr that can be resolved from within
 the CSpace of the `faulter` thread:
 
+```c
+    /* Here we need to keep in mind which CPtr we give the kernel. On the MCS
+     * kernel, we must give a CPtr which can be resolved during the course of
+     * this seL4_TCB_SetSpace syscall, from within our own CSpace.
+     *
+     * On the Master kernel, we must give a CPtr which can be resolved during
+     * the generation of a fault message, from within the CSpace of the
+     * (usually foreign) faulting thread.
+     */
+
+    error = seL4_TCB_SetSpace(
+        faulter_tcb_cap,
+        foreign_badged_faulter_empty_slot_cap,
+        faulter_cspace_root,
+        0,
+        faulter_vspace_root,
+        0);
+
+    ZF_LOGF_IF(error != 0, PROGNAME "Failed to configure faulter's TCB with our fault ep!");
+    printf(PROGNAME "Successfully registered badged fault handling ep with "
+           "the kernel.\n"
+           PROGNAME "About to wake the faulter thread.\n");
+
+    /* Signal the faulter thread to try to touch the invalid cspace slot. */
+    seL4_Reply(seL4_MessageInfo_new(0, 0, 0, 0));
+    /* Now wait for the fault IPC message from the kernel. */
+    seL4_Recv(faulter_fault_ep_cap, &tmp_badge);
+```
+/*-- filter ExcludeDocs() -*/
 ```c
 /*-- filter TaskContent("fault-ep-setup", TaskContentType.COMPLETED, subtask="setup", completion="About to touch fault vaddr.") -*/
     error = seL4_TCB_SetSpace(
@@ -252,20 +311,40 @@ the CSpace of the `faulter` thread:
         0);
 /*-- endfilter -*/
 ```
+/*-- endfilter -*/
 
-### Receiving the IPC message from the kernel:
+### Receiving the IPC message from the kernel
 
 The kernel will deliver the IPC message to any thread waiting on the fault
 endpoint. To wait for a fault IPC message simply `seL4_Recv()`, the same way
 you'd wait for any other IPC message:
 
+```c
+    /* The IPC message for a cap fault contains the cap address of the slot
+     * which generated the cap fault.
+     *
+     * We need to retrieve this slot address and fill that slot with a random
+     * endpoint cap of our choosing so that the faulter thread can touch that
+     * slot successfully.
+     */
+
+    foreign_faulter_capfault_cap = seL4_GetMR(seL4_CapFault_Addr);
+
+    printf(PROGNAME "Received fault IPC message from the kernel.\n"
+           PROGNAME "Fault occured at cap addr %lu within faulter's cspace.\n",
+           foreign_faulter_capfault_cap);
+```
+
+/*-- filter ExcludeDocs() -*/
 ```c
 /*-- filter TaskContent("fault-ipc-recv", TaskContentType.COMPLETED, subtask="getmr", completion="Fault occured at cap addr 3 within faulter's cspace.") -*/
     foreign_faulter_capfault_cap = seL4_GetMR(seL4_CapFault_Addr);
 /*-- endfilter -*/
 ```
+/*-- endfilter -*/
+
 
-### Finding out information about the generated thread fault:
+### Finding out information about the generated thread fault
 
 In the thread fault IPC message, the kernel will send information about the
 fault including the capability address whose access triggered the thread fault.
@@ -277,7 +356,7 @@ In our example here, our sample code generated a Cap Fault, so according to the
 seL4 manual, we can find out the cap fault address using at offset
 `seL4_CapFault_Addr` in the IPC message, as you see above in the code snippet.
 
-### Handling a thread fault:
+### Handling a thread fault
 
 Now that we know the cap address that generated a fault in the `faulting` thread,
 we can "handle" the fault by putting a random cap into that slot and then when
@@ -286,6 +365,28 @@ no thread fault will be generated.
 
 So here we'll copy an endpoint cap into the faulting slot:
 
+```c
+    /* Handle the fault by copying an endpoint cap into the empty slot. It
+     * doesn't matter which one: as long as we copy it in with receive rights
+     * because the faulter is going to attempt to perform an seL4_NBRecv() on
+     * it.
+     */
+
+    error = seL4_CNode_Copy(
+        faulter_cspace_root,
+        foreign_faulter_capfault_cap,
+        seL4_WordBits,
+        handler_cspace_root,
+        sequencing_ep_cap,
+        seL4_WordBits,
+        seL4_AllRights);
+
+    ZF_LOGF_IF(error != 0, PROGNAME "Failed to copy a cap into faulter's cspace to resolve the fault!");
+    printf(PROGNAME "Successfully copied a cap into foreign faulting slot.\n"
+           PROGNAME "About to resume the faulter thread.\n");
+```
+
+/*-- filter ExcludeDocs() -*/
 ```c
 /*-- filter TaskContent("fault-handle", TaskContentType.COMPLETED, subtask="copy", completion="Successfully copied a cap into foreign faulting slot.") -*/
     error = seL4_CNode_Copy(
@@ -298,25 +399,33 @@ So here we'll copy an endpoint cap into the faulting slot:
         seL4_AllRights);
 /*-- endfilter -*/
 ```
+/*-- endfilter -*/
 
-### Resuming a faulting thread:
+### Resuming a faulting thread
 
 Finally, to have the `faulter` thread wake up and try to execute again, we
 `seL4_Reply()` to it:
 
+```c
+     seL4_Reply(seL4_MessageInfo_new(0, 0, 0, 0));
+
+    printf(PROGNAME "Successfully resumed faulter thread.\n"
+           PROGNAME "Finished execution.\n");
+```
+
+/*-- filter ExcludeDocs() -*/
 ```c
 /*-- filter TaskContent("fault-resume", TaskContentType.COMPLETED, subtask="reply", completion="Faulter: Finished execution.") -*/
-    seL4_Reply(seL4_MessageInfo_new(0, 0, 0, 0));
+     seL4_Reply(seL4_MessageInfo_new(0, 0, 0, 0));
 /*-- endfilter -*/
 ```
+/*-- endfilter -*/
 
 ## Further exercises
 
 If you'd like to challenge yourself, make sure to set up the fault handling on
 both versions of the kernel: master and MCS.
 
-/*? macros.help_block() ?*/
-
 /*-- filter ExcludeDocs() -*/
 
 ```c
diff --git a/tutorials/hello-camkes-0/hello-camkes-0.md b/tutorials/hello-camkes-0/hello-camkes-0.md
index 6a1b2c11..a164b925 100644
--- a/tutorials/hello-camkes-0/hello-camkes-0.md
+++ b/tutorials/hello-camkes-0/hello-camkes-0.md
@@ -6,24 +6,25 @@
 
 /*? declare_task_ordering(['hello']) ?*/
 
-# CAmkES Tutorial: Introduction
+# Hello CAmkES
 
 This tutorial is an introduction to CAmkES. This will involve introducing the CAmkES syntax, bootstrapping a basic
 static CAmkES application and describing its components.
 
+Outcomes:
+1. Understand the structure of a CAmkES application, as a described, well-defined, static system.
+2. Understand the file-layout of a CAmkES ADL project.
+3. Become acquainted with the basics of creating a practical CAmkES application.
+
+Use this [slide presentation](https://github.com/seL4/sel4-tutorials/blob/master/docs/CAmkESTutorial.pdf) to guide you through the tutorials [0](https://docs.sel4.systems/Tutorials/hello-camkes-0), [1](https://docs.sel4.systems/Tutorials/hello-camkes-1) and [2](https://docs.sel4.systems/Tutorials/hello-camkes-2).
+
 ## Prerequisites
-1. [Set up your machine](https://docs.sel4.systems/HostDependencies#camkes-build-dependencies).
-2. [Hello world](https://docs.sel4.systems/Tutorials/hello-world)
-2. Familiarize yourself with the [CAmkES manual](https://github.com/seL4/camkes-tool/blob/master/docs/index.md).
+1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up).
+2. [Hello world tutorial](https://docs.sel4.systems/Tutorials/hello-world)
+3. Familiarise yourself with the [CAmkES manual](https://github.com/seL4/camkes-tool/blob/master/docs/index.md).
 Note that it's possible to successfully complete the CAmkES tutorial without having read the manual, however highly
 recommended.
 
-## Outcomes
-
-- Understand the structure of a CAmkES application, as a described, well-defined, static system.
-- Understand the file-layout of a CAmkES ADL project.
-- Become acquainted with the basics of creating a practical CAmkES application.
-
 ## Background
 
 The fundamentals of CAmkES are the component, the interface and the connection. Components are logical
@@ -193,7 +194,7 @@ Hello CAmkES World
 structure of ADL: it's key to understanding CAmkES. And well done on
 building and running your first CAmkES application.
 
-/*? macros.help_block() ?*/
+
 
 /*- filter ExcludeDocs() -*/
 
diff --git a/tutorials/hello-camkes-1/hello-camkes-1.md b/tutorials/hello-camkes-1/hello-camkes-1.md
index 26d6f4c6..4ba3ef8c 100644
--- a/tutorials/hello-camkes-1/hello-camkes-1.md
+++ b/tutorials/hello-camkes-1/hello-camkes-1.md
@@ -4,29 +4,37 @@
   SPDX-License-Identifier: BSD-2-Clause
 -->
 
-# CAmkES Tutorial 1
+# Introduction to CAmkES
 /*? declare_task_ordering(['hello']) ?*/
 
 This tutorial is an introduction to
 CAmkES: bootstrapping a basic static CAmkES application, describing its
 components, and linking them together.
 
-## Prerequisites
+Outcomes:
+1. Understand the structure of a CAmkES application, as a described,
+well-defined, static system.
+2. Understand the file-layout of a CAmkES ADL project.
+3. Become acquainted with the basics of creating a practical CAmkES application.
 
+Use this [slide presentation](https://github.com/seL4/sel4-tutorials/blob/master/docs/CAmkESTutorial.pdf) to guide you through the tutorials [0](https://docs.sel4.systems/Tutorials/hello-camkes-0), [1](https://docs.sel4.systems/Tutorials/hello-camkes-1) and [2](https://docs.sel4.systems/Tutorials/hello-camkes-2).
 
-1. [Set up your machine](https://docs.sel4.systems/HostDependencies#camkes-build-dependencies).
-2. [Camkes hello world](https://docs.sel4.systems/Tutorials/hello-camkes-0)
+## Prerequisites
+1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up)
+2. [CAmkES hello world tutorial](https://docs.sel4.systems/Tutorials/hello-camkes-0)
 
 ## Initialising
 
 /*? macros.tutorial_init("hello-camkes-1") ?*/
 
-## Outcomes
+<details markdown='1'>
+<summary><em>Hint:</em> tutorial solutions</summary>
+<br>
+All tutorials come with complete solutions. To get solutions run:
 
-1. Understand the structure of a CAmkES application, as a described,
-well-defined, static system.
-1. Understand the file-layout of a CAmkES ADL project.
-1. Become acquainted with the basics of creating a practical CAmkES application.
+/*? macros.tutorial_init_with_solution("hello-camkes-1") ?*/
+
+</details>
 
 ## Background
 
@@ -70,10 +78,10 @@ a communication channel then, also are well defined, and logically
 grouped so as to provide clear directional understanding of all
 transmissions over a connection. Components are connected together in
 CAmkES, yes -- but the interfaces that are exposed over each connection
-for calling by other components, are also described. 
+for calling by other components, are also described.
 
 There are different
-kinds of interfaces: 
+kinds of interfaces:
 -Dataports,
 -Procedural interfaces,
 -and Notifications.
@@ -88,7 +96,7 @@ Procedure interface may be found here:
 Find the "Procedure" keyword definition here:
 <https://github.com/seL4/camkes-tool/blob/master/docs/index.md#procedure>
 
-### Component source 
+### Component source
 
  Based on the ADL, CAmkES generates boilerplate which
 conforms to your system's architecture, and enables you to fill in the
@@ -130,8 +138,9 @@ the second one was named `a2`? Then in order to call on that second
 
 ## Exercises
 
+### Define an instance in the composition section of the ADL
 
-**Exercise** First modify `hello-1.camkes`. Define instances of `Echo` and `Client` in the 
+**Exercise** First modify `hello-1.camkes`. Define instances of `Echo` and `Client` in the
 `composition` section of the ADL.
 
 ```
@@ -139,8 +148,14 @@ the second one was named `a2`? Then in order to call on that second
 assembly {
     composition {
          component EmptyComponent empty;
-         // TODO remove the empty component, and define an Echo and a Client component
+         // TODO define an Echo and a Client component
 /*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```
 /*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="define") -*/
 assembly {
     composition {
@@ -149,20 +164,32 @@ assembly {
          component Echo echo;
 /*-- endfilter -*/
 ```
+</details>
+
+### Add a connection
 
 **Exercise** Now add a connection from `client.hello` to `echo.hello`.
 
-```
+```c
 /*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="connect") -*/
         /* hint 1: use seL4RPCCall as the connector (or you could use seL4RPC if you prefer)
          * hint 2: look at
          * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application
          */
 /*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="connect") -*/
         connection seL4RPCCall hello_con(from client.hello, to echo.hello);
 /*-- endfilter -*/
 ```
+</details>
+
+### Define an interface
 
 **Exercise** Define the interface for hello in `interfaces/HelloSimple.idl4`. 
 
@@ -175,28 +202,24 @@ procedure HelloSimple {
      * hint 2: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application
      */
 /*-- endfilter -*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```
 /*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="interface") -*/
     void say_hello(in string str);
 /*-- endfilter -*/
-/*-- endfilter -*/
-};
 ```
+</details>
 
+### Implement a RPC function
 **Exercise** Implement the RPC hello function.
 
 ```c
-/*- filter File("components/Echo/src/echo.c") --*/
-/*
- * CAmkES tutorial part 1: components with RPC. Server part.
- */
-#include <stdio.h>
-
-/* generated header for our component */
-#include <camkes.h>
-
 /*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="rpc") -*/
-/* TASK 5: implement the RPC function. */
+/* Implement the RPC function. */
 /* hint 1: the name of the function to implement is a composition of an interface name and a function name:
  * i.e.: <interface>_<function>
  * hint 2: the interfaces available are defined by the component, e.g. in hello-1.camkes
@@ -207,15 +230,58 @@ procedure HelloSimple {
  * hint 7: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application
  */
 /*-- endfilter -*/
+```
+
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```
 /*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="rpc") -*/
+/* Implement the RPC function. */
 void hello_say_hello(const char *str) {
     printf("Component %s saying: %s\n", get_instance_name(), str);
 }
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
+
+### Invoke a RPC function
 
 **Exercise** Invoke the RPC function in `components/Client/src/client.c`.
+
+```c
+/*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="hello") -*/
+    /* TODO: invoke the RPC function */
+    /* hint 1: the name of the function to invoke is a composition of an interface name and a function name:
+     * i.e.: <interface>_<function>
+     * hint 2: the interfaces available are defined by the component, e.g. in hello-1.camkes
+     * hint 3: the function name is defined by the interface definition, e.g. in interfaces/HelloSimple.idl4
+     * hint 4: so the function would be:  hello_say_hello()
+     * hint 5: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application
+     */
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```
+/*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="hello") -*/
+    /* Invoke the RPC function */
+    char *shello = "hello world";
+    hello_say_hello(shello);
+/*-- endfilter -*/
+```
+</details>
+
+## Done
+
+Now build and run the project, if it compiles: Congratulations! Be sure to read up on the keywords and
+structure of ADL: it's key to understanding CAmkES. And well done on
+writing your first CAmkES application.
+
+/*-- filter ExcludeDocs() -*/
 ```c
 /*- filter File("components/Client/src/client.c") --*/
 /*
@@ -232,41 +298,30 @@ int run(void) {
     printf("Starting the client\n");
     printf("-------------------\n");
 
-/*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="hello") -*/
-    /* TODO: invoke the RPC function */
-    /* hint 1: the name of the function to invoke is a composition of an interface name and a function name:
-     * i.e.: <interface>_<function>
-     * hint 2: the interfaces available are defined by the component, e.g. in hello-1.camkes
-     * hint 3: the function name is defined by the interface definition, e.g. in interfaces/HelloSimple.idl4
-     * hint 4: so the function would be:  hello_say_hello()
-     * hint 5: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application
-     */
-/*-- endfilter -*/
-/*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="hello") -*/
-    char *shello = "hello world";
-    hello_say_hello(shello);
-/*-- endfilter -*/
+/*? include_task_type_append([("hello", 'hello')]) ?*/
 
     printf("After the client\n");
     return 0;
 }
-
 /*-- endfilter -*/
 ```
 
-### TASK 5
- Here you define the callee-side invocation functions for
-the Hello interface exposed by Echo.
+```c
+/*- filter File("components/Echo/src/echo.c") --*/
+/*
+ * CAmkES tutorial part 1: components with RPC. Server part.
+ */
+#include <stdio.h>
 
-## Done
+/* generated header for our component */
+#include <camkes.h>
 
-Now build and run the project, if it compiles: Congratulations! Be sure to read up on the keywords and
-structure of ADL: it's key to understanding CAmkES. And well done on
-writing your first CAmkES application.
+/*? include_task_type_append([("hello", 'rpc')]) ?*/
+
+/*-- endfilter -*/
 
-/*? macros.help_block() ?*/
+```
 
-/*-- filter ExcludeDocs() -*/
 ```
 /*- filter File("hello-1.camkes") --*/
 /*
diff --git a/tutorials/hello-camkes-2/hello-camkes-2.md b/tutorials/hello-camkes-2/hello-camkes-2.md
index 1061eaf6..0017d4ed 100644
--- a/tutorials/hello-camkes-2/hello-camkes-2.md
+++ b/tutorials/hello-camkes-2/hello-camkes-2.md
@@ -6,103 +6,744 @@
 
 /*? declare_task_ordering(['hello']) ?*/
 
-# CAmkES Tutorial 2
-This tutorial is an introduction to
-CAmkES: bootstrapping a basic static CAmkES application, describing its
-components, and linking them together.
+# Events in CAmkES
+This tutorial shows how to build events in CAmkES.
+
+Learn how to:
+- Represent and implement events in CAmkES.
+- Use Dataports.
+
+Use this [slide presentation](https://github.com/seL4/sel4-tutorials/blob/master/docs/CAmkESTutorial.pdf) to guide you through the tutorials [0](https://docs.sel4.systems/Tutorials/hello-camkes-0), [1](https://docs.sel4.systems/Tutorials/hello-camkes-1) and [2](https://docs.sel4.systems/Tutorials/hello-camkes-2).
+
+## Prerequisites
+1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up)
+2. [Introduction to CAmkES tutorial](https://docs.sel4.systems/Tutorials/hello-camkes-1)
+
+
+## CapDL Loader
+
+This tutorial uses the *capDL loader*, a root task which allocates statically
+ configured objects and capabilities.
+
+<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>
 
 ## Initialising
 
 /*? macros.tutorial_init("hello-camkes-2") ?*/
 
-## Prerequisites
+<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("hello-camkes-2") ?*/
+
+</details>
+
+
+
+### Specify an events interface
+Here you're declaring the events that will be bounced
+back and forth in this tutorial. An event is a signal is sent over a
+Notification connection.
+
+You are strongly advised to read the manual section on Events here:
+<https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events>.
+
+  ''Ensure that when declaring the consumes and emits keywords between
+  the Client.camkes and Echo.camkes files, you match them up so that
+  you're not emitting on both sides of a single interface, or consuming
+  on both sides of an interface.''
+
+#### Specify an events interface
+
+```
+/*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="event-task1") -*/
+    /* TASK 1: the event interfaces */
+    /* hint 1: specify 2 interfaces: one "emits" and one "consumes"
+     * hint 2: you can use an arbitrary string as the interface type (it doesn't get used)
+     * hint 3: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events
+     */
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```
+/*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="event-task1") -*/
+    /* TASK 1: the event interfaces */
+    emits TheEvent echo;
+    consumes TheEvent client;
+/*-- endfilter -*/
+```
+
+</details>
+
+```
+/*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="event-task3") -*/
+    /* TASK 3: the event interfaces */
+    /* hint 1: specify 2 interfaces: one "emits" and one "consumes"
+     * hint 2: you can use an arbitrary string as the interface type (it doesn't get used)
+     * hint 3: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events
+     */
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
 
-1. [Set up your machine](https://docs.sel4.systems/HostDependencies). 
-2. [Camkes 1](https://docs.sel4.systems/Tutorials/hello-camkes-1)
+```
+/*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="event-task3") -*/
+    /* TASK 3: the event interfaces */
+    consumes TheEvent echo;
+    emits TheEvent client;
+/*-- endfilter -*/
+```
+</details>
+
+#### Add connections
+
+```
+/*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="event-task5") -*/
+    /* TASK 5: Event connections */
+    /* hint 1: connect each "emits" interface in a component to the "consumes" interface in the other
+     * hint 2: use seL4Notification as the connector
+     * hint 3: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events
+     */
+/*-- endfilter -*/
+```
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```
+/*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="event-task5") -*/
+    /* TASK 5: Event connections */
+    connection seL4Notification echo_event(from client.echo, to echo.echo);
+    connection seL4Notification client_event(from echo.client, to client.client);
+/*-- endfilter -*/
+```
+</details>
+
+### Data
+Recall that CAmkES prefixes the name
+of the interface instance to the function being called across that
+interface? This is the same phenomenon, but for events; in the case of a
+connection over which events are sent, there is no API, but rather
+CAmkES will generate \_emit() and \_wait() functions to enable the
+application to transparently interact with these events.
+
+#### Signal that the data is available
+
+```
+/*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="signal-task10") -*/
+    /* TASK 10: emit event to signal that the data is available */
+    /* hint 1: use the function <interface_name>_emit
+    * hint 2: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events
+    */
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
+/*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="signal-task10") -*/
+    /* TASK 10: emit event to signal that the data is available */
+    echo_emit();
+/*-- endfilter -*/
+```
+</details>
+
+#### Wait for data to become available
+```
+/*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="wait-task11") -*/
+    /* TASK 11: wait to get an event back signalling that the reply data is available */
+    /* hint 1: use the function <interface_name>_wait
+     * hint 2: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events
+     */
+/*-- endfilter -*/
+```
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
+/*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="wait-task11") -*/
+    /* TASK 11: wait to get an event back signalling that the reply data is available */
+    client_wait();
+/*-- endfilter -*/
+```
+</details>
 
-## Learning outcomes
+#### Signal that data is available
 
+```c
+/*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="emit-task14") -*/
+    /* TASK 14: emit event to signal that the data is available */
+    /* hint 1: we've already done this before */
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
+/*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="emit-task14") -*/
+    /* TASK 14: emit event to signal that the data is available */
+    echo_emit();
+/*-- endfilter -*/
+```
+</details>
+
+#### Wait for data to be read
+
+```c
+/*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="wait-task15") -*/
+    /* TASK 15: wait to get an event back signalling that data has been read */
+    /* hint 1: we've already done this before */
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
+/*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="wait-task15") -*/
+    /* TASK 15: wait to get an event back signalling that data has been read */
+    client_wait();
+/*-- endfilter -*/
+```
+</details>
+
+#### Signal that data is available
+```c
+/*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="notify-task22") -*/
+    /* TASK 22: notify the client that there is new data available for it */
+    /* hint 1: use the function <interface_name>_emit
+    * hint 2: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events
+    */
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
+/*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="notify-task22") -*/
+    /* TASK 22: notify the client that there is new data available for it */
+    client_emit();
+/*-- endfilter -*/
+```
+</details>
+
+#### Signal that data has been read
+
+```c
+/*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="notify-task25") -*/
+    /* TASK 25: notify the client that we are done reading the data */
+    /* hint 1: use the function <interface_name>_emit
+    * hint 2: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events
+    */
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
+/*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="notify-task25") -*/
+    /* TASK 25: notify the client that we are done reading the data */
+    client_emit();
+/*-- endfilter -*/
+```
+</details>
+
+### Handle notifications
+One way to handle notifications in CAmkES is to
+use callbacks when they are raised. CAmkES generates functions that
+handle the registration of callbacks for each notification interface
+instance. These steps help you to become familiar with this approach.
+
+#### Register a callback handler
+
+```c
+/*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="register-task18") -*/
+    /* TASK 18: register the first callback handler for this interface */
+    /* hint 1: use the function <interface name>_reg_callback()
+     * hint 2: register the function "callback_handler_1"
+     * hint 3: pass NULL as the extra argument to the callback
+     * hint 4: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events
+     */
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
+/*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="register-task18") -*/
+    /* TASK 18: register the first callback handler for this interface */
+    int error = echo_reg_callback(callback_handler_1, NULL);
+    ZF_LOGF_IF(error != 0, "Failed to register callback");
+/*-- endfilter -*/
+```
+</details>
+
+#### Register another callback handler
+
+```c
+/*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="register-task21") -*/
+  /* TASK 21: register the second callback for this event. */
+  /* hint 1: use the function <interface name>_reg_callback()
+    * hint 2: register the function "callback_handler_2"
+    * hint 3: pass NULL as the extra argument to the callback
+    * hint 4: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events
+    */
+/*-- endfilter -*/
+```
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
+/*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="register-task21") -*/
+    /* TASK 21: register the second callback for this event. */
+    int error = echo_reg_callback(callback_handler_2, NULL);
+    ZF_LOGF_IF(error != 0, "Failed to register callback");
+/*-- endfilter -*/
+```
+</details>
+
+#### Register a callback handler
+
+```c
+/*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="register-task24") -*/
+  /* TASK 24: register the original callback handler for this event */
+    /* hint 1: use the function <interface name>_reg_callback()
+     * hint 2: register the function "callback_handler_1"
+     * hint 3: pass NULL as the extra argument to the callback
+     * hint 4: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events
+     */
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
+/*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="register-task24") -*/
+    /* TASK 24: register the original callback handler for this event */
+    int error = echo_reg_callback(callback_handler_1, NULL);
+    ZF_LOGF_IF(error != 0, "Failed to register callback");
+/*-- endfilter -*/
+```
+</details>
+
+------------------------------------------------------------------------
+
+### Dataports
+Dataports are typed shared memory mappings. In your
+CAmkES ADL specification, you state what C data type you'll be using to
+access the data in the shared memory -- so you can specify a C struct
+type, etc.
+
+The really neat part is more that CAmkES provides access control for
+accessing these shared memory mappings: if a shared mem mapping is such
+that one party writes and the other reads and never writes, we can tell
+CAmkES about this access constraint in ADL.
+
+So in TASKs 2 and 4, you're first being led to create the "Dataport"
+interface instances on each of the components that will be participating
+in the shared mem communication. We will then link them together using a
+"seL4SharedData" connector later on.
+
+#### Specify dataport interfaces
+```
+/*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="dataport-task2") -*/
+    /* TASK 2: the dataport interfaces */
+    /* hint 1: specify 3 interfaces: one of type "Buf", one of type "str_buf_t" and one of type "ptr_buf_t"
+     * hint 2: for the definition of these types see "str_buf.h".
+     * hint 3: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports
+     */
+ /*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```
+/*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="dataport-task2") -*/
+    /* TASK 2: the dataport interfaces */
+    dataport Buf d;
+    dataport str_buf_t d_typed;
+    dataport ptr_buf_t d_ptrs;
+/*-- endfilter -*/
+```
+
+</details>
+
+#### Specify dataport interfaces
+```
+/*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="dataport-task4") -*/
+    /* TASK 4: the dataport interfaces */
+    /* hint 1: specify 3 interfaces: one of type "Buf", one of type "str_buf_t" and one of type "ptr_buf_t"
+     * hint 3: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports
+     */
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```
+/*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="dataport-task4") -*/
+    /* TASK 4: the dataport interfaces */
+    dataport Buf d;
+    dataport str_buf_t d_typed;
+    dataport ptr_buf_t d_ptrs;
+/*-- endfilter -*/
+```
+</details>
+
+### Dataport connections
+And here we are: we're about to specify connections
+between the shared memory pages in each client, and tell CAmkES to link
+these using shared underlying Frame objects. Fill out this step, and
+proceed.
+
+#### Specify dataport connections
+
+```
+/*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="dataport-task6") -*/
+    /* TASK 6: Dataport connections */
+    /* hint 1: connect the corresponding dataport interfaces of the components to each other
+    * hint 2: use seL4SharedData as the connector
+    * hint 3: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports
+    */
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```
+/*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="dataport-task6") -*/
+    /* TASK 6: Dataport connections */
+    connection seL4SharedData data_conn(from client.d, to echo.d);
+    connection seL4SharedData typed_data_conn(from client.d_typed, to echo.d_typed);
+    connection seL4SharedData ptr_data_conn(from client.d_ptrs, to echo.d_ptrs);
+/*-- endfilter -*/
+```
+</details>
+
+### Access and manipulate share memory mapping (Dataport) of the client
+These steps are asking you to write some C code
+to access and manipulate the data in the shared memory mapping
+(Dataport) of the client. Follow through to the next step.
+
+#### Copy strings to an untyped dataport
+```c
+/*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="copy-task9") -*/
+    /* TASK 9: copy strings to an untyped dataport */
+    /* hint 1: use the "Buf" dataport as defined in the Client.camkes file
+     * hint 2: to access the dataport use the interface name as defined in Client.camkes.
+     * For example if you defined it as "dataport Buf d" then you would use "d" to refer to the dataport in C.
+     * hint 3: first write the number of strings (NUM_STRINGS) to the dataport
+     * hint 4: then copy all the strings from "s_arr" to the dataport.
+     * hint 5: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports
+     */
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
+/*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="copy-task9") -*/
+    /* TASK 9: copy strings to an untyped dataport */
+    int *n = (int*)d;
+    *n = NUM_STRINGS;
+    char *str = (char*)(n + 1);
+    for (int i = 0; i < NUM_STRINGS; i++) {
+        strcpy(str, s_arr[i]);
+        str += strlen(str) + 1;
+    }
+/*-- endfilter -*/
+```
+</details>
+
+#### Read the reply data from a typed dataport
+```
+/*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="read-task12") -*/
+    /* TASK 12: read the reply data from a typed dataport */
+    /* hint 1: use the "str_buf_t" dataport as defined in the Client.camkes file
+     * hint 2: to access the dataport use the interface name as defined in Client.camkes.
+     * For example if you defined it as "dataport str_buf_t d_typed" then you would use "d_typed" to refer to the dataport in C.
+     * hint 3: for the definition of "str_buf_t" see "str_buf.h".
+     * hint 4: use the "n" field to determine the number of strings in the dataport
+     * hint 5: print out the specified number of strings from the "str" field
+     * hint 6: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports
+     */
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```
+/*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="read-task12") -*/
+    /* TASK 12: read the reply data from a typed dataport */
+    for (int i = 0; i < d_typed->n; i++) {
+        printf("%s: string %d (%p): \"%s\"\n", get_instance_name(), i, d_typed->str[i], d_typed->str[i]);
+    }
+/*-- endfilter -*/
+```
+</details>
+
+#### Send data using dataports
+
+```
+/*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="send-task13") -*/
+  /* TASK 13: send the data over again, this time using two dataports, one
+     * untyped dataport containing the data, and one typed dataport containing
+     * dataport pointers pointing to data in the untyped, dataport.
+     */
+    /* hint 1: for the untyped dataport use the "Buf" dataport as defined in the Client.camkes file
+     * hint 2: for the typed dataport use the "ptr_buf_t" dataport as defined in the Client.camkes file
+     * hint 3: for the definition of "ptr_buf_t" see "str_buf.h".
+     * hint 4: copy all the strings from "s_arr" into the untyped dataport
+     * hint 5: use the "n" field of the typed dataport to specify the number of dataport pointers (NUM_STRINGS)
+     * hint 6: use the "ptr" field of the typed dataport to store the dataport pointers
+     * hint 7: use the function "dataport_wrap_ptr()" to create a dataport pointer from a regular pointer
+     * hint 8: the dataport pointers should point into the untyped dataport
+     * hint 9: for more information about dataport pointers see: https://github.com/seL4/camkes-tool/blob/master/docs/index.md
+     */
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
+/*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="send-task13") -*/
+    /* TASK 13: send the data over again, this time using two dataports, one
+     * untyped dataport containing the data, and one typed dataport containing
+     * dataport pointers pointing to data in the untyped, dataport.
+     */
+    d_ptrs->n = NUM_STRINGS;
+    str = (char*)d;
+    for (int i = 0; i < NUM_STRINGS; i++) {
+        strcpy(str, s_arr[i]);
+        d_ptrs->ptr[i] = dataport_wrap_ptr(str);
+        str += strlen(str) + 1;
+    }
+/*-- endfilter -*/
+```
+</details>
+
+### Access and manipulate share memory mapping (Dataport) of the server
+And these steps are asking you to write some C
+code to access and manipulate the data in the shared memory mapping
+(Dataport) of the server.
+
+#### Read data from an untyped dataport
+```c
+/*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="read-task19") -*/
+  /* TASK 19: read some data from the untyped dataport */
+  /* hint 1: use the "Buf" dataport as defined in the Echo.camkes file
+    * hint 2: to access the dataport use the interface name as defined in Echo.camkes.
+    * For example if you defined it as "dataport Buf d" then you would use "d" to refer to the dataport in C.
+    * hint 3: first read the number of strings from the dataport
+    * hint 4: then print each string from the dataport
+    * hint 5: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports
+    */
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
+/*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="read-task19") -*/
+    /* TASK 19: read some data from the untyped dataport */
+    int *n = (int*)d;
+    char *str = (char*)(n + 1);
+    for (int i = 0; i < *n; i++) {
+      printf("%s: saying (%p): \"%s\"\n", get_instance_name(), str, str);
+      str += strlen(str) + 1;
+    }
+/*-- endfilter -*/
+```
+</details>
+
+#### Put data into a typed dataport
+
+```c
+/*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="put-task20") -*/
+  /* TASK 20: put a modified copy of the data from the untyped dataport into the typed dataport */
+    /* hint 1: modify each string by making it upper case, use the function "uppercase"
+     * hint 2: read from the "Buf" dataport as above
+     * hint 3: write to the "str_buf_t" dataport as defined in the Echo.camkes file
+     * hint 4: to access the dataport use the interface name as defined in Echo.camkes.
+     * For example if you defined it as "dataport str_buf_t d_typed" then you would use "d_typed" to refer to the dataport in C.
+     * hint 5: for the definition of "str_buf_t" see "str_buf.h"
+     * hint 6: use the "n" field to specify the number of strings in the dataport
+     * hint 7: copy the specified number of strings from the "Buf" dataport to the "str" field
+     * hint 8: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports
+     * hint 9: you could combine this TASK with the previous one in a single loop if you want
+     */
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
+/*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="put-task20") -*/
+  /* TASK 20: put a modified copy of the data from the untyped dataport into the typed dataport */
+    n = (int*)d;
+    str = (char*)(n + 1);
+    for (int i = 0, j = *n - 1; i < *n; i++, j--) {
+        strncpy(d_typed->str[j], str, STR_LEN);
+        uppercase(d_typed->str[j]);
+        str += strlen(str) + 1;
+    }
+    d_typed->n = *n;
+/*-- endfilter -*/
+```
+</details>
 
-- Understand how to represent and implement events in CAmkES.
-- Understand how to use Dataports.
+#### Read data from a typed dataport
 
-## Walkthrough
- Bear in mind, this article will be going through the
-tutorial steps in the order that the user is led through them in the
-slide presentation, except where several similar tasks are coalesced to
-avoid duplication. Additionally, if a tasks step covers material that
-has already been touched on, it will be omitted from this article.
+```c
+/*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="read-task23") -*/
+  /* TASK 23: read some data from the dataports. specifically:
+    * read a dataport pointer from one of the typed dataports, then use
+    * that pointer to access data in the untyped dataport.
+    */
+  /* hint 1: for the untyped dataport use the "Buf" dataport as defined in the Echo.camkes file
+    * hint 2: for the typed dataport use the "ptr_buf_t" dataport as defined in the Echo.camkes file
+    * hint 3: for the definition of "ptr_buf_t" see "str_buf.h".
+    * hint 4: the "n" field of the typed dataport specifies the number of dataport pointers
+    * hint 5: the "ptr" field of the typed dataport contains the dataport pointers
+    * hint 6: use the function "dataport_unwrap_ptr()" to create a regular pointer from a dataport pointer
+    * hint 7: for more information about dataport pointers see: https://github.com/seL4/camkes-tool/blob/master/docs/index.md
+    * hint 8: print out the string pointed to by each dataport pointer
+    */
+/*-- endfilter -*/
+```
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
 
-### TASK 1
- Here you're declaring the events that will be bounced
-back and forth in this tutorial. An event is a signal is sent over a
-Notification connection.
+```c
+/*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="read-task23") -*/
+  /* TASK 23: read some data from the dataports. specifically:
+    * read a dataport pointer from one of the typed dataports, then use
+    * that pointer to access data in the untyped dataport.
+    */
+  char *str;
+  for (int i = 0; i < d_ptrs->n; i++) {
+      str = dataport_unwrap_ptr(d_ptrs->ptr[i]);
+      printf("%s: dptr saying (%p): \"%s\"\n", get_instance_name(), str, str);
+  }
+/*-- endfilter -*/
+```
+</details>
 
-You are strongly advised to read the manual section on Events here:
-<https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events>.
+### CAmkES attributes
+This is an introduction to CAmkES attributes: you're
+being asked to set the priority of the components.
 
-  ''Ensure that when declaring the consumes and emits keywords between
-  the Client.camkes and Echo.camkes files, you match them up so that
-  you're not emitting on both sides of a single interface, or consuming
-  on both sides of an interface.''
+#### Set component priorities
 
-### TASK 10, 11, 14, 15, 22, 25
- Recall that CAmkES prefixes the name
-of the interface instance to the function being called across that
-interface? This is the same phenomenon, but for events; in the case of a
-connection over which events are sent, there is no API, but rather
-CAmkES will generate \_emit() and \_wait() functions to enable the
-application to transparently interact with these events.
+```
+/*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="set-task7") -*/
+    /* TASK 7: set component priorities */
+    /* hint 1: component priority is specified as an attribute with the name <component name>.priority
+    * hint 2: the highest priority is represented by 255, the lowest by 0
+    */
+/*-- endfilter -*/
+```
 
-### TASK 18, 21, 24
- One way to handle notifications in CAmkES is to
-use callbacks when they are raised. CAmkES generates functions that
-handle the registration of callbacks for each notification interface
-instance. These steps help you to become familiar with this approach.
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
 
-------------------------------------------------------------------------
+```
+/*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="set-task7") -*/
+    /* TASK 7: set component priorities */
+    client.priority = 255;
+    echo.priority = 254;
+/*-- endfilter -*/
+```
+</details>
 
-### TASK 2, 4
- Dataports are typed shared memory mappings. In your
-CAmkES ADL specification, you state what C data type you'll be using to
-access the data in the shared memory -- so you can specify a C struct
-type, etc.
+### Specify the data access constraints for Dataports
+This is where we specify the data access constraints
+for the Dataports in a shared memory connection. We then go about
+attempting to violate those constraints to see how CAmkES has truly met
+our constraints when mapping those Dataports.
 
-The really neat part is more that CAmkES provides access control for
-accessing these shared memory mappings: if a shared mem mapping is such
-that one party writes and the other reads and never writes, we can tell
-CAmkES about this access constraint in ADL.
+#### Restrict access to dataports
 
-So in TASKs 2 and 4, you're first being led to create the "Dataport"
-interface instances on each of the components that will be participating
-in the shared mem communication. We will then link them together using a
-"seL4SharedData" connector later on.
+```
+/*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="restrict-task8") -*/
+    /* TASK 8: restrict access to dataports */
+    /* hint 1: use attribute <component>.<interface_name>_access for each component and interface
+    * hint 2: appropriate values for the to_access and from_access attributes are: "R" or "W"
+    * hint 4: make the "Buf" dataport read only for the Echo component
+    * hint 3: make the "str_buf_t" dataport read only for the Client component
+    */
+/*-- endfilter -*/
+```
 
-### TASK 6
- And here we are: we're about to specify connections
-between the shared memory pages in each client, and tell CAmkES to link
-these using shared underlying Frame objects. Fill out this step, and
-proceed.
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
 
-### TASK 9, 12, 13
- These steps are asking you to write some C code
-to access and manipulate the data in the shared memory mapping
-(Dataport) of the client. Follow through to the next step.
+```
+/*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="restrict-task8") -*/
+    /* TASK 8: restrict access to dataports */
+    echo.d_access = "R";
+    client.d_access = "W";
+    echo.d_typed_access = "W";
+    client.d_typed_access = "R";
+/*-- endfilter -*/
+```
+</details>
 
-### TASK 19, 20, 23
- And these steps are asking you to write some C
-code to access and manipulate the data in the shared memory mapping
-(Dataport) of the server.
+#### Test the read and write permissions on the dataport
+```
+/*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="test-task16") -*/
+    /* TASK 16: test the read and write permissions on the dataport.
+    * When we try to write to a read-only dataport, we will get a VM fault.
+    */
+    /* hint 1: try to assign a value to a field of the "str_buf_t" dataport */
+/*-- endfilter -*/
+```
 
-### TASK 7
- This is an introduction to CAmkES attributes: you're
-being asked to set the priority of the components.
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
 
-### TASK 8, 16
- This is where we specify the data access constraints
-for the Dataports in a shared memory connection. We then go about
-attempting to violate those constraints to see how CAmkES has truly met
-our constraints when mapping those Dataports.
+```
+/*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="test-task16") -*/
+    /* TASK 16: test the read and write permissions on the dataport.
+    * When we try to write to a read-only dataport, we will get a VM fault.
+    */
+    d_typed->n = 0;
+/*-- endfilter -*/
+```
+</details>
 
 ## Done!
  Congratulations: be sure to read up on the keywords and
@@ -110,7 +751,7 @@ structure of ADL: it's key to understanding CAmkES. And well done on
 writing your first CAmkES application.
 
 
-/*? macros.help_block() ?*/
+
 
 /*-- filter ExcludeDocs() -*/
 ```c
@@ -123,31 +764,14 @@ component Client {
     /* this component has a control thread */
     control;
 
-    /* TASK 1: the event interfaces */
-    /* hint 1: specify 2 interfaces: one "emits" and one "consumes"
-     * hint 2: you can use an arbitrary string as the interface type (it doesn't get used)
-     * hint 3: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events
-     */
-/*- if solution -*/
-    emits TheEvent echo;
-    consumes TheEvent client;
-/*- endif -*/
-
-    /* TASK 2: the dataport interfaces */
-    /* hint 1: specify 3 interfaces: one of type "Buf", one of type "str_buf_t" and one of type "ptr_buf_t"
-     * hint 2: for the definition of these types see "str_buf.h".
-     * hint 3: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports
-     */
-/*- if solution -*/
-    dataport Buf d;
-    dataport str_buf_t d_typed;
-    dataport ptr_buf_t d_ptrs;
-/*- endif -*/
-}
+/*? include_task_type_append([("hello","event-task1")]) ?*/
 
+/*? include_task_type_append([("hello","dataport-task2")]) ?*/
 
+}
 /*-- endfilter -*/
 ```
+
 ```c
 /*- filter File("components/Echo/Echo.camkes") --*/
 
@@ -155,25 +779,10 @@ component Echo {
     /* include definitions of typedefs for the dataports */
     include "str_buf.h";
 
-    /* TASK 3: the event interfaces */
-    /* hint 1: specify 2 interfaces: one "emits" and one "consumes"
-     * hint 2: you can use an arbitrary string as the interface type (it doesn't get used)
-     * hint 3: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events
-     */
-/*- if solution -*/
-    consumes TheEvent echo;
-    emits TheEvent client;
-/*- endif -*/
+/*? include_task_type_append([("hello","event-task3")]) ?*/
+
+/*? include_task_type_append([("hello","dataport-task4")]) ?*/
 
-    /* TASK 4: the dataport interfaces */
-    /* hint 1: specify 3 interfaces: one of type "Buf", one of type "str_buf_t" and one of type "ptr_buf_t"
-     * hint 3: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports
-     */
-/*- if solution -*/
-    dataport Buf d;
-    dataport str_buf_t d_typed;
-    dataport ptr_buf_t d_ptrs;
-/*- endif -*/
 }
 
 
@@ -197,50 +806,16 @@ assembly {
         component Client client;
         component Echo echo;
 
-        /* TASK 5: Event connections */
-        /* hint 1: connect each "emits" interface in a component to the "consumes" interface in the other
-         * hint 2: use seL4Notification as the connector
-         * hint 3: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events
-         */
-/*- if solution -*/
-        connection seL4Notification echo_event(from client.echo, to echo.echo);
-        connection seL4Notification client_event(from echo.client, to client.client);
-/*- endif -*/
-
-        /* TASK 6: Dataport connections */
-        /* hint 1: connect the corresponding dataport interfaces of the components to each other
-         * hint 2: use seL4SharedData as the connector
-         * hint 3: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports
-         */
-/*- if solution -*/
-        connection seL4SharedData data_conn(from client.d, to echo.d);
-        connection seL4SharedData typed_data_conn(from client.d_typed, to echo.d_typed);
-        connection seL4SharedData ptr_data_conn(from client.d_ptrs, to echo.d_ptrs);
-/*- endif -*/
+/*? include_task_type_append([("hello","event-task5")]) ?*/
+
+/*? include_task_type_append([("hello","dataport-task6")]) ?*/
 
     }
     configuration {
-        /* TASK 7: set component priorities */
-        /* hint 1: component priority is specified as an attribute with the name <component name>.priority
-         * hint 2: the highest priority is represented by 255, the lowest by 0
-         */
-/*- if solution -*/
-        client.priority = 255;
-        echo.priority = 254;
-/*- endif -*/
-
-        /* TASK 8: restrict access to dataports */
-        /* hint 1: use attribute <component>.<interface_name>_access for each component and interface
-         * hint 2: appropriate values for the to_access and from_access attributes are: "R" or "W"
-         * hint 4: make the "Buf" dataport read only for the Echo component
-         * hint 3: make the "str_buf_t" dataport read only for the Client component
-         */
-/*- if solution -*/
-        echo.d_access = "R";
-        client.d_access = "W";
-        echo.d_typed_access = "W";
-        client.d_typed_access = "R";
-/*- endif -*/
+/*? include_task_type_append([("hello","set-task7")]) ?*/
+
+/*? include_task_type_append([("hello","restrict-task8")]) ?*/
+
     }
 }
 
@@ -301,100 +876,23 @@ char *s_arr[NUM_STRINGS] = { "hello", "world", "how", "are", "you?" };
 int run(void) {
     printf("%s: Starting the client\n", get_instance_name());
 
-    /* TASK 9: copy strings to an untyped dataport */
-    /* hint 1: use the "Buf" dataport as defined in the Client.camkes file
-     * hint 2: to access the dataport use the interface name as defined in Client.camkes.
-     * For example if you defined it as "dataport Buf d" then you would use "d" to refer to the dataport in C.
-     * hint 3: first write the number of strings (NUM_STRINGS) to the dataport
-     * hint 4: then copy all the strings from "s_arr" to the dataport.
-     * hint 5: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports
-     */
-/*- if solution -*/
-    int *n = (int*)d;
-    *n = NUM_STRINGS;
-    char *str = (char*)(n + 1);
-    for (int i = 0; i < NUM_STRINGS; i++) {
-        strcpy(str, s_arr[i]);
-        str += strlen(str) + 1;
-    }
-/*- endif -*/
+/*? include_task_type_append([("hello","copy-task9")]) ?*/
 
-    /* TASK 10: emit event to signal that the data is available */
-    /* hint 1: use the function <interface_name>_emit
-     * hint 2: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events
-     */
-/*- if solution -*/
-    echo_emit();
-/*- endif -*/
+/*? include_task_type_append([("hello","signal-task10")]) ?*/
 
-    /* TASK 11: wait to get an event back signalling that the reply data is avaialble */
-    /* hint 1: use the function <interface_name>_wait
-     * hint 2: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events
-     */
-/*- if solution -*/
-    client_wait();
-/*- endif -*/
+/*? include_task_type_append([("hello","wait-task11")]) ?*/
 
-    /* TASK 12: read the reply data from a typed dataport */
-    /* hint 1: use the "str_buf_t" dataport as defined in the Client.camkes file
-     * hint 2: to access the dataport use the interface name as defined in Client.camkes.
-     * For example if you defined it as "dataport str_buf_t d_typed" then you would use "d_typed" to refer to the dataport in C.
-     * hint 3: for the definition of "str_buf_t" see "str_buf.h".
-     * hint 4: use the "n" field to determine the number of strings in the dataport
-     * hint 5: print out the specified number of strings from the "str" field
-     * hint 6: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports
-     */
-/*- if solution -*/
-    for (int i = 0; i < d_typed->n; i++) {
-        printf("%s: string %d (%p): \"%s\"\n", get_instance_name(), i, d_typed->str[i], d_typed->str[i]);
-    }
-/*- endif -*/
+/*? include_task_type_append([("hello","read-task12")]) ?*/
 
-    /* TASK 13: send the data over again, this time using two dataports, one
-     * untyped dataport containing the data, and one typed dataport containing
-     * dataport pointers pointing to data in the untyped, dataport.
-     */
-    /* hint 1: for the untyped dataport use the "Buf" dataport as defined in the Client.camkes file
-     * hint 2: for the typed dataport use the "ptr_buf_t" dataport as defined in the Client.camkes file
-     * hint 3: for the definition of "ptr_buf_t" see "str_buf.h".
-     * hint 4: copy all the strings from "s_arr" into the untyped dataport
-     * hint 5: use the "n" field of the typed dataport to specify the number of dataport pointers (NUM_STRINGS)
-     * hint 6: use the "ptr" field of the typed dataport to store the dataport pointers
-     * hint 7: use the function "dataport_wrap_ptr()" to create a dataport pointer from a regular pointer
-     * hint 8: the dataport pointers should point into the untyped dataport
-     * hint 9: for more information about dataport pointers see: https://github.com/seL4/camkes-tool/blob/master/docs/index.md
-     */
-/*- if solution -*/
-    d_ptrs->n = NUM_STRINGS;
-    str = (char*)d;
-    for (int i = 0; i < NUM_STRINGS; i++) {
-        strcpy(str, s_arr[i]);
-        d_ptrs->ptr[i] = dataport_wrap_ptr(str);
-        str += strlen(str) + 1;
-    }
-/*- endif -*/
+/*? include_task_type_append([("hello","send-task13")]) ?*/
 
-    /* TASK 14: emit event to signal that the data is available */
-    /* hint 1: we've already done this before */
-/*- if solution -*/
-    echo_emit();
-/*- endif -*/
+/*? include_task_type_append([("hello","emit-task14")]) ?*/
 
-    /* TASK 15: wait to get an event back signalling that data has been read */
-    /* hint 1: we've already done this before */
-/*- if solution -*/
-    client_wait();
-/*- endif -*/
+/*? include_task_type_append([("hello","wait-task15")]) ?*/
 
     printf("%s: the next instruction will cause a vm fault due to permissions\n", get_instance_name());
 
-    /* TASK 16: test the read and write permissions on the dataport.
-     * When we try to write to a read-only dataport, we will get a VM fault.
-     */
-    /* hint 1: try to assign a value to a field of the "str_buf_t" dataport */
-/*- if solution -*/
-    d_typed->n = 0;
-/*- endif -*/
+/*? include_task_type_append([("hello","test-task16")]) ?*/
 
     return 0;
 }
@@ -437,64 +935,15 @@ void callback_handler_2(void *a);
  * also register a different handler.
  */
 void callback_handler_1(void *a) {
-    /* TASK 19: read some data from the untyped dataport */
-    /* hint 1: use the "Buf" dataport as defined in the Echo.camkes file
-     * hint 2: to access the dataport use the interface name as defined in Echo.camkes.
-     * For example if you defined it as "dataport Buf d" then you would use "d" to refer to the dataport in C.
-     * hint 3: first read the number of strings from the dataport
-     * hint 4: then print each string from the dataport
-     * hint 5: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports
-     */
-/*- if solution -*/
-    int *n = (int*)d;
-    char *str = (char*)(n + 1);
-    for (int i = 0; i < *n; i++) {
-        printf("%s: saying (%p): \"%s\"\n", get_instance_name(), str, str);
-        str += strlen(str) + 1;
-    }
-/*- endif -*/
 
-    /* TASK 20: put a modified copy of the data from the untyped dataport into the typed dataport */
-    /* hint 1: modify each string by making it upper case, use the function "uppercase"
-     * hint 2: read from the "Buf" dataport as above
-     * hint 3: write to the "str_buf_t" dataport as defined in the Echo.camkes file
-     * hint 4: to access the dataport use the interface name as defined in Echo.camkes.
-     * For example if you defined it as "dataport str_buf_t d_typed" then you would use "d_typed" to refer to the dataport in C.
-     * hint 5: for the definition of "str_buf_t" see "str_buf.h"
-     * hint 6: use the "n" field to specify the number of strings in the dataport
-     * hint 7: copy the specified number of strings from the "Buf" dataport to the "str" field
-     * hint 8: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-dataports
-     * hint 9: you could combine this TASK with the previous one in a single loop if you want
-     */
-/*- if solution -*/
-    n = (int*)d;
-    str = (char*)(n + 1);
-    for (int i = 0, j = *n - 1; i < *n; i++, j--) {
-        strncpy(d_typed->str[j], str, STR_LEN);
-        uppercase(d_typed->str[j]);
-        str += strlen(str) + 1;
-    }
-    d_typed->n = *n;
-/*- endif -*/
+/*? include_task_type_append([("hello","read-task19")]) ?*/
 
-    /* TASK 21: register the second callback for this event. */
-    /* hint 1: use the function <interface name>_reg_callback()
-     * hint 2: register the function "callback_handler_2"
-     * hint 3: pass NULL as the extra argument to the callback
-     * hint 4: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events
-     */
-/*- if solution -*/
-    int error = echo_reg_callback(callback_handler_2, NULL);
-    ZF_LOGF_IF(error != 0, "Failed to register callback");
-/*- endif -*/
+/*? include_task_type_append([("hello","put-task20")]) ?*/
+
+/*? include_task_type_append([("hello","register-task21")]) ?*/
+
+/*? include_task_type_append([("hello","notify-task22")]) ?*/
 
-    /* TASK 22: notify the client that there is new data available for it */
-    /* hint 1: use the function <interface_name>_emit
-     * hint 2: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events
-     */
-/*- if solution -*/
-    client_emit();
-/*- endif -*/
 }
 
 /* this callback handler is meant to be invoked the second time an event
@@ -506,45 +955,13 @@ void callback_handler_1(void *a) {
  * also register a different handler.
  */
 void callback_handler_2(void *a) {
-    /* TASK 23: read some data from the dataports. specifically:
-     * read a dataport pointer from one of the typed dataports, then use
-     * that pointer to access data in the untyped dataport.
-     */
-    /* hint 1: for the untyped dataport use the "Buf" dataport as defined in the Echo.camkes file
-     * hint 2: for the typed dataport use the "ptr_buf_t" dataport as defined in the Echo.camkes file
-     * hint 3: for the definition of "ptr_buf_t" see "str_buf.h".
-     * hint 4: the "n" field of the typed dataport specifies the number of dataport pointers
-     * hint 5: the "ptr" field of the typed dataport contains the dataport pointers
-     * hint 6: use the function "dataport_unwrap_ptr()" to create a regular pointer from a dataport pointer
-     * hint 7: for more information about dataport pointers see: https://github.com/seL4/camkes-tool/blob/master/docs/index.md
-     * hint 8: print out the string pointed to by each dataport pointer
-     */
-/*- if solution -*/
-    char *str;
-    for (int i = 0; i < d_ptrs->n; i++) {
-        str = dataport_unwrap_ptr(d_ptrs->ptr[i]);
-        printf("%s: dptr saying (%p): \"%s\"\n", get_instance_name(), str, str);
-    }
-/*- endif -*/
 
-    /* TASK 24: register the original callback handler for this event */
-    /* hint 1: use the function <interface name>_reg_callback()
-     * hint 2: register the function "callback_handler_1"
-     * hint 3: pass NULL as the extra argument to the callback
-     * hint 4: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events
-     */
-/*- if solution -*/
-    int error = echo_reg_callback(callback_handler_1, NULL);
-    ZF_LOGF_IF(error != 0, "Failed to register callback");
-/*- endif -*/
+/*? include_task_type_append([("hello","read-task23")]) ?*/
+
+/*? include_task_type_append([("hello","register-task24")]) ?*/
+
+/*? include_task_type_append([("hello","notify-task25")]) ?*/
 
-    /* TASK 25: notify the client that we are done reading the data */
-    /* hint 1: use the function <interface_name>_emit
-     * hint 2: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events
-     */
-/*- if solution -*/
-    client_emit();
-/*- endif -*/
 }
 
 /* this function is invoked to initialise the echo event interface before it
@@ -554,16 +971,7 @@ void callback_handler_2(void *a) {
  * For example if you defined it as "consumes TheEvent c_event" then you would use "c_event".
  */
 void echo__init(void) {
-    /* TASK 18: register the first callback handler for this interface */
-    /* hint 1: use the function <interface name>_reg_callback()
-     * hint 2: register the function "callback_handler_1"
-     * hint 3: pass NULL as the extra argument to the callback
-     * hint 4: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#an-example-of-events
-     */
-/*- if solution -*/
-    int error = echo_reg_callback(callback_handler_1, NULL);
-    ZF_LOGF_IF(error != 0, "Failed to register callback");
-/*- endif -*/
+/*? include_task_type_append([("hello","register-task18")]) ?*/
 }
 
 
@@ -604,4 +1012,4 @@ GenerateCAmkESRootserver()
 /*? macros.cmake_check_script(state) ?*/
 /*-- endfilter -*/
 ```
-/*-- endfilter -*/
+/*-- endfilter -*/
\ No newline at end of file
diff --git a/tutorials/hello-camkes-timer/CMakeLists.txt b/tutorials/hello-camkes-timer/CMakeLists.txt
index 6bcd29da..a365a8f2 100644
--- a/tutorials/hello-camkes-timer/CMakeLists.txt
+++ b/tutorials/hello-camkes-timer/CMakeLists.txt
@@ -43,8 +43,5 @@ DeclareCAmkESComponent(EmptyComponent)
 DeclareCAmkESRootserver(hello-camkes-timer.camkes)
 
 GenerateCAmkESRootserver()
-/*? declare_task_ordering(['1']) ?*/
 
-/*- filter TaskContent("1", TaskContentType.BEFORE, completion="Booting all finished, dropped to user space") -*//*- endfilter -*/
-/*- filter TaskContent("1", TaskContentType.COMPLETED, completion="After the client: wakeup") -*//*- endfilter -*/
-/*? macros.cmake_check_script(state) ?*/
+/*? macros.cmake_check_script(state) ?*/
\ No newline at end of file
diff --git a/tutorials/hello-camkes-timer/hello-camkes-timer.md b/tutorials/hello-camkes-timer/hello-camkes-timer.md
index 9850136b..1fb486ae 100644
--- a/tutorials/hello-camkes-timer/hello-camkes-timer.md
+++ b/tutorials/hello-camkes-timer/hello-camkes-timer.md
@@ -4,6 +4,8 @@
   SPDX-License-Identifier: BSD-2-Clause
 -->
 
+/*? declare_task_ordering(['1']) ?*/
+
 # CAmkES Timer Tutorial
 
 This tutorial guides you through setting up a sample timer driver component in
@@ -29,10 +31,42 @@ commented out.
 1. [Set up your machine](https://docs.sel4.systems/HostDependencies).
 2. [Camkes 2](https://docs.sel4.systems/Tutorials/hello-camkes-2)
 
-## Exercises - Part 1
+## CapDL Loader
+
+This tutorial uses the *capDL loader*, a root task which allocates statically
+ configured objects and capabilities.
+
+<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>
+
+## Initialising
+
+/*? macros.tutorial_init("hello-camkes-timer") ?*/
+
+<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("hello-camkes-timer") ?*/
 
-### TASK 1
+</details>
+
+## Exercises - Part 1
 
+### Instantiate a Timer and Timerbase
 Start in `hello-camkes-timer.camkes`.
 
 Instantiate some components. You're already given one component instance
@@ -55,21 +89,89 @@ timer.hello);` and `timer.sem_value = 0;` in the `hello-camkes-timer.camkes`
 file. They assume that the name of the timer ''driver'' will be `timer`. If you
 wish to call your driver something else, you'll have to change these lines.
 
-### TASK 2
+```
+/*-- filter TaskContent("1", TaskContentType.BEFORE, subtask="part1-task1") -*/
+    /* Part 1, TASK 1: component instances */
+    /* hint 1: one hardware component and one driver component
+        * hint 2: look at
+        * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application
+        */
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```
+/*-- filter TaskContent("1", TaskContentType.COMPLETED, subtask="part1-task1") -*/
+    /* Part 1, TASK 1: component instances */
+    component Timerbase timerbase;
+    component Timer timer;
+/*-- endfilter -*/
+```
+</details>
+
 
+### Connect a timer driver component
 Connect the timer driver component (`Timer`) to the timer hardware component
 (`Timerbase`). The timer hardware component exposes two interfaces which must
 be connected to the timer driver. One of these represents memory-mapped
 registers. The other represents an interrupt.
 
-### TASK 3
+```
+/*-- filter TaskContent("1", TaskContentType.BEFORE, subtask="part1-task2") -*/
+    /* Part 1, TASK 2: connections */
+    /* hint 1: use seL4HardwareMMIO to connect device memory
+        * hint 2: use seL4HardwareInterrupt to connect interrupt
+        * hint 3: look at
+        * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application
+        */
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```
+/*-- filter TaskContent("1", TaskContentType.COMPLETED, subtask="part1-task2") -*/
+    /* Part 1, TASK 2: connections */
+    connection seL4HardwareMMIO timer_mem(from timer.reg, to timerbase.reg);
+    connection seL4HardwareInterrupt timer_irq(from timerbase.irq, to timer.irq);
+/*-- endfilter -*/
+```
+</details>
 
+
+### Configure a timer hardware component instance
 Configure the timer hardware component instance with device-specific info. The
 physical address of the timer's memory-mapped registers, and its IRQ number
 must both be configured.
 
-### TASK 4
+```
+/*-- filter TaskContent("1", TaskContentType.BEFORE, subtask="part1-task3") -*/
+    /* Part 1, TASK 3: hardware resources */
+    /* Timer and Timerbase:
+        * hint 1: find out the device memory address and IRQ number from the hardware data sheet
+        * hint 2: look at
+        * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#hardware-components
+        */
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
 
+```
+/*-- filter TaskContent("1", TaskContentType.COMPLETED, subtask="part1-task3") -*/
+    /* Part 1, TASK 3: hardware resources */
+    timerbase.reg_paddr = 0xF8001000;   // paddr of mmio registers
+    timerbase.reg_size = 0x1000;        // size of mmio registers
+    timerbase.irq_irq_number = 42;      // timer irq number
+/*-- endfilter -*/
+```
+</details>
+
+### Call into a supplied driver to handle the interrupt
 Now open `components/Timer/src/timer.c`.
 
 We'll start by completing the `irq_handle` function, which is called in
@@ -87,33 +189,128 @@ where the initial `repo init` command was executed.
 This task is to call the `timer_handle_irq` function from the supply driver to
 inform the driver that an interrupt has occurred.
 
-### TASK 5
+```c
+/*-- filter TaskContent("1", TaskContentType.BEFORE, subtask="part1-task4") -*/
+    /* Part 1, TASK 4: call into the supplied driver to handle the interrupt. */
+    /* hint: timer_handle_irq
+     */
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
 
+```c
+/*-- filter TaskContent("1", TaskContentType.COMPLETED, subtask="part1-task4") -*/
+    /* Part 1, TASK 4: call into the supplied driver to handle the interrupt. */
+    timer_handle_irq(&timer_drv);
+/*-- endfilter -*/
+```
+</details>
+
+### Stop a timer
 Stop the timer from running. The `timer_stop` function will be helpful here.
 
-### TASK 6
+```c
+/*-- filter TaskContent("1", TaskContentType.BEFORE, subtask="part1-task5") -*/
+    /* Part 1, TASK 5: stop the timer. */
+    /* hint: timer_stop
+     */
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
+/*-- filter TaskContent("1", TaskContentType.COMPLETED, subtask="part1-task5") -*/
+    /* Part 1, TASK 5: stop the timer. */
+    timer_stop(&timer_drv);
+/*-- endfilter -*/
+```
+</details>
 
+### Acknowledge an interrupt
 The interrupt now needs to be acknowledged.
 
 CAmkES generates the seL4-specific code for ack-ing an interrupt and provides a
 function `<interface>_acknowldege` for IRQ interfaces (specifically those
 connected with `seL4HardwareInterrupt`).
 
-### TASK 7
+```c
+/*-- filter TaskContent("1", TaskContentType.BEFORE, subtask="part1-task6") -*/
+    /* Part 1, TASK 6: acknowledge the interrupt */
+    /* hint 1: use the function <irq interface name>_acknowledge()
+     */
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
+/*-- filter TaskContent("1", TaskContentType.COMPLETED, subtask="part1-task6") -*/
+    /* Part 1, TASK 6: acknowledge the interrupt */
+    error = irq_acknowledge();
+    ZF_LOGF_IF(error != 0, "failed to acknowledge interrupt");
+/*-- endfilter -*/
+```
+</details>
 
+### Get a timer handler
 Now we'll complete `hello__init` - a function which is called once
 before the component's interfaces start running.
 
 We need to initialise a handle to the timer driver for this device, and store a
 handle to the driver in the global variable `timer_drv`.
 
-### TASK 8
+```c
+/*-- filter TaskContent("1", TaskContentType.BEFORE, subtask="part1-task7") -*/
+    /* Part 1, TASK 7: call into the supplied driver to get the timer handler */
+    /* hint1: timer_init
+     * hint2: The timer ID is supplied as a #define in this file
+     * hint3: The register's variable name is the same name as the dataport in the Timer component
+     */
+/*-- endfilter -*/
+```
 
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
+/*-- filter TaskContent("1", TaskContentType.COMPLETED, subtask="part1-task7") -*/
+    /* Part 1, TASK 7: call into the supplied driver to get the timer handler */
+    int error = timer_init(&timer_drv, DEFAULT_TIMER_ID, reg);
+    assert(error == 0);
+/*-- endfilter -*/
+```
+</details>
+
+### Start a timer
 After initialising the timer, we now need to start the timer. Do so by calling
 `timer_start` and passing the handle to the driver.
 
-### TASK 9
+```c
+/*-- filter TaskContent("1", TaskContentType.BEFORE, subtask="part1-task8") -*/
+    /* Part 1, TASK 8: start the timer */
+    /* hint: timer_start
+     */
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
+/*-- filter TaskContent("1", TaskContentType.COMPLETED, subtask="part1-task8") -*/
+    /* Part 1, TASK 8: start the timer */
+    error = timer_start(&timer_drv);
+    assert(error == 0);
+/*-- endfilter -*/
+```
+</details>
 
+### Implement a RPC interface
 Note that this task is to understand the existing code. You won't have
 to modify anything for this task.
 
@@ -124,12 +321,58 @@ should return after a given number of seconds. in
 exposed by the `Timer` component is called `hello`. Thus, the function we
 need to implement is called `hello_sleep`.
 
-### TASK 10
+```c
+/*-- filter TaskContent("1", TaskContentType.BEFORE, subtask="part1-task9") -*/
+    /* Part 1, TASK 9: implement the rpc function. */
+    /* hint 1: the name of the function to implement is a composition of an interface name and a function name:
+    * i.e.: <interface>_<function>
+    * hint 2: the interfaces available are defined by the component, e.g. in components/timer/timer.camkes
+    * hint 3: the function name is defined by the interface definition, e.g. in interfaces/timer.camkes
+    * hint 4: so the function would be: hello_sleep()
+    * hint 5: the camkes 'int' type maps to 'int' in c
+    * hint 6: invoke a function in supplied driver the to set up the timer
+    * hint 7: look at https://github.com/sel4/camkes-tool/blob/master/docs/index.md#creating-an-application
+    */
+/*-- endfilter -*/
+```
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
 
+```c
+ /*-- filter TaskContent("1", TaskContentType.COMPLETED, subtask="part1-task9") -*/
+/* Part 1, TASK 9: implement the rpc function. */
+void hello_sleep(int sec) {
+    int error = 0;
+/*-- endfilter -*/
+```
+</details>
+
+### Set a timer interrupt
 Tell the timer to interrupt after the given number of seconds. The
 `timer_set_timeout` function from the included driver will help. Note that it
 expects its time argument to be given in nanoseconds.
 
+```c
+/*-- filter TaskContent("1", TaskContentType.BEFORE, subtask="part1-task10") -*/
+    /* Part 1, TASK 10: invoke a function in the supplied driver to set a timeout */
+    /* hint1: timer_set_timeout
+     * hint2: periodic should be set to false
+     */
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
+/*-- filter TaskContent("1", TaskContentType.COMPLETED, subtask="part1-task10") -*/
+    /* Part 1, TASK 10: invoke a function in the supplied driver to set a timeout */
+    error = timer_set_timeout(&timer_drv, sec * NS_IN_SECOND, false);
+    assert(error == 0);
+/*-- endfilter -*/
+```
+</details>
+
 Note the existing code in `hello_sleep`. It waits on a binary semaphore.
 `irq_handle` will be called on another thread when the timer interrupt occurs,
 and that function will post to the binary semaphore, unblocking us and allowing
@@ -157,8 +400,7 @@ kernel, look in the `tools/dts/` folder of the kernel sources. If a suitable
 devicetree blob is not available for your platform, then do not proceed with
 the tutorial.
 
-### TASK 1
-
+### Instantiate a TimerDTB component
 Navigate to the `hello-camkes-timer.camkes` file.
 
 Remove the `Timerbase` and `Timer` component instantiations and instantiate a
@@ -166,14 +408,57 @@ Remove the `Timerbase` and `Timer` component instantiations and instantiate a
 hello_timer(from client.hello, to timer.hello);` and `timer.sem_value = 0;`
 lines if necessary.
 
-### TASK 2
+```
+/*-- filter TaskContent("1", TaskContentType.BEFORE, subtask="part2-task1") -*/
+    /* Part 2, TASK 1: component instances */
+    /* hint 1: a single TimerDTB component
+    * hint 2: look at
+    * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application
+    */
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
 
+```
+/*-- filter TaskContent("1", TaskContentType.COMPLETED, subtask="part2-task1") -*/
+    /* Part 2, TASK 1: component instances */
+    //uncomment the line below
+//    component TimerDTB timer;
+/*-- endfilter -*/
+```
+</details>
+
+### Connect interfaces using the seL4DTBHardware connector
 Remove the `seL4HardwareMMIO` and `seL4HardwareInterrupt` connections. Connect
 the two interfaces inside the `TimerDTB` component with the `seL4DTBHardware`
 connector.
 
-### TASK 3
+```
+/*-- filter TaskContent("1", TaskContentType.BEFORE, subtask="part2-task2") -*/
+    /* Part 2, TASK 2: connections */
+    /* hint 1: connect the dummy_source and timer interfaces
+    * hint 2: the dummy_source should be the 'from' end
+    * hint 3: look at
+    * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application
+    */
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```
+/*-- filter TaskContent("1", TaskContentType.COMPLETED, subtask="part2-task2") -*/
+      /* Part 2, TASK 2: connections */
+      // uncomment the line below
+//    connection seL4DTBHardware timer_dtb(from timer.dummy_source, to timer.tmr);
+/*-- endfilter -*/
+```
+</details>
 
+### Configure the TimerDTB component
 Before opening `components/Timer/Timer.camkes`, remove the `Timerbase` settings
 inside the configurations block.
 
@@ -184,8 +469,32 @@ and grab the necessary data to initialise hardware resources. More
 specifically, it reads the registers field and optionally the interrupts field
 to allocate memory and interrupts.
 
-### TASK 4
+```
+/*-- filter TaskContent("1", TaskContentType.BEFORE, subtask="part2-task3") -*/
+    /* Part 2, TASK 3: hardware resources */
+    /* TimerDTB:
+     * hint 1: look in the DTB/DTS for the path of a timer
+     * hint 2: set the 'dtb' setting for the tmr interface in the TimerDTB component,
+     *         e.g. foo.dtb = dtb({"path" : "/bar"});
+     * hint 3: set the 'generate_interrupts' setting to 1
+     */
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
 
+```
+/*-- filter TaskContent("1", TaskContentType.COMPLETED, subtask="part2-task3") -*/
+     /* Part 2, TASK 3: hardware resources */
+     // uncomment the lines below
+//    tmr.dtb = dtb({"path" : "/amba/timer@f8001000"});   // path of the timer in the DTB
+//    tmr.generate_interrupts = 1;                        // tell seL4DTBHardware to init interrupts
+/*-- endfilter -*/
+```
+</details>
+
+### Handle the interrupt
 Move to `components/TimerDTB/src/timerdtb.c`.
 
 Similar to part one, we'll start with the `tmr_irq_handle` function. This
@@ -206,12 +515,48 @@ Likewise with part one, the implementation of the timer driver is in the
 included driver in `timer_driver` and the task here is to call
 `timer_handle_irq`.
 
-### TASK 5
+```c
+/*-- filter TaskContent("1", TaskContentType.BEFORE, subtask="part2-task4") -*/
+    /* Part 2, TASK 4: call into the supplied driver to handle the interrupt. */
+    /* hint: timer_handle_irq
+     */
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
+/*-- filter TaskContent("1", TaskContentType.COMPLETED, subtask="part2-task4") -*/
+    /* Part 2, TASK 4: call into the supplied driver to handle the interrupt. */
+    timer_handle_irq(&timer_drv);
+/*-- endfilter -*/
+```
+</details>
+
+### Stop a timer
+Stop the timer from running. The `timer_stop` function will be helpful here.
 
-The timer needs to be stopped, the task here is the same as part one's task 5.
+```c
+/*-- filter TaskContent("1", TaskContentType.BEFORE, subtask="part2-task5") -*/
+    /* Part 2, TASK 5: stop the timer. */
+    /* hint: timer_stop
+     */
+/*-- endfilter -*/
+```
 
-### TASK 6
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
 
+```c
+/*-- filter TaskContent("1", TaskContentType.COMPLETED, subtask="part2-task5") -*/
+    /* Part 2, TASK 5: stop the timer. */
+    timer_stop(&timer_drv);
+/*-- endfilter -*/
+```
+</details>
+
+### Acknowledge the interrupt
 Again, the interrupt now has to be acknowledged.
 
 For the `seL4DTBHardware` connector, CAmkES also generates and provides a
@@ -221,13 +566,33 @@ takes in a `ps_irq_t *` argument. Similarly, the `ps_irq_t *` argument helps
 CAmkES to differentiate between the possibly many interrupts of a device that
 you wish to acknowledge.
 
+```c
+/*-- filter TaskContent("1", TaskContentType.BEFORE, subtask="part2-task6") -*/
+    /* Part 2, TASK 6: acknowledge the interrupt */
+    /* hint 1: use the function <to_interface_name>_irq_acknowledge()
+     * hint 2: pass in the 'irq' variable to the function
+     */
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
+/*-- filter TaskContent("1", TaskContentType.COMPLETED, subtask="part2-task6") -*/
+    /* Part 2, TASK 6: acknowledge the interrupt */
+    error = tmr_irq_acknowledge(irq);
+    ZF_LOGF_IF(error != 0, "failed to acknowledge interrupt");
+/*-- endfilter -*/
+```
+</details>
+
 ### TASK 7 - 10
 
 Task 7 to 10 are the exact same as the tasks in part one.
 
 You should also expect the same output as the first part.
 
-/*? macros.help_block() ?*/
 
 /*-- filter ExcludeDocs() -*/
 ```c
@@ -300,17 +665,9 @@ component TimerDTB {
     }
 
     configuration {
-    /* Part 2, TASK 3: hardware resources */
-    /* TimerDTB:
-     * hint 1: look in the DTB/DTS for the path of a timer
-     * hint 2: set the 'dtb' setting for the tmr interface in the TimerDTB component,
-     *         e.g. foo.dtb = dtb({"path" : "/bar"});
-     * hint 3: set the 'generate_interrupts' setting to 1
-     */
-/*- if solution -*/
-//        tmr.dtb = dtb({"path" : "/amba/timer@f8001000"});   // path of the timer in the DTB
-//        tmr.generate_interrupts = 1;                        // tell seL4DTBHardware to init interrupts
-/*- endif -*/
+
+/*? include_task_type_append([("1","part2-task3")]) ?*/
+
     }
 }
 /*-- endfilter -*/
@@ -333,74 +690,26 @@ timer_drv_t timer_drv;
 void irq_handle(void) {
     int error;
 
-    /* Part 1, TASK 4: call into the supplied driver to handle the interrupt. */
-    /* hint: timer_handle_irq
-     */
-/*- if solution -*/
-    timer_handle_irq(&timer_drv);
-/*- endif -*/
+/*? include_task_type_append([("1","part1-task4")]) ?*/
 
-    /* Part 1, TASK 5: stop the timer. */
-    /* hint: timer_stop
-     */
-/*- if solution -*/
-    timer_stop(&timer_drv);
-/*- endif -*/
+/*? include_task_type_append([("1","part1-task5")]) ?*/
 
     /* signal the rpc interface. */
     error = sem_post();
     ZF_LOGF_IF(error != 0, "failed to post to semaphore");
 
-    /* Part 1, TASK 6: acknowledge the interrupt */
-    /* hint 1: use the function <irq interface name>_acknowledge()
-     */
-/*- if solution -*/
-    error = irq_acknowledge();
-    ZF_LOGF_IF(error != 0, "failed to acknowledge interrupt");
-/*- endif -*/
+/*? include_task_type_append([("1","part1-task6")]) ?*/
 }
 
 void hello__init() {
-    /* Part 1, TASK 7: call into the supplied driver to get the timer handler */
-    /* hint1: timer_init
-     * hint2: The timer ID is supplied as a #define in this file
-     * hint3: The register's variable name is the same name as the dataport in the Timer component
-     */
-/*- if solution -*/
-    int error = timer_init(&timer_drv, DEFAULT_TIMER_ID, reg);
-    assert(error == 0);
-/*- endif -*/
+/*? include_task_type_append([("1","part1-task7")]) ?*/
 
-    /* Part 1, TASK 8: start the timer
-     * hint: timer_start
-     */
-/*- if solution -*/
-    error = timer_start(&timer_drv);
-    assert(error == 0);
-/*- endif -*/
+/*? include_task_type_append([("1","part1-task8")]) ?*/
 }
 
-/* part 1, TASK 9: implement the rpc function. */
-/* hint 1: the name of the function to implement is a composition of an interface name and a function name:
- * i.e.: <interface>_<function>
- * hint 2: the interfaces available are defined by the component, e.g. in components/timer/timer.camkes
- * hint 3: the function name is defined by the interface definition, e.g. in interfaces/timer.camkes
- * hint 4: so the function would be: hello_sleep()
- * hint 5: the camkes 'int' type maps to 'int' in c
- * hint 6: invoke a function in supplied driver the to set up the timer
- * hint 7: look at https://github.com/sel4/camkes-tool/blob/master/docs/index.md#creating-an-application
- */
-void hello_sleep(int sec) {
-    int error = 0;
+/*? include_task_type_append([("1","part1-task9")]) ?*/
 
-    /* Part 1, TASK 10: invoke a function in the supplied driver to set a timeout */
-    /* hint1: timer_set_timeout
-     * hint2: periodic should be set to false
-     */
-/*- if solution -*/
-    error = timer_set_timeout(&timer_drv, sec * NS_IN_SECOND, false);
-    assert(error == 0);
-/*- endif -*/
+/*? include_task_type_append([("1","part1-task10")]) ?*/
 
     error = sem_wait();
     ZF_LOGF_IF(error != 0, "failed to wait on semaphore");
@@ -422,32 +731,15 @@ timer_drv_t timer_drv;
 void tmr_irq_handle(ps_irq_t *irq) {
     int error;
 
-    /* Part 2, TASK 4: call into the supplied driver to handle the interrupt. */
-    /* hint: timer_handle_irq
-     */
-/*- if solution -*/
-    timer_handle_irq(&timer_drv);
-/*- endif -*/
+/*? include_task_type_append([("1","part2-task4")]) ?*/
 
-    /* Part 2, TASK 5: stop the timer. */
-    /* hint: timer_stop
-     */
-/*- if solution -*/
-    timer_stop(&timer_drv);
-/*- endif -*/
+/*? include_task_type_append([("1","part2-task5")]) ?*/
 
     /* signal the rpc interface. */
     error = sem_post();
     ZF_LOGF_IF(error != 0, "failed to post to semaphore");
 
-    /* Part 2, TASK 6: acknowledge the interrupt */
-    /* hint 1: use the function <to_interface_name>_irq_acknowledge()
-     * hint 2: pass in the 'irq' variable to the function
-     */
-/*- if solution -*/
-    error = tmr_irq_acknowledge(irq);
-    ZF_LOGF_IF(error != 0, "failed to acknowledge interrupt");
-/*- endif -*/
+/*? include_task_type_append([("1","part2-task6")]) ?*/
 }
 
 void hello__init() {
@@ -529,23 +821,10 @@ assembly {
 /*- if not solution -*/
         component EmptyComponent empty;
 /*- endif -*/
-        /* Part 1, TASK 1: component instances */
-        /* hint 1: one hardware component and one driver component
-         * hint 2: look at
-         * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application
-         */
 
-        /* Part 2, TASK 1: component instances */
-        /* hint 1: a single TimerDTB component
-         * hint 2: look at
-         * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application
-         */
-/*- if solution -*/
-        component Timerbase timerbase;
-        component Timer timer;
+/*? include_task_type_append([("1","part1-task1")]) ?*/
 
-//        component TimerDTB timer;
-/*- endif -*/
+/*? include_task_type_append([("1","part2-task1")]) ?*/
 
 /*- if solution -*/
         component Client client;
@@ -556,25 +835,9 @@ assembly {
 //        component Client client;
 /*- endif -*/
 
-        /* Part 1, TASK 2: connections */
-        /* hint 1: use seL4HardwareMMIO to connect device memory
-         * hint 2: use seL4HardwareInterrupt to connect interrupt
-         * hint 3: look at
-         * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application
-         */
-
-        /* Part 2, TASK 2: connections */
-        /* hint 1: connect the dummy_source and timer interfaces
-         * hint 2: the dummy_source should be the 'from' end
-         * hint 3: look at
-         * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application
-         */
-/*- if solution -*/
-        connection seL4HardwareMMIO timer_mem(from timer.reg, to timerbase.reg);
-        connection seL4HardwareInterrupt timer_irq(from timerbase.irq, to timer.irq);
+/*? include_task_type_append([("1","part1-task2")]) ?*/
 
-//        connection seL4DTBHardware timer_dtb(from timer.dummy_source, to timer.tmr);
-/*- endif -*/
+/*? include_task_type_append([("1","part2-task2")]) ?*/
 
         /* timer interface connection */
 /*- if solution -*/
@@ -588,22 +851,12 @@ assembly {
 /*- endif -*/
     }
     configuration {
-        /* Part 1, TASK 3: hardware resources */
-        /* Timer and Timerbase:
-         * hint 1: find out the device memory address and IRQ number from the hardware data sheet
-         * hint 2: look at
-         * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#hardware-components
-         */
+/*? include_task_type_append([("1","part1-task3")]) ?*/
 
         /* Part 2, TASK 3: hardware resources */
         /* TimerDTB:
          * check components/Timer/Timer.camkes
          */
-/*- if solution -*/
-        timerbase.reg_paddr = 0xF8001000;   // paddr of mmio registers
-        timerbase.reg_size = 0x1000;        // size of mmio registers
-        timerbase.irq_irq_number = 42;      // timer irq number
-/*- endif -*/
 
         /* assign an initial value to semaphore */
 /*- if solution -*/
@@ -616,4 +869,8 @@ assembly {
 /*-- endfilter -*/
 /*? ExternalFile("CMakeLists.txt") ?*/
 ```
-/*-- endfilter -*/
+
+/*- filter TaskContent("1", TaskContentType.BEFORE, completion="Booting all finished, dropped to user space") -*//*- endfilter -*/
+/*- filter TaskContent("1", TaskContentType.COMPLETED, completion="After the client: wakeup") -*//*- endfilter -*/
+
+/*-- endfilter -*/
\ No newline at end of file
diff --git a/tutorials/hello-world/hello-world.md b/tutorials/hello-world/hello-world.md
index f1a8d208..f9eaddf7 100644
--- a/tutorials/hello-world/hello-world.md
+++ b/tutorials/hello-world/hello-world.md
@@ -7,47 +7,92 @@
 /*? declare_task_ordering(['hello-world', 'hello-world-mod']) ?*/
 # Hello, World!
 
-This tutorial guides you through getting a simple "Hello World" program running as a user-level application on seL4. 
-It allows you to test your local set up and make sure all the tools are working before moving onto more detailed tutorials.
+In this tutorial you will:
+
+1. Run Hello, World! to ensure your setup is working correctly
+2. Become familiar with the jargon *root task*
+3. Build and simulate a seL4 project
+4. Have a basic understanding of the role of the `CMakeLists.txt` file in applications
 
 ## Prerequisites
+1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up)
+
+## Building your first program
+seL4 is a microkernel, not an operating system, and as a result only provides very minimal services.
+
+After the kernel boots, an initial thread called the *root task* is started, which is then responsible for setting up the user-level system.
+
+When the root task starts there are no available drivers, however a minimal C library is provided.
+
+The tutorial is already set up to print "Hello, world!", so at this point  all you need to do is build and run the tutorial.
+
+## Revisiting containers
+
+We will use two terminals, as described in [Setting up your machine](https://docs.sel4.systems/Tutorials/setting-up#mapping-a-container).
+ - Terminal A is just a normal terminal, and is used for git operations, editing (e.g., vim, emacs), and other normal operations.
+ - Terminal B is running in a container, and is only used for compilation.
+
+This gives you the flexibility to use all the normal tools you are used to, while having the seL4 dependencies separated from your machine.
+
+### Create a container
 
-1. [Set up your machine](https://docs.sel4.systems/HostDependencies). 
+Open a new terminal, Terminal B, to run a container.
+
+
+Create a container:
+
+```
+container
+```
 
 ## Initialising
 
+Initialise the tutorial in Terminal B, which is running the container.
+
 /*? macros.tutorial_init("hello-world") ?*/
 
-## Outcomes
+This step creates two new directories in `sel4-tutorials-manifest`, namely `hello-world` and `hello-world_build`
 
-By the end of this tutorial, you should:
+<details markdown='1'>
 
-* Be familiar with the jargon *root task*.
-* Be able to build and simulate seL4 projects.
-* Have a basic understanding of the role of the `CMakeLists.txt` file in applications.
+<summary><em>Hint:</em> tutorial solutions</summary>
+<br>
+All tutorials come with complete solutions. To get solutions run:
 
-## Building your first program
+/*? macros.tutorial_init_with_solution("hello-world") ?*/
+
+This will generate another `hello-world` directory and `hello-world_build` directory, with unique names, e.g. `hello-world44h1po5q` and `hello-world44h1po5q_build`.
+
+</details>
 
-seL4 is a microkernel, not an operating system, and as a result only provides very minimal services. 
-After the kernel boots, an initial thread called the *root task* is started, which is then responsible for
- setting up the user-level system.
-When the root task starts there are no available drivers, however a minimal C library is provided. 
 
-The tutorial is already set up to print "Hello, world!", so at this point 
-all you need to do is build and run the tutorial:
+
+### Build the program
+
+```
+cd sel4-tutorials-manifest/hello-world_build
+```
+
+Next, build the program in Terminal B using ninja
 
 /*? macros.ninja_block() ?*/
 
-If successful, you should see the final ninja rule passing:
+If successful, you should see the final ninja rule passing, e.g.:
+
 ```
 [150/150] objcopy kernel into bootable elf
-$
 ```
 
+### Run Hello, World using QEMU
+
 The final image can be run by:
-/*? macros.simulate_block() ?*/
 
-This will run the result on an instance of the [QEMU](https://www.qemu.org) simulator. 
+```
+./simulate
+```
+
+This will run the result on an instance of the [QEMU](https://www.qemu.org) simulator.
+
 If everything has worked, you should see:
 
 ```
@@ -63,6 +108,12 @@ because the program hasn't properly cleaned up after itself yet. (This will come
 `Ctrl-A, X` will terminate QEMU.
 
 ## Looking at the sources
+To look at the sources, open a new terminal, Terminal A:
+
+```
+cd sel4-tutorials-manifest/hello-world
+ls
+```
 
 In your tutorial directory, you will find the following files:
  * `CMakeLists.txt` - the file that incorporates the root task into the wider seL4 build system.
@@ -148,7 +199,11 @@ int main(int argc, char *argv[]) {
 }
 /*- endfilter --*/
 ```
-Once you have made your change, rerun `ninja` to rebuild the project:
+
+Once you have made your change, use Terminal B to rebuild the project.
+
+*Hint:* Remember to exit the QEMU simulator before rerunning the project with `ctrl-A,x`
+
 /*? macros.ninja_block() ?*/
 Then run the simulator again:
 
@@ -162,8 +217,6 @@ Second hello
 /*- endfilter -*/
 ```
 
-/*? macros.help_block() ?*/
-
 /*- filter ExcludeDocs() -*/
 
 ```c
diff --git a/tutorials/interrupts/interrupts.md b/tutorials/interrupts/interrupts.md
index 3e9dbbbc..0818efed 100644
--- a/tutorials/interrupts/interrupts.md
+++ b/tutorials/interrupts/interrupts.md
@@ -4,23 +4,54 @@
   SPDX-License-Identifier: BSD-2-Clause
 -->
 
-# Interrupts
 /*? declare_task_ordering(['timer-start', 'timer-get', 'timer-set', 'timer-ack']) ?*/
 
+# Interrupts
+This tutorial covers seL4 interrupts.
+
+You will learn:
+1. The purpose of the IRQControl capability.
+2. How to obtain capabilities for specific interrupts.
+3. How to handle interrupts and their relation with notification objects.
+
 ## Prerequisites
 
-1. [Set up your machine](https://docs.sel4.systems/HostDependencies).
-2. [Notification tutorial](https://docs.sel4.systems/Tutorials/notifications)
+1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up)
+2. [Notifications tutorial](https://docs.sel4.systems/Tutorials/notifications)
 
 # Initialising
 
 /*? macros.tutorial_init("interrupts") ?*/
 
-## Outcomes
+<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("interrupts") ?*/
 
-* Understand the purpose of the IRQControl capability.
-* Be able to obtain capabilities for specific interrupts.
-* Learn how to handle interrupts and their relation with notification objects.
+Answers are also available in drop down menus under each section.
+</details>
+
+## CapDL Loader
+
+This tutorial uses the *capDL loader*, a root task which allocates statically
+ configured objects and capabilities.
+
+<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>
 
 ## Background
 
@@ -57,6 +88,7 @@ with the IRQHandler capability for that irq, as follows:
 ```bash
 seL4_IRQHandler_SetNotification(irq_handler, notification);
 ```
+
 On success, this call will result in signals being delivered to the notification object when
 an interrupt occurs. To handle multiple interrupts on the same notification object, you
 can set different badges on the notification capabilities bound to each IRQHandler.
@@ -104,6 +136,8 @@ main@timer.c:78 [Cond failed: error]
 
 The timer driver we are using emits an interrupt in the `TTC0_TIMER1_IRQ` number.
 
+### Invoke IRQ control
+
 **Exercise** Invoke `irq_control`, which contains the `seL4_IRQControl` capability,
 the place the `IRQHandler` capability for `TTC0_TIMER1_IRQ` into the `irq_handler` CSlot.
 
@@ -112,15 +146,23 @@ the place the `IRQHandler` capability for `TTC0_TIMER1_IRQ` into the `irq_handle
     /* TODO invoke irq_control to put the interrupt for TTC0_TIMER1_IRQ in
        cslot irq_handler (depth is seL4_WordBits) */
 /*-- endfilter -*/
-/*-- filter ExcludeDocs() -*/
+
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("timer-get", TaskContentType.COMPLETED, subtask='get') -*/
     /* put the interrupt handle for TTC0_TIMER1_IRQ in the irq_handler cslot */
     error = seL4_IRQControl_Get(irq_control, TTC0_TIMER1_IRQ, cnode, irq_handler, seL4_WordBits);
     ZF_LOGF_IF(error, "Failed to get irq capability");
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
 
+</details>
+
+
 On success, you should see the following output, without the error message that occurred earlier,
 as the irq_handle capability is now valid:
 
@@ -133,21 +175,30 @@ Undelivered IRQ: 42
 This is a warning message from the kernel that an IRQ was recieved for irq number 42, but no
 notification capability is set to sent a signal to.
 
+### Set NTFN
 **Exercise** Now set the notification capability (`ntfn`) by invoking the irq handler.
 
 ```
 /*-- filter TaskContent("timer-start", TaskContentType.ALL, subtask='set') -*/
      /* TODO set ntfn as the notification for irq_handler */
 /*-- endfilter -*/
-/*-- filter ExcludeDocs() -*/
+
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("timer-set", TaskContentType.COMPLETED, subtask='set') -*/
     /* set ntfn as the notification for irq_handler */
     error =  seL4_IRQHandler_SetNotification(irq_handler, ntfn);
     ZF_LOGF_IF(error, "Failed to set notification");
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
 
+</details>
+
+
 Now the output will be:
 
 ```
@@ -160,21 +211,30 @@ Only one interrupt is delivered, as the interrupt has not been acknowledged. The
 programmed to emit an interrupt every millisecond, so we need to count 2000 interrupts
 before replying to the client.
 
+### Acknowledge an interrupt
+
 **Exercise** Acknowledge the interrupt after handling it in the timer driver.
 
 ```
 /*-- filter TaskContent("timer-start", TaskContentType.ALL, subtask='ack') -*/
         /* TODO ack the interrupt */
 /*-- endfilter -*/
-/*-- filter ExcludeDocs() -*/
+
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("timer-ack", TaskContentType.COMPLETED, subtask='ack') -*/
         /* ack the interrupt */
         error = seL4_IRQHandler_Ack(irq_handler);
         ZF_LOGF_IF(error, "Failed to ack irq");
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
 
+</details>
+
 Now the timer interrupts continue to come in, and the reply is delivered to the client.
 
 ```
@@ -185,8 +245,6 @@ timer client wakes up
 
 That's it for this tutorial.
 
-/*? macros.help_block() ?*/
-
 /*-- filter ExcludeDocs() -*/
 ```c
 /*-- filter ELF("client") -*/
@@ -337,8 +395,8 @@ int main(void) {
     return 0;
 }
 
-
 /*-- endfilter -*/
 ```
+
 /*? ExternalFile("CMakeLists.txt") ?*/
 /*- endfilter -*/
diff --git a/tutorials/ipc/ipc.md b/tutorials/ipc/ipc.md
index 6c73b30b..9b4348b0 100644
--- a/tutorials/ipc/ipc.md
+++ b/tutorials/ipc/ipc.md
@@ -7,21 +7,52 @@
 # IPC
 /*? declare_task_ordering(['ipc-start', 'ipc-badge', 'ipc-echo', 'ipc-reply', 'ipc-order']) ?*/
 
+This tutorial is about interprocess communication (IPC), the microkernel mechanism for synchronous transmission of small amounts of data.
+
+You will learn:
+1. How to use IPC to send data and capabilities between processes.
+2. The jargon *cap transfer*.
+3. How to differentiate requests via badged capabilities.
+4. Design protocols that use the IPC fastpath.
+
 ## Prerequisites
 
-1. [Set up your machine](https://docs.sel4.systems/HostDependencies).
+1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up)
 2. [Capabilities tutorial](https://docs.sel4.systems/Tutorials/capabilities)
 
 ## Initialising
 
 /*? macros.tutorial_init("ipc") ?*/
 
-## Outcomes
+<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("ipc") ?*/
+
+Answers are also available in drop down menus under each section.
+</details>
+
+## CapDL Loader
+
+This tutorial uses the *capDL loader*, a root task which allocates statically
+ configured objects and capabilities.
 
-1. Be able to use IPC to send data and capabilities between processes.
-2. Learn the jargon *cap transfer*.
-3. Be able to differentiate requests via badged capabilities.
-4. Know how to design protocols that use the IPC fastpath.
+<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.
+
+More information about CapDL projects can be found [here](https://docs.sel4.systems/CapDL.html).
+
+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>
 
 ## Background
 
@@ -174,6 +205,8 @@ uses the badged endpoint, such that the server can identify the client. However,
 currently send the badged capability! We have provided code to badge the endpoint capability, and
 reply to the client.
 
+### Use capability transfer to send the badged capability
+
 **Exercise** Your task is to set up the cap transfer such that the client successfully
 receives the badged endpoint.
 
@@ -198,7 +231,12 @@ receives the badged endpoint.
              /* wait for the next message */
              info = seL4_Recv(endpoint, &sender);
 /*-- endfilter -*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("ipc-badge", TaskContentType.COMPLETED, subtask="badge", completion='received badged endpoint') -*/
              /* No badge! give this sender a badged copy of the endpoint */
              seL4_Word badge = seL4_GetMR(0);
@@ -221,9 +259,11 @@ receives the badged endpoint.
              /* wait for the next message */
              info = seL4_Recv(endpoint, &sender);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
 
+</details>
+
+
 Now the output should look something like:
 ```bash
 Booting all finished, dropped to user space
@@ -239,6 +279,8 @@ Depending on timing, the messages may be different, the result is the same: the
 This is because one of the clients has hit the else case, where the badge is set, and the server
 does not respond, or wait for new messages from this point.
 
+### Get a message
+
 **Exercise** Your next task is to implement the echo part of the server.
 
 ```c
@@ -246,15 +288,20 @@ does not respond, or wait for new messages from this point.
              // TODO use printf to print out the message sent by the client
              // followed by a new line
 /*-- endfilter -*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("ipc-echo", TaskContentType.COMPLETED, subtask="echo") -*/
              for (int i = 0; i < seL4_MessageInfo_get_length(info); i++) {
                  printf("%c", (char) seL4_GetMR(i));
              }
              printf("\n");
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
 
 At this point, you should see a single word output to the console in a loop.
 ```
@@ -267,18 +314,27 @@ the
 
 This is because the server does not reply to the client, and continues to spin in a loop
  repeating the last message.
+
+### Reply and wait
+
 **Exercise**  Update the code to reply to the clients after printing the message.
 
 ```c
 /*-- filter TaskContent("ipc-start", TaskContentType.ALL, subtask="reply") -*/
              // TODO reply to the client and wait for the next message
 /*-- endfilter -*/
-/*-- filter ExcludeDocs() -*/
+
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("ipc-reply", TaskContentType.COMPLETED, subtask="reply", completion="lazy") -*/
              info = seL4_ReplyRecv(endpoint, info, &sender);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
 
 Now the output should be something like this:
 
@@ -296,11 +352,17 @@ over
 lazy
 ```
 
+### Save a reply and store reply capabilities
+
 **Exercise** Currently each client is scheduled for its full timeslice until it is preempted. Alter
 your server to only print one message from each client, alternating. You will need to use
 [`seL4_CNode_SaveCaller`](https://docs.sel4.systems/ApiDoc.html#save-caller)  to save the reply
 capability for each sender. You can use `free_slot` to store the reply capabilities.
-/*-- filter ExcludeDocs() -*/
+
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
 ```c
 /*-- filter TaskContent("ipc-order", TaskContentType.COMPLETED, subtask="order", completion="dog") -*/
               error = seL4_CNode_SaveCaller(cnode, free_slot, seL4_WordBits);
@@ -313,7 +375,9 @@ capability for each sender. You can use `free_slot` to store the reply capabilit
               seL4_Send(free_slot, seL4_MessageInfo_new(0, 0, 0, 0));
 /*-- endfilter -*/
 ```
-/*-- endfilter -*/
+
+</details>
+
 
 Depending on your approach, successful output should look something like this:
 ```
@@ -338,7 +402,7 @@ to become more familiar with IPC.
 * Try using `seL4_Send` and `seL4_Recv`.
 * Try the non-blocking variants, `seL4_NBSend` and `seL4_NBRecv`.
 
-/*? macros.help_block() ?*/
+
 
 /*-- filter ExcludeDocs() -*/
 ```c
diff --git a/tutorials/dynamic-1/CMakeLists.txt b/tutorials/libraries-1/CMakeLists.txt
similarity index 70%
rename from tutorials/dynamic-1/CMakeLists.txt
rename to tutorials/libraries-1/CMakeLists.txt
index 216a099c..5e7ebf79 100644
--- a/tutorials/dynamic-1/CMakeLists.txt
+++ b/tutorials/libraries-1/CMakeLists.txt
@@ -8,18 +8,18 @@ include(${SEL4_TUTORIALS_DIR}/settings.cmake)
 sel4_tutorials_regenerate_tutorial(${CMAKE_CURRENT_SOURCE_DIR})
 
 cmake_minimum_required(VERSION 3.7.2)
-# declare the dynamic-1 CMake project and the languages it is written in
-project(dynamic-1 C ASM)
+# declare the libraries-1 CMake project and the languages it is written in
+project(libraries-1 C ASM)
 
 sel4_tutorials_setup_roottask_tutorial_environment()
 
-add_executable(dynamic-1 main.c)
+add_executable(libraries-1 main.c)
 
-target_link_libraries(dynamic-1
+target_link_libraries(libraries-1
     sel4
     muslc utils sel4tutorials
     sel4muslcsys sel4platsupport sel4utils sel4debug sel4allocman)
 
 include(rootserver)
-DeclareRootserver(dynamic-1)
+DeclareRootserver(libraries-1)
 /*? macros.cmake_check_script(state) ?*/
diff --git a/tutorials/dynamic-1/dynamic-1.md b/tutorials/libraries-1/libraries-1.md
similarity index 91%
rename from tutorials/dynamic-1/dynamic-1.md
rename to tutorials/libraries-1/libraries-1.md
index 285ec0d3..bfda9368 100644
--- a/tutorials/dynamic-1/dynamic-1.md
+++ b/tutorials/libraries-1/libraries-1.md
@@ -22,9 +22,9 @@
 'task-15',
 ]) ?*/
 
-# seL4 Dynamic Libraries: initialisation & threading
+# seL4 Libraries: Initialisation & Threading
 
-This tutorial provides code examples and exercises for using the dynamic libraries
+This tutorial provides code examples and exercises for using the libraries
 found in [`seL4_libs`](https://github.com/seL4/seL4_libs) to bootstrap a system and start a thread.
 
 The tutorial is useful in that
@@ -33,19 +33,12 @@ it addresses conceptual problems for two different types of developers:
 - Experienced kernel developers whose minds are pre-programmed to
       think in terms of "One address space equals one process", and
       begins to introduce the seL4 CSpace vs VSpace model.
-- New kernel developers, for whom the tutorial will prompt them on
-      what to read about.
+- New kernel developers, for whom the tutorial will provide prompts on what to read.
 
 Don't gloss over the globals declared before `main()` -- they're declared
 for your benefit so you can grasp some of the basic data structures.
 
-## Prerequisites
-
-1. [Set up your machine](https://docs.sel4.systems/HostDependencies).
-2. [Hello world](https://docs.sel4.systems/Tutorials/hello-world)
-
-## Outcomes:
-
+Outcomes:
 - Understand the kernel's startup procedure.
 - Understand that the kernel centers around certain objects and
         capabilities to those objects.
@@ -59,9 +52,25 @@ for your benefit so you can grasp some of the basic data structures.
         idea that a thread has a TCB, VSpace and CSpace, and that you
         must fill these out.
 
+## Prerequisites
+
+1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up)
+2. [Hello world tutorial](https://docs.sel4.systems/Tutorials/hello-world)
+
+
 ## Initialising
 
-/*? macros.tutorial_init("dynamic-1") ?*/
+/*? macros.tutorial_init("libraries-1") ?*/
+
+<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("libraries-1") ?*/
+
+Answers are also available in drop down menus under each section.
+</details>
 
 ## Exercises
 
@@ -103,16 +112,22 @@ It also sets up the IPC buffer so that it can perform some syscalls such as `seL
 /*? task_1_desc ?*/
 /*-- filter TaskContent("task-1", TaskContentType.BEFORE) -*/
 /*-- endfilter -*/
-/*-- filter ExcludeDocs() -*/
+}
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-1", TaskContentType.COMPLETED) -*/
     info = platsupport_get_bootinfo();
 /*-- endfilter -*/
-/*-- endfilter -*/
-}
 ```
+</details>
+
 On success, you should see the following:
 ```
-dynamic-1: main@main.c:124 [Cond failed: allocman == NULL]
+libraries-1: main@main.c:124 [Cond failed: allocman == NULL]
 /*-- filter TaskCompletion("task-1", TaskContentType.COMPLETED) -*/
 	Failed to initialize alloc manager.
 	Memory pool sufficiently sized?
@@ -135,13 +150,16 @@ You need to initialize it with some default state before using it.
     */
 /*-- endset -*/
 /*? task_2_desc ?*/
-/*-- filter ExcludeDocs() -*/
+```
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-2", TaskContentType.COMPLETED, completion="Memory pool pointer valid?") -*/
     simple_default_init_bootinfo(&simple, info);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
-
+</details>
 On successful completion of this task, the output should not change.
 
 ### Use simple to print BootInfo
@@ -157,12 +175,18 @@ Use a `simple` function to print out the contents of the `seL4_BootInfo` functio
      */
 /*-- endset -*/
 /*? task_3_desc ?*/
-/*-- filter ExcludeDocs() -*/
+
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-3", TaskContentType.COMPLETED) -*/
     simple_print(&simple);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
 
 - <https://github.com/seL4/seL4_libs/blob/master/libsel4simple/include/simple/simple.h>
 
@@ -181,7 +205,7 @@ untypeds:        [316 --> 406)
 Initial thread domain: 0
 Initial thread cnode size:
 /*-- endfilter -*/
-dynamic-1: main@main.c:126 [Cond failed: allocman == NULL]
+libraries-1: main@main.c:126 [Cond failed: allocman == NULL]
 ```
 
 ### Initialise an allocator
@@ -209,16 +233,23 @@ step.
      */
 /*-- endset -*/
 /*? task_4_desc ?*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-4", TaskContentType.COMPLETED, completion="main: hello world") -*/
     allocman = bootstrap_use_current_simple(&simple, ALLOCATOR_STATIC_POOL_SIZE, allocator_mem_pool);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
+
 The output should now be as follows:
+
 ```
-<<seL4(CPU 0) [decodeInvocation/530 T0xffffff801ffb5400 "dynamic-1" @401303]: Attempted to invoke a null cap #0.>>
-dynamic-1: main@main.c:199 [Err seL4_InvalidCapability]:
+<<seL4(CPU 0) [decodeInvocation/530 T0xffffff801ffb5400 "libraries-1" @401303]: Attempted to invoke a null cap #0.>>
+libraries-1: main@main.c:199 [Err seL4_InvalidCapability]:
 /*-- filter TaskCompletion("task-4", TaskContentType.COMPLETED) -*/
 	Failed to set the priority for the new TCB object.
 /*-- endfilter -*/
@@ -245,12 +276,17 @@ and the VKA library simplifies this for you, among other things.
      */
 /*-- endset -*/
 /*? task_5_desc ?*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-5", TaskContentType.COMPLETED, completion="Failed to set the priority for the new TCB object.") -*/
     allocman_make_vka(&vka, allocman);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
 
 On successful completion this task, the output should not change.
 
@@ -267,12 +303,18 @@ On successful completion this task, the output should not change.
     seL4_CPtr cspace_cap;
 /*-- endset -*/
 /*? task_6_desc ?*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-6", TaskContentType.COMPLETED, completion="Failed to set the priority for the new TCB object.") -*/
     cspace_cap = simple_get_cnode(&simple);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
+
 This is where the differences between seL4 and contemporary kernels
 begin to start playing out. Every kernel-object that you "retype" will
 be handed to you using a capability reference. The seL4 kernel keeps
@@ -307,12 +349,19 @@ On successful completion this task, the output should not change.
     seL4_CPtr pd_cap;
 /*-- endset -*/
 /*? task_7_desc ?*/
-/*-- filter ExcludeDocs() -*/
+
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-7", TaskContentType.COMPLETED, completion="Failed to set the priority for the new TCB object.") -*/
     pd_cap = simple_get_pd(&simple);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
+
 Just as in the previous step, you were made to grab a reference to the
 root of your thread's CSpace, now you're being made to grab a reference
 to the root of your thread's VSpace.
@@ -335,12 +384,18 @@ On successful completion this task, the output should not change.
     vka_object_t tcb_object = {0};
 /*-- endset -*/
 /*? task_8_desc ?*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-8", TaskContentType.COMPLETED) -*/
     error = vka_alloc_tcb(&vka, &tcb_object);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
+
 In order to manage the threads that are created in seL4, the seL4 kernel
 keeps track of TCB (Thread Control Block) objects. Each of these
 represents a schedulable executable resource. Unlike other contemporary
@@ -382,12 +437,18 @@ main: hello world
      */
 /*-- endset -*/
 /*? task_9_desc ?*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-9", TaskContentType.COMPLETED, completion="main: hello world") -*/
     error = seL4_TCB_Configure(tcb_object.cptr, seL4_CapNull,  cspace_cap, seL4_NilData, pd_cap, seL4_NilData, 0, 0);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
+
 You must create a new VSpace for your new thread if you need it to
 execute in its own isolated address space, and tell the kernel which
 VSpace you plan for the new thread to execute in. This opens up the
@@ -415,12 +476,18 @@ On successful completion this task, the output should not change.
     /* hint: we've done thread naming before */
 /*-- endset -*/
 /*? task_10_desc ?*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-10", TaskContentType.COMPLETED, completion="main: hello world") -*/
-    NAME_THREAD(tcb_object.cptr, "dynamic-1: thread_2");
-/*-- endfilter -*/
+    NAME_THREAD(tcb_object.cptr, "libraries-1: thread_2");
 /*-- endfilter -*/
 ```
+</details>
+
 This is a convenience function -- sets a name string for the TCB object.
 
 On successful completion this task, the output should not change.
@@ -443,12 +510,18 @@ On successful completion this task, the output should not change.
      */
 /*-- endset -*/
 /*? task_11_desc ?*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-11", TaskContentType.COMPLETED, completion="main: hello world") -*/
     sel4utils_set_instruction_pointer(&regs, (seL4_Word)thread_2);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
+
 Pay attention to the line that precedes this particular task -- the line
 that zeroes out a new "seL4_UserContext" object. As we previously
 explained, seL4 requires you to fill out the Thread Control Block
@@ -472,12 +545,18 @@ On successful completion this task, the output should not change.
      */
 /*-- endset -*/
 /*? task_12_desc ?*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-12", TaskContentType.COMPLETED, completion="main: hello world") -*/
     sel4utils_set_stack_pointer(&regs, thread_2_stack_top);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
+
 This TASK is just some pointer arithmetic. The cautionary note that the
 stack grows down is meant to make you think about the arithmetic.
 Processor stacks push new values toward decreasing addresses, so give it
@@ -502,12 +581,18 @@ On successful completion this task, the output should not change.
      */
 /*-- endset -*/
 /*? task_13_desc ?*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-13", TaskContentType.COMPLETED, completion="main: hello world") -*/
     error = seL4_TCB_WriteRegisters(tcb_object.cptr, 0, 0, 2, &regs);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
+
 As explained above, we've been filling out our new thread's TCB for the
 last few operations, so now we're writing the values we've chosen, to
 the TCB object in the kernel.
@@ -526,12 +611,18 @@ On successful completion this task, the output should not change.
      */
 /*-- endset -*/
 /*? task_14_desc ?*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-14", TaskContentType.COMPLETED, completion="main: hello world") -*/
     error = seL4_TCB_Resume(tcb_object.cptr);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
+
 Finally, we tell the kernel that our new thread is runnable. From here,
 the kernel itself will choose when to run the thread based on the
 priority we gave it, and according to the kernel's configured scheduling
@@ -547,13 +638,19 @@ On successful completion this task, the output should not change.
     /* hint: printf() */
 /*-- endset -*/
 /*? task_15_desc ?*/
-/*-- filter ExcludeDocs() -*/
+}
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-15", TaskContentType.COMPLETED, completion="thread_2: hallo wereld") -*/
     printf("thread_2: hallo wereld\n");
 /*-- endfilter -*/
-/*-- endfilter -*/
-}
 ```
+</details>
+
 For the sake of confirmation that our new thread was executed by the
 kernel successfully, we cause it to print something to the screen.
 
@@ -574,7 +671,7 @@ On success, you should see output from your new thread.
 
 That's it for this tutorial.
 
-/*? macros.help_block() ?*/
+
 
 /*-- filter ExcludeDocs() -*/
 /*? ExternalFile("CMakeLists.txt") ?*/
@@ -656,8 +753,8 @@ int main(void) {
      * It is part of the root task's boot environment and defined in bootinfo.h from libsel4:
      * https://docs.sel4.systems/Tutorials/seL4_Tutorial_2#globals-links:
      */
-    zf_log_set_tag_prefix("dynamic-1:");
-    NAME_THREAD(seL4_CapInitThreadTCB, "dynamic-1");
+    zf_log_set_tag_prefix("libraries-1:");
+    NAME_THREAD(seL4_CapInitThreadTCB, "libraries-1");
 
     /*? task_2_desc ?*/
     /*? include_task_type_append([("task-2")]) ?*/
diff --git a/tutorials/dynamic-2/CMakeLists.txt b/tutorials/libraries-2/CMakeLists.txt
similarity index 70%
rename from tutorials/dynamic-2/CMakeLists.txt
rename to tutorials/libraries-2/CMakeLists.txt
index 5eef8e1f..8e6dbe71 100644
--- a/tutorials/dynamic-2/CMakeLists.txt
+++ b/tutorials/libraries-2/CMakeLists.txt
@@ -8,19 +8,19 @@ include(${SEL4_TUTORIALS_DIR}/settings.cmake)
 sel4_tutorials_regenerate_tutorial(${CMAKE_CURRENT_SOURCE_DIR})
 
 cmake_minimum_required(VERSION 3.7.2)
-# declare the dynamic-2 CMake project and the languages it is written in
-project(dynamic-2 C ASM)
+# declare the libraries-2 CMake project and the languages it is written in
+project(libraries-2 C ASM)
 
 sel4_tutorials_setup_roottask_tutorial_environment()
 
-add_executable(dynamic-2 main.c)
+add_executable(libraries-2 main.c)
 
-target_link_libraries(dynamic-2
+target_link_libraries(libraries-2
     sel4
     muslc utils sel4tutorials
     sel4muslcsys sel4platsupport sel4utils sel4debug sel4allocman)
 
 include(rootserver)
-DeclareRootserver(dynamic-2)
+DeclareRootserver(libraries-2)
 
 /*? macros.cmake_check_script(state) ?*/
diff --git a/tutorials/dynamic-2/dynamic-2.md b/tutorials/libraries-2/libraries-2.md
similarity index 94%
rename from tutorials/dynamic-2/dynamic-2.md
rename to tutorials/libraries-2/libraries-2.md
index 082995f9..f2691de9 100644
--- a/tutorials/dynamic-2/dynamic-2.md
+++ b/tutorials/libraries-2/libraries-2.md
@@ -22,7 +22,7 @@
 'task-15',
 ]) ?*/
 
-# seL4 Dynamic Libraries: IPC
+# seL4 Libraries: IPC
 
 The tutorial is designed to
 teach the basics of seL4 IPC using Endpoint objects, and userspace
@@ -39,7 +39,7 @@ tutorial are filled out and you don't have to repeat them: in much the
 same way, we won't be repeating conceptual explanations on this page, if
 they were covered by a previous tutorial in the series.
 
-## Learning outcomes
+Learning outcomes:
 
 - Repeat the spawning of a thread. "''If it's nice, do it twice''"
         -- Caribbean folk-saying. Once again, the new thread will be
@@ -58,19 +58,27 @@ they were covered by a previous tutorial in the series.
         both an Endpoint and a Notification using "Bound Notifications".
 - Understand CSpace pointers, which are really just integers with
         multiple indexes concatenated into one. Understanding them well
-        however, is important to understanding how capabilities work. Be
-        sure you understand the diagram on the "**CSpace example and
-        addressing**" slide.
+        however, is important to understanding how capabilities work.
+
+## Prerequisites
+
+1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up)
+2. [Libraries: initialisation & threading](https://docs.sel4.systems/Tutorials/libraries-1)
+
 
 ## Initialising
 
-/*? macros.tutorial_init("dynamic-2") ?*/
+/*? macros.tutorial_init("libraries-2") ?*/
 
+<details markdown='1'>
+<summary><em>Hint:</em> tutorial solutions</summary>
+<br>
+All tutorials come with complete solutions. To get solutions run:
 
-## Prerequisites
+/*? macros.tutorial_init_with_solution("libraries-2") ?*/
 
-1. [Set up your machine](https://docs.sel4.systems/HostDependencies).
-1. [dynamic-1](https://docs.sel4.systems/Tutorials/dynamic-1)
+Answers are also available in drop down menus under each section.
+</details>
 
 ## Exercises
 
@@ -117,18 +125,26 @@ of a MMU-utilizing kernel apply.
     vka_object_t ipc_frame_object;
 /*-- endset -*/
 /*? task_1_desc ?*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-1", TaskContentType.COMPLETED) -*/
     error = vka_alloc_frame(&vka, IPCBUF_FRAME_SIZE_BITS, &ipc_frame_object);
     ZF_LOGF_IFERR(error, "Failed to alloc a frame for the IPC buffer.\n"
                   "\tThe frame size is not the number of bytes, but an exponent.\n"
                   "\tNB: This frame is not an immediately usable, virtually mapped page.\n")
 /*-- endfilter -*/
+```
+</details>
+
+/*-- filter ExcludeDocs() -*/
 /*--filter TaskCompletion("task-1", TaskContentType.ALL) -*/
 Booting all finished, dropped to user space
 /*-- endfilter -*/
 /*-- endfilter -*/
-```
 
 On completion, the output will not change.
 
@@ -181,17 +197,22 @@ into a VSpace, and the mapping of a new page-table into a VSpace.
      */
 /*-- endset -*/
 /*? task_2_desc ?*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-2", TaskContentType.COMPLETED) -*/
     error = seL4_ARCH_Page_Map(ipc_frame_object.cptr, pd_cap, ipc_buffer_vaddr,
                                seL4_AllRights, seL4_ARCH_Default_VMAttributes);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
 
 On completion, the output will be as follows:
 ```
-dynamic-2: main@main.c:260 [Err seL4_FailedLookup]:
+libraries-2: main@main.c:260 [Err seL4_FailedLookup]:
 /*--filter TaskCompletion("task-2", TaskContentType.COMPLETED) -*/
 	Failed to allocate new page table.
 /*-- endfilter -*/
@@ -216,17 +237,26 @@ page-table object to use as a leaf page-table in your VSpace.
          */
 /*-- endset -*/
 /*? task_3_desc ?*/
-/*-- filter ExcludeDocs() -*/
+ ```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-3", TaskContentType.COMPLETED) -*/
         vka_object_t pt_object;
         error =  vka_alloc_page_table(&vka, &pt_object);
 /*-- endfilter -*/
+```
+</details>
+
+On completion, you will see another fault.
+
+/*-- filter ExcludeDocs() -*/
 /*--filter TaskCompletion("task-3", TaskContentType.ALL) -*/
 Booting all finished, dropped to user space
 /*-- endfilter -*/
 /*-- endfilter -*/
- ```
-On completion, you will see another fault.
 
 ### Map a page table
 
@@ -259,17 +289,26 @@ try again to finally map the IPC-buffer's frame object into the VSpace.
          */
 /*-- endset -*/
 /*? task_4_desc ?*/
-/*-- filter ExcludeDocs() -*/
+```
+
+On completion, you will see another fault.
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-4", TaskContentType.COMPLETED) -*/
         error = seL4_ARCH_PageTable_Map(pt_object.cptr, pd_cap,
                                         ipc_buffer_vaddr, seL4_ARCH_Default_VMAttributes);
 /*-- endfilter -*/
+```
+
+</details>
+
+/*-- filter ExcludeDocs() -*/
 /*--filter TaskCompletion("task-4", TaskContentType.ALL)--*/
 Booting all finished, dropped to user space
 /*-- endfilter -*/
 /*-- endfilter -*/
-```
-On completion, you will see another fault.
 
 ### Map a page
 
@@ -285,19 +324,26 @@ should fail. Complete it and proceed.
          */
 /*-- endset -*/
 /*? task_5_desc ?*/
-/*-- filter ExcludeDocs() -*/
+
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-5", TaskContentType.COMPLETED) -*/
         error = seL4_ARCH_Page_Map(ipc_frame_object.cptr, pd_cap,
                                    ipc_buffer_vaddr, seL4_AllRights, seL4_ARCH_Default_VMAttributes);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
+
 On completion, you will see the following:
 ```
 /*--filter TaskCompletion("task-5", TaskContentType.COMPLETED) -*/
 main: hello world
 /*-- endfilter -*/
-dynamic-2: main@main.c:464 [Cond failed: seL4_MessageInfo_get_length(tag) != 1]
+libraries-2: main@main.c:464 [Cond failed: seL4_MessageInfo_get_length(tag) != 1]
 	Response data from thread_2 was not the length expected.
 	How many registers did you set with seL4_SetMR within thread_2?
 ```
@@ -329,12 +375,18 @@ and proceed.
      */
 /*-- endset -*/
 /*? task_6_desc ?*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-6", TaskContentType.COMPLETED, completion="main: hello world") -*/
     error = vka_alloc_endpoint(&vka, &ep_object);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
+
 On completion, the output will not change.
 
 ### Badge an endpoint
@@ -381,13 +433,19 @@ data, and know which sender you are. Complete the step and proceed.
      */
 /*-- endset -*/
 /*? task_7_desc ?*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-7", TaskContentType.COMPLETED, completion="main: hello world") -*/
     error = vka_mint_object(&vka, &ep_object, &ep_cap_path, seL4_AllRights,
                             EP_BADGE);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
+
 On completion, the output will not change.
 
 ### Message registers
@@ -439,17 +497,22 @@ transmitted in the message.
      */
 /*-- endset -*/
 /*? task_8_desc ?*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-8", TaskContentType.COMPLETED) -*/
     tag = seL4_MessageInfo_new(0, 0, 0, 1);
     seL4_SetMR(0, MSG_DATA);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
 
 On completion, the output should change as follows:
 ```
-dynamic-2: main@main.c:472 [Cond failed: msg != ~MSG_DATA]
+libraries-2: main@main.c:472 [Cond failed: msg != ~MSG_DATA]
 /*-- filter TaskCompletion("task-8", TaskContentType.COMPLETED) -*/
 	Response data from thread_2's content was not what was expected.
 /*-- endfilter -*/
@@ -507,12 +570,17 @@ response message, if the sender doesn't want it to.
      */
 /*-- endset -*/
 /*? task_9_desc ?*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-9", TaskContentType.COMPLETED) -*/
     tag = seL4_Call(ep_cap_path.capPtr, tag);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
 
 On completion, you should see thread_2 fault as follows:
 ```
@@ -528,6 +596,7 @@ in thread 0xffffff801ffb4400 "child of: 'rootserver'" at address (nil)
 With stack:
 ```
 
+
 ### Receive a reply
 
 While this task is out of order, since we haven't yet examined the
@@ -549,12 +618,18 @@ designated, single IPC buffer.
      */
 /*-- endset -*/
 /*?  task_10_desc ?*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-10", TaskContentType.COMPLETED, completion="thread_2: hallo wereld") -*/
     msg = seL4_GetMR(0);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
+
 On completion, the output should not change.
 
 ### Receive an IPC
@@ -586,12 +661,17 @@ explicitly interested in distinguishing the sender.
      */
 /*-- endset -*/
 /*? task_11_desc ?*/
-/*-- filter ExcludeDocs() -*/
+```
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-11", TaskContentType.COMPLETED) -*/
     tag = seL4_Recv(ep_object.cptr, &sender_badge);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
+
 On completion, the output should change slightly:
 ```
 /*-- filter TaskCompletion("task-11", TaskContentType.COMPLETED) -*/
@@ -621,7 +701,12 @@ Complete them and proceed to the next step.
      */
 /*-- endset -*/
 /*? task_12_desc ?*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-12", TaskContentType.COMPLETED, completion="thread_2: hallo wereld") -*/
     ZF_LOGF_IF(sender_badge != EP_BADGE,
                "Badge on the endpoint was not what was expected.\n");
@@ -630,8 +715,8 @@ Complete them and proceed to the next step.
                "Length of the data send from root thread was not what was expected.\n"
                "\tHow many registers did you set with seL4_SetMR, within the root thread?\n");
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
 
 On completion, the output should not change.
 
@@ -651,12 +736,18 @@ Again, just reading the data from the Message Registers.
      */
 /*-- endset -*/
 /*? task_13_desc ?*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-13", TaskContentType.COMPLETED, completion="main: hello world") -*/
     msg = seL4_GetMR(0);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
+
 On completion, the output should change slightly:
 ```
 /*--filter TaskCompletion("task-13", TaskContentType.COMPLETED) -*/
@@ -680,12 +771,18 @@ And writing Message Registers again.
      */
 /*-- endset -*/
 /*? task_14_desc ?*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-14", TaskContentType.COMPLETED, completion="main: hello world") -*/
     seL4_SetMR(0, msg);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
+
 On completion, the output should not change.
 
 ### Reply to a message
@@ -725,21 +822,28 @@ Complete the step and pat yourself on the back.
      */
 /*-- endset -*/
 /*? task_15_desc ?*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-15", TaskContentType.COMPLETED, completion="main: hello world") -*/
     seL4_ReplyRecv(ep_object.cptr, tag, &sender_badge);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
+
 On completion, the output should change, with the fault message replaced with the following:
 ```
 /*--filter TaskCompletion("task-15", TaskContentType.COMPLETED) -*/
 main: got a reply: [0xffff9e9e|0xffffffffffff9e9e]
 /*-- endfilter -*/
 ```
+
 That's it for this tutorial.
 
-/*? macros.help_block() ?*/
+
 
 /*- filter ExcludeDocs() -*/
 /*? ExternalFile("CMakeLists.txt") ?*/
@@ -849,8 +953,8 @@ int main(void) {
     ZF_LOGF_IF(info == NULL, "Failed to get bootinfo.");
 
     /* Set up logging and give us a name: useful for debugging if the thread faults */
-    zf_log_set_tag_prefix("dynamic-2:");
-    name_thread(seL4_CapInitThreadTCB, "dynamic-2");
+    zf_log_set_tag_prefix("libraries-2:");
+    name_thread(seL4_CapInitThreadTCB, "libraries-2");
 
     /* init simple */
     simple_default_init_bootinfo(&simple, info);
@@ -940,7 +1044,7 @@ int main(void) {
 
 
     /* give the new thread a name */
-    name_thread(tcb_object.cptr, "dynamic-2: thread_2");
+    name_thread(tcb_object.cptr, "libraries-2: thread_2");
 
     /* set start up registers for the new thread */
     seL4_UserContext regs = {0};
diff --git a/tutorials/dynamic-3/CMakeLists.txt b/tutorials/libraries-3/CMakeLists.txt
similarity index 76%
rename from tutorials/dynamic-3/CMakeLists.txt
rename to tutorials/libraries-3/CMakeLists.txt
index 226425ef..da97aab6 100644
--- a/tutorials/dynamic-3/CMakeLists.txt
+++ b/tutorials/libraries-3/CMakeLists.txt
@@ -8,8 +8,8 @@ include(${SEL4_TUTORIALS_DIR}/settings.cmake)
 sel4_tutorials_regenerate_tutorial(${CMAKE_CURRENT_SOURCE_DIR})
 
 cmake_minimum_required(VERSION 3.7.2)
-# declare the dynamic-3 CMake project and the languages it is written in
-project(dynamic-3 C ASM)
+# declare the libraries-3 CMake project and the languages it is written in
+project(libraries-3 C ASM)
 
 sel4_tutorials_setup_roottask_tutorial_environment()
 
@@ -20,13 +20,13 @@ target_link_libraries(app sel4runtime sel4 muslc utils sel4tutorials
 include(cpio)
 MakeCPIO(archive.o "$<TARGET_FILE:app>")
 
-add_executable(dynamic-3 archive.o main.c)
+add_executable(libraries-3 archive.o main.c)
 
-target_link_libraries(dynamic-3
+target_link_libraries(libraries-3
     sel4
     muslc utils sel4tutorials
     sel4muslcsys sel4platsupport sel4utils sel4debug sel4allocman)
 
 include(rootserver)
-DeclareRootserver(dynamic-3)
+DeclareRootserver(libraries-3)
 /*? macros.cmake_check_script(state) ?*/
diff --git a/tutorials/dynamic-3/dynamic-3.md b/tutorials/libraries-3/libraries-3.md
similarity index 92%
rename from tutorials/dynamic-3/dynamic-3.md
rename to tutorials/libraries-3/libraries-3.md
index 1588a1cf..b3102a76 100644
--- a/tutorials/dynamic-3/dynamic-3.md
+++ b/tutorials/libraries-3/libraries-3.md
@@ -15,7 +15,7 @@
 'task-8'
 ])?*/
 
-# seL4 Dynamic Libraries: Processes & Elf loading
+# seL4 Libraries: Processes & ELF loading
 
 This tutorial shows how a separate ELF file can be loaded and expanded into a
 VSpace, and subsequently executed, while facilitating IPC between the
@@ -31,7 +31,7 @@ tutorial are filled out and you don't have to repeat them: in much the
 same way, we won't be repeating conceptual explanations on this page, if
 they were covered by a previous tutorial in the series.
 
-## Learning outcomes
+Learning outcomes:
 
 - Once again, repeat the spawning of a thread: however, this time
         the two threads will only share the same vspace, but have
@@ -45,15 +45,25 @@ they were covered by a previous tutorial in the series.
 - Understand how minting a capability to a thread in another
         CSpace works.
 
+## Prerequisites
+
+1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up)
+2. [Libraries: IPC](https://docs.sel4.systems/Tutorials/libraries-2)
 
 ## Initialising
 
-/*? macros.tutorial_init("dynamic-3") ?*/
+/*? macros.tutorial_init("libraries-3") ?*/
 
-## Prerequisites
+<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("libraries-3") ?*/
+
+Answers are also available in drop down menus under each section.
+</details>
 
-1. [Set up your machine](https://docs.sel4.systems/HostDependencies).
-1. [dynamic-2](https://docs.sel4.systems/Tutorials/dynamic-2)
 
 ## Exercises
 
@@ -73,8 +83,8 @@ userImagePaging: [12 --> 15)
 untypeds:        [399 --> 488)
 Initial thread domain: 0
 Initial thread cnode size: 12
-dynamic-3: vspace_reserve_range_aligned@vspace.h:621 Not implemented
-dynamic-3: main@main.c:117 [Cond failed: virtual_reservation.res == NULL]
+libraries-3: vspace_reserve_range_aligned@vspace.h:621 Not implemented
+libraries-3: main@main.c:117 [Cond failed: virtual_reservation.res == NULL]
 /*-- filter TaskCompletion("task-1", TaskContentType.BEFORE) -*/
 	Failed to reserve a chunk of memory.
 /*-- endfilter -*/
@@ -115,18 +125,23 @@ function may seem tedious, it's doing some important things.
 /*? task_1_desc ?*/
 /*-- filter TaskContent("task-1", TaskContentType.BEFORE) -*/
 /*-- endfilter -*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-1", TaskContentType.COMPLETED) -*/
     error = sel4utils_bootstrap_vspace_with_bootinfo_leaky(&vspace,
                                                            &data, simple_get_pd(&simple), &vka, info);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
 
 On success, you should see a different error:
 
 ```
-<<seL4(CPU 0) [handleUnknownSyscall/106 T0xffffff801ffb5400 "dynamic-3" @40139e]: SysDebugNameThread: cap is not a TCB, halting>>
+<<seL4(CPU 0) [handleUnknownSyscall/106 T0xffffff801ffb5400 "libraries-3" @40139e]: SysDebugNameThread: cap is not a TCB, halting>>
 /*-- filter TaskCompletion("task-1", TaskContentType.COMPLETED) -*/
 halting...
 /*-- endfilter -*/
@@ -161,18 +176,23 @@ thread.
      */
 /*-- endset -*/
 /*? task_2_desc ?*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-2", TaskContentType.COMPLETED) -*/
     sel4utils_process_config_t config = process_config_default_simple(&simple, APP_IMAGE_NAME, APP_PRIORITY);
     error = sel4utils_configure_process_custom(&new_process, &vka, &vspace, config);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
 
 On success, you should see a different error:
 
 ```
- dynamic-3: main@main.c:196 [Cond failed: new_ep_cap == 0]
+ libraries-3: main@main.c:196 [Cond failed: new_ep_cap == 0]
 /*-- filter TaskCompletion("task-2", TaskContentType.COMPLETED) -*/
 	Failed to mint a badged copy of the IPC endpoint into the new thread's CSpace.
 	sel4utils_mint_cap_to_process takes a cspacepath_t: double check what you passed.
@@ -225,12 +245,18 @@ wouldn't know who was whom.
     seL4_CPtr new_ep_cap = 0;
 /*-- endset -*/
 /*? task_3_desc ?*/
-/*-- filter ExcludeDocs() -*/
+ ```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-3", TaskContentType.COMPLETED, completion="what you passed.") -*/
     vka_cspace_make_path(&vka, ep_object.cptr, &ep_cap_path);
 /*-- endfilter -*/
-/*-- endfilter -*/
- ```
+```
+</details>
+
 On success, the output should not change.
 
 ### Badge a capability
@@ -258,20 +284,25 @@ free slot that the VKA library found for us.
      */
 /*-- endset -*/
 /*? task_4_desc ?*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-4", TaskContentType.COMPLETED) -*/
     new_ep_cap = sel4utils_mint_cap_to_process(&new_process, ep_cap_path,
                                                seL4_AllRights, EP_BADGE);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
 
 On success, the output should look something like:
 
 ```
 NEW CAP SLOT: 6ac.
 main: hello world
-dynamic-3: main@main.c:247 [Cond failed: sender_badge != EP_BADGE]
+libraries-3: main@main.c:247 [Cond failed: sender_badge != EP_BADGE]
 /*-- filter TaskCompletion("task-4", TaskContentType.COMPLETED) -*/
 	The badge we received from the new thread didn't match our expectation
 /*-- endfilter -*/
@@ -311,7 +342,12 @@ communicate with us, we can let it run. Complete this step and proceed.
 
 /*-- endset -*/
 /*? task_5_desc ?*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-5", TaskContentType.COMPLETED) -*/
     new_ep_cap = sel4utils_mint_cap_to_process(&new_process, ep_cap_path,
                                                seL4_AllRights, EP_BADGE);
@@ -322,8 +358,9 @@ communicate with us, we can let it run. Complete this step and proceed.
 
     error = sel4utils_spawn_process_v(&new_process, &vka, &vspace, argc, (char**) &argv, 1);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
+
 
 On success, you should be able to see the second process running. The output should
 be as follows:
@@ -336,7 +373,7 @@ main@app.c:67 [Cond failed: msg != ~MSG_DATA]
 	Unexpected response from root thread.
 /*-- endfilter -*/
 main: hello world
-dynamic-3: main@main.c:255 [Cond failed: sender_badge != EP_BADGE]
+libraries-3: main@main.c:255 [Cond failed: sender_badge != EP_BADGE]
 	The badge we received from the new thread didn't match our expectation.
 ```
 
@@ -366,11 +403,19 @@ Then we verify the fidelity of the data that was transmitted.
 /*-- filter TaskCompletion("task-6", TaskContentType.COMPLETED) -*/
 	Unexpected response from root thread.
 /*-- endfilter -*/
+/*-- endfilter -*/
+```
+
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-6", TaskContentType.COMPLETED) -*/
     tag = seL4_Recv(ep_cap_path.capPtr, &sender_badge);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
 
 On success, the badge error should no longer be visible.
 
@@ -401,11 +446,18 @@ message sent by the new thread.
 /*-- filter TaskCompletion("task-7", TaskContentType.COMPLETED) -*/
 	Unexpected response from root thread.
 /*-- endfilter -*/
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-7", TaskContentType.COMPLETED) -*/
     seL4_ReplyRecv(ep_cap_path.capPtr, tag, &sender_badge);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
 
 On success, the output should not change.
 
@@ -434,14 +486,17 @@ that was sent, and that's the end.
     seL4_CPtr ep = (seL4_CPtr) atol(argv[0]);
 /*-- endset -*/
 /*? task_8_desc ?*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-8", TaskContentType.COMPLETED) -*/
     tag = seL4_Call(ep, tag);
-
-/*-- endfilter -*/
 /*-- endfilter -*/
 ```
-
+</details>
 On success, you should see the following:
 
 ```
@@ -454,13 +509,13 @@ process_2: got a reply: 0xffffffffffff9e9e
 
 That's it for this tutorial.
 
-/*? macros.help_block() ?*/
+
 /*-- filter ExcludeDocs() -*/
 /*? ExternalFile("CMakeLists.txt") ?*/
 ```
 /*-- filter File("main.c") -*/
 /*
- * Copyright 2017, Data61, CSIRO (ABN 41 687 119 230).
+ * Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
  *
  * SPDX-License-Identifier: BSD-2-Clause
  */
@@ -528,8 +583,8 @@ int main(void) {
     ZF_LOGF_IF(info == NULL, "Failed to get bootinfo.");
 
     /* Set up logging and give us a name: useful for debugging if the thread faults */
-    zf_log_set_tag_prefix("dynamic-3:");
-    NAME_THREAD(seL4_CapInitThreadTCB, "dynamic-3");
+    zf_log_set_tag_prefix("libraries-3:");
+    NAME_THREAD(seL4_CapInitThreadTCB, "libraries-3");
 
     /* init simple */
     simple_default_init_bootinfo(&simple, info);
@@ -571,7 +626,7 @@ int main(void) {
                   "\tBe sure you've passed the correct component name for the new thread!\n");
 
     /* give the new process's thread a name */
-    NAME_THREAD(new_process.thread.tcb.cptr, "dynamic-3: process_2");
+    NAME_THREAD(new_process.thread.tcb.cptr, "libraries-3: process_2");
 
     /* create an endpoint */
     vka_object_t ep_object = {0};
@@ -640,7 +695,7 @@ int main(void) {
 /*-- endfilter -*/
 /*-- filter File("app.c") -*/
 /*
- * Copyright 2017, Data61, CSIRO (ABN 41 687 119 230).
+ * Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
  *
  * SPDX-License-Identifier: BSD-2-Clause
  */
diff --git a/tutorials/dynamic-4/CMakeLists.txt b/tutorials/libraries-4/CMakeLists.txt
similarity index 76%
rename from tutorials/dynamic-4/CMakeLists.txt
rename to tutorials/libraries-4/CMakeLists.txt
index caaf7da7..ff7a0285 100644
--- a/tutorials/dynamic-4/CMakeLists.txt
+++ b/tutorials/libraries-4/CMakeLists.txt
@@ -8,8 +8,8 @@ include(${SEL4_TUTORIALS_DIR}/settings.cmake)
 sel4_tutorials_regenerate_tutorial(${CMAKE_CURRENT_SOURCE_DIR})
 
 cmake_minimum_required(VERSION 3.7.2)
-# declare the dynamic-4 CMake project and the languages it is written in
-project(dynamic-4 C ASM)
+# declare the libraries-4 CMake project and the languages it is written in
+project(libraries-4 C ASM)
 
 sel4_tutorials_setup_roottask_tutorial_environment()
 
@@ -24,13 +24,13 @@ target_link_libraries(client
 include(cpio)
 MakeCPIO(archive.o "$<TARGET_FILE:client>")
 
-add_executable(dynamic-4 archive.o main.c)
+add_executable(libraries-4 archive.o main.c)
 
-target_link_libraries(dynamic-4
+target_link_libraries(libraries-4
     sel4runtime sel4
     muslc utils sel4tutorials
     sel4muslcsys sel4platsupport sel4utils sel4debug sel4allocman)
 
 include(rootserver)
-DeclareRootserver(dynamic-4)
+DeclareRootserver(libraries-4)
 /*? macros.cmake_check_script(state) ?*/
diff --git a/tutorials/dynamic-4/dynamic-4.md b/tutorials/libraries-4/libraries-4.md
similarity index 90%
rename from tutorials/dynamic-4/dynamic-4.md
rename to tutorials/libraries-4/libraries-4.md
index a44677eb..3ac0ce21 100644
--- a/tutorials/dynamic-4/dynamic-4.md
+++ b/tutorials/libraries-4/libraries-4.md
@@ -11,31 +11,41 @@
 'task-4',
 'task-5'
 ])?*/
-# seL4 Dynamic Libraries: Timer tutorial
+# seL4 Libraries: Timer Tutorial
 
 This tutorial demonstrates how to set up and use a basic timer driver using the
-`seL4_libs` dynamic libraries.
+`seL4_libs` libraries.
 
 You'll observe that the things you've already covered in the other
 tutorials are already filled out and you don't have to repeat them: in
 much the same way, we won't be repeating conceptual explanations on this
 page, if they were covered by a previous tutorial in the series.
 
-## Learning outcomes
+Learning outcomes:
 
 - Allocate a notification object.
 - Set up a timer provided by `util_libs`.
 - Use `seL4_libs` and `util_libs` functions to manipulate timer and
       handle interrupts.
 
+## Prerequisites
+
+1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up)
+2. [Libraries: processes & elf loading](https://docs.sel4.systems/Tutorials/libraries-3)
+
 ## Initialising
 
-/*? macros.tutorial_init("dynamic-4") ?*/
+/*? macros.tutorial_init("libraries-4") ?*/
 
-## Prerequisites
+<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("libraries-4") ?*/
 
-1. [Set up your machine](https://docs.sel4.systems/HostDependencies).
-1. [dynamic-3](https://docs.sel4.systems/Tutorials/dynamic-3)
+Answers are also available in drop down menus under each section.
+</details>
 
 ## Exercises
 
@@ -82,13 +92,19 @@ interrupts on.
 /*? task_1_desc ?*/
 /*-- filter TaskContent("task-1", TaskContentType.BEFORE) -*/
 /*-- endfilter -*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-1", TaskContentType.COMPLETED) -*/
     error = vka_alloc_notification(&vka, &ntfn_object);
     assert(error == 0);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
+
 The output will not change as a result of completing this task.
 
 ### Initialise the timer
@@ -116,13 +132,19 @@ initialise a timer driver. Assign it to the `timer` global variable.
     assert(error == 0);
 /*-- endset -*/
 /*? task_2_desc ?*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-2", TaskContentType.COMPLETED) -*/
-    error = ltimer_default_init(&timer, ops, NULL, NULL); 
+    error = ltimer_default_init(&timer, ops, NULL, NULL);
     assert(error == 0);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
+
 After this change, the server will output non-zero for the tick value at the end.
 ```
 /*-- filter TaskCompletion("task-2", TaskContentType.COMPLETED) -*/
@@ -150,13 +172,19 @@ it.
      */
 /*-- endset -*/
 /*? task_3_desc ?*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-3", TaskContentType.COMPLETED) -*/
     error = ltimer_set_timeout(&timer, NS_IN_MS, TIMEOUT_PERIODIC);
     assert(error == 0);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
+
 The output will cease after the following line as a result of completing this task.
 ```
 /*-- filter TaskCompletion("task-3", TaskContentType.COMPLETED) -*/
@@ -167,7 +195,7 @@ main: got a message from 0x61 to sleep 2 seconds
 ### Handle the interrupt
 
 In order to receive more interrupts, you need to handle the interrupt in the driver
-and acknowledge the irq. 
+and acknowledge the irq.
 
 ```c
 /*-- set task_4_desc -*/
@@ -187,13 +215,24 @@ and acknowledge the irq.
 /*-- filter TaskCompletion("task-4", TaskContentType.COMPLETED) -*/
 main: got a message from 0x61 to sleep 2 seconds
 /*-- endfilter -*/
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-4", TaskContentType.COMPLETED) -*/
         seL4_Word badge;
         seL4_Wait(ntfn_object.cptr, &badge);
         sel4platsupport_irq_handle(&ops.irq_ops, MINI_IRQ_INTERFACE_NTFN_ID, badge);
 /*-- endfilter -*/
-/*-- endfilter -*/
+        count++;
+        if (count == 1000 * msg) {
+            break;
+        }
 ```
+</details>
 The timer interrupts are bound to the IRQ interface initialised in Task 2,
 hence when we receive an interrupt, we forward it to the interface and let it notify the timer driver.
 
@@ -213,7 +252,7 @@ timer client wakes up:
 /*-- set task_5_desc -*/
     /*
      * TASK 5: Stop the timer
-     * hint: ltimer_destroy 
+     * hint: ltimer_destroy
      */
 /*-- endset -*/
 /*? task_5_desc ?*/
@@ -222,16 +261,25 @@ timer client wakes up:
 timer client wakes up:
  got the current timer tick:
 /*-- endfilter -*/
+/*-- endfilter -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("task-5", TaskContentType.COMPLETED) -*/
     ltimer_destroy(&timer);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
+
+
 The output should not change on successful completion of completing this task.
 
 That's it for this tutorial.
 
-/*? macros.help_block() ?*/
+
 /*-- filter ExcludeDocs() -*/
 /*? ExternalFile("CMakeLists.txt") ?*/
 ```
@@ -311,7 +359,7 @@ int main(void) {
     ZF_LOGF_IF(info == NULL, "Failed to get bootinfo.");
 
     /* give us a name: useful for debugging if the thread faults */
-    name_thread(seL4_CapInitThreadTCB, "dynamic-4");
+    name_thread(seL4_CapInitThreadTCB, "libraries-4");
 
     /* init simple */
     simple_default_init_bootinfo(&simple, info);
@@ -349,7 +397,7 @@ int main(void) {
     assert(error == 0);
 
     /* give the new process's thread a name */
-    name_thread(new_process.thread.tcb.cptr, "dynamic-4: timer_client");
+    name_thread(new_process.thread.tcb.cptr, "libraries-4: timer_client");
 
     /* create an endpoint */
     vka_object_t ep_object = {0};
@@ -435,7 +483,7 @@ int main(void) {
 /*-- endfilter -*/
 /*-- filter File("client.c") -*/
 /*
- * Copyright 2017, Data61, CSIRO (ABN 41 687 119 230).
+ * Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
  *
  * SPDX-License-Identifier: BSD-2-Clause
  */
diff --git a/tutorials/mapping/mapping.md b/tutorials/mapping/mapping.md
index 9a8f811b..5ca70334 100644
--- a/tutorials/mapping/mapping.md
+++ b/tutorials/mapping/mapping.md
@@ -12,14 +12,24 @@ This tutorial provides an introduction to virtual memory management on seL4.
 
 ## Prerequisites
 
-1. [Set up your machine](https://docs.sel4.systems/HostDependencies).
+1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up)
 2. [Capabilities tutorial](https://docs.sel4.systems/Tutorials/capabilities)
 
-## Outcomes
+## Initialising
+
+/*? macros.tutorial_init("mapping") ?*/
+
+<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("mapping") ?*/
+
+Answers are also available in drop down menus under each section.
+</details>
 
-By the end of this tutorial, you should be familiar with:
 
-1. How to map and unmap virtual memory pages in seL4.
 
 ## Background
 
@@ -139,14 +149,17 @@ the number of bits in the virtual address that could not be resolved due to miss
     // TODO map a page directory object
 /*-- endfilter -*/
 ```
-/*-- filter ExcludeDocs() -*/
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
 ```c
 /*-- filter TaskContent("mapping-pd", TaskContentType.COMPLETED, subtask='pd',completion='Failed to map page') -*/
     error = seL4_X86_PageDirectory_Map(pd, seL4_CapInitThreadVSpace, TEST_VADDR, seL4_X86_Default_VMAttributes);
     assert(error == seL4_NoError);
 /*-- endfilter -*/
 ```
-/*-- endfilter -*/
+</details>
 
 On success, you should see the following:
 ```
@@ -167,14 +180,18 @@ Note that in the above output, the number of failed bits has changed from `30` t
     // TODO map a page table object
 /*-- endfilter -*/
 ```
-/*-- filter ExcludeDocs() -*/
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
 ```c
 /*-- filter TaskContent("mapping-pt", TaskContentType.COMPLETED, subtask='pt', completion='Caught cap fault') -*/
+    // map a page table object
     error = seL4_X86_PageTable_Map(pt, seL4_CapInitThreadVSpace, TEST_VADDR, seL4_X86_Default_VMAttributes);
     assert(error == seL4_NoError);
 /*-- endfilter -*/
 ```
-/*-- endfilter -*/
+</details>
 
 On success, you should see the following:
 ```
@@ -209,14 +226,18 @@ that the fault occured on (address).
     // TODO remap the page
 /*-- endfilter -*/
 ```
-/*-- filter ExcludeDocs() -*/
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
 ```c
 /*-- filter TaskContent("mapping-remap", TaskContentType.COMPLETED, subtask='remap', completion='Success!') -*/
     error = seL4_X86_Page_Map(frame, seL4_CapInitThreadVSpace, TEST_VADDR, seL4_ReadWrite, seL4_X86_Default_VMAttributes);
     assert(error == seL4_NoError);
 /*-- endfilter -*/
 ```
-/*-- endfilter -*/
+
+</details>
 
 ### Unmapping pages
 
@@ -232,7 +253,7 @@ to become more familiar with virtual memory management on seL4.
 * Port this tutorial to another architecture (ARM, RISCV).
 * Create a generic function for converting from `seL4_MappingFailedLookupLevel` to the required seL4 object.
 
-/*? macros.help_block() ?*/
+
 
 /*-- filter ExcludeDocs() -*/
 ```c
diff --git a/tutorials/mcs/mcs.md b/tutorials/mcs/mcs.md
index 9d19ed38..11308b12 100644
--- a/tutorials/mcs/mcs.md
+++ b/tutorials/mcs/mcs.md
@@ -5,13 +5,32 @@
 -->
 
 # MCS Extensions
-/*? declare_task_ordering(['mcs-start','mcs-periodic', 'mcs-unbind', 'mcs-bind', 'mcs-sporadic', 
+/*? declare_task_ordering(['mcs-start','mcs-periodic', 'mcs-unbind', 'mcs-bind', 'mcs-sporadic',
 'mcs-server','mcs-badge','mcs-fault']) ?*/
 
+This tutorial presents the features in the Mixed-Criticality System (MCS) extensions for seL4, which are currently undergoing
+verification. For further context on the new features, please see the
+[paper](https://trustworthy.systems/publications/csiro_full_text/Lyons_MAH_18.pdf) or [phd](https://github.com/pingerino/phd/blob/master/phd.pdf)
+ which provides a comprehensive background on the changes.
+
+Learn:
+1. About the MCS new kernel API.
+2. How to create and configure scheduling contexts.
+3. The jargon *passive server*.
+4. How to spawn round-robin and periodic threads.
+
 ## Prerequisites
 
-1. [Set up your machine](https://docs.sel4.systems/HostDependencies).
-2. You should be familiar with the seL4 Api. Otherwise do the [Mechanisms tutorials](https://docs.sel4.systems/Tutorials)
+1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up)
+2. [Hello world tutorial](https://docs.sel4.systems/Tutorials/hello-world)
+3. [Capabilities tutorial](https://docs.sel4.systems/Tutorials/capabilities)
+4. [Untyped tutorial](https://docs.sel4.systems/Tutorials/untyped)
+5. [Mapping tutorial](https://docs.sel4.systems/Tutorials/mapping)
+6. [Threads tutorial](https://docs.sel4.systems/Tutorials/threads)
+7. [IPC tutorial](https://docs.sel4.systems/Tutorials/ipc)
+8. [Notifications tutorial](https://docs.sel4.systems/Tutorials/notifications)
+9. [Interrupts tutorial](https://docs.sel4.systems/Tutorials/interrupts)
+10. [Fault handlers tutorial](https://docs.sel4.systems/Tutorials/fault-handlers)
 
 
 ## Initialising
@@ -20,43 +39,40 @@ Then initialise the tutorial:
 
 /*? macros.tutorial_init("mcs") ?*/
 
-## Outcomes
+<details markdown='1'>
+<summary><em>Hint:</em> tutorial solutions</summary>
+<br>
+All tutorials come with complete solutions. To get solutions run:
 
-This tutorial presents the features in the upcoming MCS extensions for seL4, which are currently undergoing
-verification. For further context on the new features, please see the 
-[paper](https://trustworthy.systems/publications/csiro_full_text/Lyons_MAH_18.pdf) or [phd](https://github.com/pingerino/phd/blob/master/phd.pdf)
- which provides a comprehensive background on the changes.
+/*? macros.tutorial_init_with_solution("mcs") ?*/
 
-1. Learn about the MCS new kernel API.
-1. Be able to create and configure scheduling contexts.
-2. Learn the jargon *passive server*.
-3. Spawn round-robin and periodic threads.
+</details>
 
 ## Background
 
 The MCS extensions provide capability-based access to CPU time, and provide mechanisms to limit the upper
-bound of execution of a thread. 
+bound of execution of a thread.
 
 ### Scheduling Contexts
 
-Scheduling contexts are a new object type in the kernel, which contain scheduling parameters amoung other 
-accounting details. Most importantly, scheduling contexts contain a *budget* and a *period*, which 
+Scheduling contexts are a new object type in the kernel, which contain scheduling parameters amoung other
+accounting details. Most importantly, scheduling contexts contain a *budget* and a *period*, which
 represent an upper bound on execution time allocated: the kernel will enforce that threads cannot execute
-for more than *budget* microseconds out of *period* microseconds. 
+for more than *budget* microseconds out of *period* microseconds.
 
 ### SchedControl
 
-Parameters for scheduling contexts are configured by invoking `seL4_SchedControl` capabilities, one of 
-which is provided per CPU. The invoked `seL4_SchedControl` determines which processing core that specific 
+Parameters for scheduling contexts are configured by invoking `seL4_SchedControl` capabilities, one of
+which is provided per CPU. The invoked `seL4_SchedControl` determines which processing core that specific
 scheduling context provides access to.
 
-Scheduling contexts can be configured as *full* or *partial*. Full scheduling contexts have `budget == 
+Scheduling contexts can be configured as *full* or *partial*. Full scheduling contexts have `budget ==
 period` and grant access to 100% of CPU time. Partial scheduling contexts grant access to an upper bound of
  `budget/period` CPU time.
 
-The code example below configures a 
-scheduling context with a budget and period both equal to 1000us. Because the budget and period are equal, 
-the scheduling context is treated as round-robin 
+The code example below configures a
+scheduling context with a budget and period both equal to 1000us. Because the budget and period are equal,
+the scheduling context is treated as round-robin
 
 ```c
 /*-- filter TaskContent("mcs-start", TaskContentType.ALL, subtask='configure') -*/
@@ -68,7 +84,7 @@ the scheduling context is treated as round-robin
 ### SchedContext Binding
 
 Thread control blocks (TCBs) must have a scheduling context configured with non-zero budget and period
- in order to be picked by the scheduler. This 
+ in order to be picked by the scheduler. This
 can by invoking the scheduling context capability with the `seL4_SchedContext_Bind` invocation, or by
 using `seL4_TCB_SetSchedParams`, which takes a scheduling context capability. Below is example code for
 binding a TCB and a scheduling context.
@@ -81,35 +97,35 @@ binding a TCB and a scheduling context.
 ```
 
 TCB's can only be bound to one scheduling context at a time, and vice versa. If a scheduling context has not
-been configured with any time, then although the TCB has a scheduling context it will remain ineligible 
-for scheduling. 
+been configured with any time, then although the TCB has a scheduling context it will remain ineligible
+for scheduling.
 
 ### Bounding execution
 
 For partial scheduling contexts, an upper bound on execution is enforced by seL4 using the *sporadic server*
 algorithm, which work by guaranteeing the *sliding window* constrain, meaning that during any period, the
-budget cannot be exceeded. This is achieved by tracking the eligible budget in chunks called 
-*replenishments* (abbreviated to `refills` in the API for brevity). A replenishment is simply an amount 
+budget cannot be exceeded. This is achieved by tracking the eligible budget in chunks called
+*replenishments* (abbreviated to `refills` in the API for brevity). A replenishment is simply an amount
  of time, and a timestamp from which that time can be consumed. We explain this now through an example:
 
-Consider a scheduling context with period *T* and budget *C*. Initially, the scheduling context has 
-a single replenishment of size *C* which is eligible to be used from time *t*. 
+Consider a scheduling context with period *T* and budget *C*. Initially, the scheduling context has
+a single replenishment of size *C* which is eligible to be used from time *t*.
 
 The scheduling context is scheduled at time *t* and blocks at time *t + n*. A new replenishment is then scheduled
 for time *t+T* for *n*. The existing replenishment is updated to *C - n*, subtracting the amount consumed.
-For further details on the sporadic server algorithm, see the 
+For further details on the sporadic server algorithm, see the
 [original paper](https://dl.acm.org/citation.cfm?id=917665).
 
 If the replenishment data structure is full, replenishments are merged and the upper bound on execution is
 reduced. For this reason, the bound on execution is configurable with the `extra_refills` parameter
-on scheduling contexts. By default, scheduling contexts contain only two parameters, meaning if a 
-scheduling context is blocked, switched or preempted more than twice, the rest of the budget is forfeit until 
-the next period. `extra_refills` provides more replenishment data structures in a scheduling context. Note 
+on scheduling contexts. By default, scheduling contexts contain only two parameters, meaning if a
+scheduling context is blocked, switched or preempted more than twice, the rest of the budget is forfeit until
+the next period. `extra_refills` provides more replenishment data structures in a scheduling context. Note
 that the higher the number of replenishments the more fragmentation of budget can occur, which will increase
 scheduling overhead.
 
-`extra_refills` itself is bounded by the size of a scheduling context, which is itself configurable. 
-On scheduling context creation a size can be specified, and must be `> seL4_MinSchedContextBits`. The 
+`extra_refills` itself is bounded by the size of a scheduling context, which is itself configurable.
+On scheduling context creation a size can be specified, and must be `> seL4_MinSchedContextBits`. The
 maximum number of extra refills that can fit into a specific scheduling context size can be calculated
 with the function `seL4_MaxExtraRefills()` provided in `libsel4`.
 
@@ -123,11 +139,11 @@ The seL4 scheduler is largely unchanged: the highest priority, non-blocked threa
 
 ### Passive servers
 
-The MCS extensions allow for RPC style servers to run on client TCBs' scheduling contexts. This is achived by 
-unbinding the scheduling context once a server is blocked on an endpoint, rendering the server *passive*. 
+The MCS extensions allow for RPC style servers to run on client TCBs' scheduling contexts. This is achived by
+unbinding the scheduling context once a server is blocked on an endpoint, rendering the server *passive*.
 Caller scheduling contexts are donated to the server on `seL4_Call` and returned on `seL4_ReplyRecv`.
 
-Passive servers can also receive scheduling contexts from their bound notification object, which is 
+Passive servers can also receive scheduling contexts from their bound notification object, which is
 achieved by binding a notification object using `seL4_SchedContext_Bind`.
 
 ### Timeout faults
@@ -136,34 +152,34 @@ Threads can register a timeout fault handler using `seL4_TCB_SetTimeoutEndpoint`
 handlers are optional and are raised when a thread's replenishment expires *and* they have a valid handler
 registered. The timeout fault message from the kernel contains the data word which can be used to identify the
 scheduling context that the thread was using when the timeout fault occurred, and the amount of time
-consumed by the thread since the last fault or `seL4_SchedContext_Consumed`. 
+consumed by the thread since the last fault or `seL4_SchedContext_Consumed`.
 
 ### New invocations
 
 * `seL4_SchedContext_Bind` - bind a TCB or Notification capability to the invoked scheduling context.
 * `seL4_SchedContext_Unbind` - unbind any objects from the invoked scheduling context.
 * `seL4_SchedContext_UnbindObject`- unbind a specific object from the invoked scheduling context.
-* `seL4_SchedContext_YieldTo` - if the thread running on the invoked scheduling context is 
-schedulable, place it at the head of the scheduling queue for its priority. For same priority threads, this 
-will result in the target thread being scheduled. Return the amount of time consumed by this scheduling 
+* `seL4_SchedContext_YieldTo` - if the thread running on the invoked scheduling context is
+schedulable, place it at the head of the scheduling queue for its priority. For same priority threads, this
+will result in the target thread being scheduled. Return the amount of time consumed by this scheduling
 context since the last timeout fault, `YieldTo` or `Consumed` invocation.
-* `seL4_SchedContext_Consumed` - Return the amount of time consumed by this scheduling 
+* `seL4_SchedContext_Consumed` - Return the amount of time consumed by this scheduling
 context since the last timeout fault, `YieldTo` or `Consumed` invocation.
 * `seL4_TCB_SetTimeoutEndpoint` - Set the timeout fault endpoint for a TCB.
 
 ### Reply objects
 
-The MCS API also makes the reply channel explicit: reply capabilities are now fully fledged objects 
+The MCS API also makes the reply channel explicit: reply capabilities are now fully fledged objects
 which must be provided by a thread on `seL4_Recv` operations. They are used to track the scheduling
 context donation chain and return donated scheduling contexts to callers.
 
-Please see the [release notes](https://docs.sel4.systems/sel4_release/seL4_9.0.0-mcs) and 
+Please see the [release notes](https://docs.sel4.systems/sel4_release/seL4_9.0.0-mcs) and
 [manual](https://docs.sel4.systems/sel4_release/seL4_9.0.0-mcs.html) for further details
- on the API changes. 
- 
+ on the API changes.
+
 ## Exercises
 
-In the initial state of the tutorial, the main function in `mcs.c` is running in one process, and the 
+In the initial state of the tutorial, the main function in `mcs.c` is running in one process, and the
 following loop from `spinner.c` is running in another process:
 
 
@@ -198,18 +214,24 @@ Yield
 /*-- filter TaskContent("mcs-start", TaskContentType.ALL, subtask='periodic') -*/
     //TODO reconfigure sched_context to be periodic
 /*-- endfilter -*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("mcs-periodic", TaskContentType.COMPLETED, subtask='periodic') -*/
     // reconfigure sched_context to be periodic
     error = seL4_SchedControl_Configure(sched_control, sched_context, 0.9 * US_IN_S, 1 * US_IN_S, 0, 0);
     ZF_LOGF_IF(error != seL4_NoError, "Failed to configure schedcontext");
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
+
 
 By completing this task successfully, the output will not change, but the rate that the output is
 printed will slow: each subsequent line should be output once the period has elapsed. You should now
-be able to see the loop where the `mcs.c` process and `spinner.c` process alternate, until the `mcs.c` 
+be able to see the loop where the `mcs.c` process and `spinner.c` process alternate, until the `mcs.c`
 process blocks, at which point `"Yield"` is emitted by `spinner.c` every second, as shown below:
 
 ```
@@ -237,12 +259,13 @@ Yield
 Yield
 /*-- endfilter -*/
 ```
-Before you completed this task, the scheduling context was round-robin, and so was 
-schedulable immediately after the call to `seL4_Yield`. 
+
+Before you completed this task, the scheduling context was round-robin, and so was
+schedulable immediately after the call to `seL4_Yield`.
 By changing
-the scheduling parameters of `sched_context` to periodic parameters (budget < period), each time 
-`seL4_Yield()` is called the available budget in the scheduling context is abandoned, causing the 
-thread to sleep until the next replenishment, determined by the period.  
+the scheduling parameters of `sched_context` to periodic parameters (budget < period), each time
+`seL4_Yield()` is called the available budget in the scheduling context is abandoned, causing the
+thread to sleep until the next replenishment, determined by the period.
 
 ### Unbinding scheduling contexts
 
@@ -253,16 +276,12 @@ thread state. Unbinding a scheduling context does not alter the thread state, bu
 from the scheduler queues.
 
 **Exercise** Unbind `sched_context` to stop the spinner process from running.
+
 ```c
 /*-- filter TaskContent("mcs-start", TaskContentType.ALL, subtask='unbind') -*/
-    //TODO unbind sched_context to stop yielding thread 
+    //TODO unbind sched_context to stop yielding thread
 /*- endfilter --*/
 /*-- filter ExcludeDocs() --*/
-/*-- filter TaskContent("mcs-unbind", TaskContentType.COMPLETED, subtask='unbind') -*/
-    // unbind sched_context to stop the yielding thread
-    error = seL4_SchedContext_Unbind(sched_context);
-    ZF_LOGF_IF(error, "Failed to unbind sched_context");
-/*-- endfilter -*/
 /*-- filter TaskCompletion("mcs-unbind", TaskContentType.COMPLETED) -*/
 Tick 6
 Yield
@@ -274,11 +293,25 @@ Tick 8
 /*-- endfilter --*/
 ```
 
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
+/*-- filter TaskContent("mcs-unbind", TaskContentType.COMPLETED, subtask='unbind') -*/
+    // unbind sched_context to stop the yielding thread
+    error = seL4_SchedContext_Unbind(sched_context);
+    ZF_LOGF_IF(error, "Failed to unbind sched_context");
+/*-- endfilter -*/
+```
+
+</details>
+
+
 On success, you should see the output from the yielding thread stop.
 
 ### Sporadic threads
 
-Your next task is to use a different process, `sender` to experiment with sporadic tasks. The 
+Your next task is to use a different process, `sender` to experiment with sporadic tasks. The
 `sender` process is ready to run, and just needs a scheduling context in order to do so.
 
 **Exercise** First, bind `sched_context` to `sender_tcb`.
@@ -287,15 +320,20 @@ Your next task is to use a different process, `sender` to experiment with sporad
 /*-- filter TaskContent("mcs-start", TaskContentType.ALL, subtask='bind') -*/
     //TODO bind sched_context to sender_tcb
 /*-- endfilter -*/
-/*-- filter ExcludeDocs() -*/
+```
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("mcs-bind", TaskContentType.COMPLETED, subtask='bind') -*/
     // bind sched_context to sender_tcb
     error = seL4_SchedContext_Bind(sched_context, sender_tcb);
     ZF_LOGF_IF(error != seL4_NoError, "Failed to bind schedcontext");
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
 
+</details>
+
 The output should look like the following:
 ```
 ...
@@ -307,12 +345,12 @@ Tock 6
 /*-- endfilter -*/
 ```
 
-Note the rate of the output: currently, you should see 2 lines come out at a time, with roughly  
+Note the rate of the output: currently, you should see 2 lines come out at a time, with roughly
 a second break between (the period of the scheduling context you set earlier). This is because
-scheduling context only has the minimum sporadic refills (see background), and each time a context switch 
-occurs a refill is used up to schedule another. 
+scheduling context only has the minimum sporadic refills (see background), and each time a context switch
+occurs a refill is used up to schedule another.
 
-**Exercise** Reconfigure the `sched_context` to an extra 6 refills, such that all of the `Tock` output 
+**Exercise** Reconfigure the `sched_context` to an extra 6 refills, such that all of the `Tock` output
 occurs in one go.
 
  ```c
@@ -320,11 +358,6 @@ occurs in one go.
     //TODO reconfigure sched_context to be periodic with 6 extra refills
 /*-- endfilter -*/
 /*-- filter ExcludeDocs() -*/
-/*-- filter TaskContent("mcs-sporadic", TaskContentType.COMPLETED, subtask='sporadic') -*/
-    // reconfigure sched_context to be periodic with 6 extra refills
-    error = seL4_SchedControl_Configure(sched_control, sched_context, 0.9 * US_IN_S, 1 * US_IN_S, 6, 0);
-    ZF_LOGF_IF(error != seL4_NoError, "Failed to configure schedcontext");
-/*-- endfilter -*/
 /*-- filter TaskCompletion("mcs-sporadic", TaskContentType.ALL) -*/
 Tock 4
 Tock 5
@@ -333,29 +366,47 @@ Tock 7
 /*-- endfilter -*/
 /*-- endfilter -*/
 ```
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
+/*-- filter TaskContent("mcs-sporadic", TaskContentType.COMPLETED, subtask='sporadic') -*/
+    // reconfigure sched_context to be periodic with 6 extra refills
+    error = seL4_SchedControl_Configure(sched_control, sched_context, 0.9 * US_IN_S, 1 * US_IN_S, 6, 0);
+    ZF_LOGF_IF(error != seL4_NoError, "Failed to configure schedcontext");
+/*-- endfilter -*/
+```
+
+</details>
+
 
 ### Passive servers
 
-Now look to the third process, `server.c`, which is a very basic echo server. It currently does 
+Now look to the third process, `server.c`, which is a very basic echo server. It currently does
 not have a scheduling context, and needs one to initialise.
 
-**Exercise** Bind `sched_context` to `server_tcb`. 
+**Exercise** Bind `sched_context` to `server_tcb`.
 
  ```c
 /*-- filter TaskContent("mcs-start", TaskContentType.ALL, subtask='server') -*/
     //TODO bind sched_context to server_tcb
 /*-- endfilter -*/
-/*-- filter ExcludeDocs() -*/
+```
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("mcs-server", TaskContentType.COMPLETED, subtask='server') -*/
     // bind the servers sched context
     error = seL4_SchedContext_Bind(sched_context, server_tcb);
     ZF_LOGF_IF(error != seL4_NoError, "Failed to bind sched_context to server_tcb");
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
 
+</details>
+
 Now you should see the server initialise and echo the messages sent. Note the initialisation protocol:
-first, you bound `sched_context` to the server. At this point, in `server.c`, the server calls 
+first, you bound `sched_context` to the server. At this point, in `server.c`, the server calls
 `seL4_NBSendRecv` which sends an IPC message on `endpoint`, indicating that the server is now initialised.
 The output should be as follows
 
@@ -374,7 +425,7 @@ Yield
 
 The following code then converts the server to passive:
 
-```c 
+```c
 /*-- filter TaskContent("mcs-start", TaskContentType.ALL, subtask='passive') -*/
     // convert to passive
     error = seL4_SchedContext_Unbind(sched_context);
@@ -407,7 +458,7 @@ to configure its own fault endpoint.
 The reason for this difference is merely that it is faster to lookup the fault
 endpoint this way since it is looked up only once at the time it is configured.
 
-#### Configuring a fault endpoint on the Master kernel:
+#### Configuring a fault endpoint on the Master kernel
 
 On the Master kernel the cap given to the kernel must be a cap to an object in
 the CSpace of the *faulting thread*.
@@ -415,9 +466,9 @@ the CSpace of the *faulting thread*.
 On the Master kernel, the fault endpoint cap is looked up from within the CSpace
 of the faulting thread everytime a fault occurs.
 
-#### Exercise:
+#### Exercise
 
-**Exercise** Set the data field of `sched_context` using `seL4_SchedControl_Configure` and set a 10s period, 1ms 
+**Exercise** Set the data field of `sched_context` using `seL4_SchedControl_Configure` and set a 10s period, 1ms
 budget and 0 extra refills.
 
 ```c
@@ -425,12 +476,6 @@ budget and 0 extra refills.
     //TODO reconfigure sched_context with 10s period, 1ms budget, 0 extra refills and data of 5.
 /*-- endfilter -*/
 /*-- filter ExcludeDocs() -*/
-/*-- filter TaskContent("mcs-badge", TaskContentType.COMPLETED, subtask='badge') -*/
-
-    // reconfigure sched_context with 1s period, 500 microsecond budget, 0 extra refills and data of 5.
-    error = seL4_SchedControl_Configure(sched_control, sched_context, 500, US_IN_S, 0, 5);
-    ZF_LOGF_IF(error != seL4_NoError, "Failed to configure sched_context");
-/*-- endfilter -*/
 /*-- filter TaskCompletion("mcs-badge", TaskContentType.COMPLETED) -*/
 Tock 8
 Starting server
@@ -442,24 +487,44 @@ echo server
 /*-- endfilter -*/
 /*-- endfilter -*/
 ```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
+/*-- filter TaskContent("mcs-badge", TaskContentType.COMPLETED, subtask='badge') -*/
+
+    // reconfigure sched_context with 1s period, 500 microsecond budget, 0 extra refills and data of 5.
+    error = seL4_SchedControl_Configure(sched_control, sched_context, 500, US_IN_S, 0, 5);
+    ZF_LOGF_IF(error != seL4_NoError, "Failed to configure sched_context");
+/*-- endfilter -*/
+```
+
+</details>
+
 The code then binds the scheduling context back to `spinner_tcb`, which starts yielding again.
 
-**Exercise** set the timeout fault endpoint for `spinner_tcb`. 
+**Exercise** set the timeout fault endpoint for `spinner_tcb`.
 
 
 ```c
 /*-- filter TaskContent("mcs-start", TaskContentType.ALL, subtask='fault') -*/
     //TODO set endpoint as the timeout fault handler for spinner_tcb
 /*-- endfilter -*/
-/*-- filter ExcludeDocs() -*/
+```
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("mcs-fault", TaskContentType.COMPLETED, subtask='fault') -*/
     // set endpoint as the timeout fault handler for spinner_tcb
     error = seL4_TCB_SetTimeoutEndpoint(spinner_tcb, endpoint);
     ZF_LOGF_IF(error != seL4_NoError, "Failed to set timeout fault endpoint for spinner");
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
 
+</details>
+
 When the `spinner` faults, you should see the following output:
 
 ```
@@ -475,10 +540,10 @@ That's all for the detailed content of this tutorial. Below we list other ideas
 to become more familiar with the MCS extensions.
 
 * Set up a passive server with a timeout fault handlers, with policies for clients that exhaust their budget.
-* Experiment with notification binding on a passive server, by binding both a notification object to the 
+* Experiment with notification binding on a passive server, by binding both a notification object to the
 server TCB and an SC to the notification object.
 
-/*? macros.help_block() ?*/
+
 
 /*-- filter ExcludeDocs() -*/
 ```c
@@ -557,7 +622,7 @@ int main(int c, char *argv[]) {
 /*? capdl_elf_tcb("spinner", "spinner_tcb") ?*/
 // capability to the tcb of the sender process
 /*? capdl_elf_tcb("sender", "sender_tcb") ?*/
-// capability to an endpoint, shared with 'sender' and 'server' 
+// capability to an endpoint, shared with 'sender' and 'server'
 /*? capdl_alloc_cap(seL4_EndpointObject, "endpoint", "endpoint", write=True, read=True, grant=True) ?*/
 // capability to a reply object
 /*? capdl_alloc_cap(seL4_RTReplyObject, "reply2", "reply", write=True, read=True, grant=True) ?*/
@@ -570,7 +635,7 @@ int main(int c, char *argv[]) {
     // bind it to `spinner_tcb`
     /*? include_task_type_append([("mcs-start", 'bind_yield')]) ?*/
 
-    int i = 0; 
+    int i = 0;
     for (; i < 9; i++) {
         seL4_Yield();
         printf("Tick %d\n", i);
@@ -584,11 +649,11 @@ int main(int c, char *argv[]) {
         seL4_Wait(endpoint, NULL);
         printf("Tock %d\n", (int) seL4_GetMR(0));
     }
- 
-    
+
+
     error = seL4_SchedContext_UnbindObject(sched_context, sender_tcb);
     ZF_LOGF_IF(error, "Failed to unbind sched_context from sender_tcb");
-    
+
     /* suspend the sender to get them off endpoint */
     error = seL4_TCB_Suspend(sender_tcb);
     ZF_LOGF_IF(error, "Failed to suspend sender_tcb");
@@ -598,19 +663,19 @@ int main(int c, char *argv[]) {
     printf("Starting server\n");
     /*? include_task_type_replace([("mcs-start", 'server'), ("mcs-server", 'server')]) ?*/
     // wait for it to initialise
-    printf("Wait for server\n"); 
+    printf("Wait for server\n");
     seL4_Wait(endpoint, NULL);
-   
+
     /*? include_task_type_append([("mcs-start", 'passive')]) ?*/
     ZF_LOGF_IF(error != seL4_NoError, "Failed to unbind sched context");
 
     const char *messages[] = {
-        "running", 
+        "running",
         "passive",
         "echo server",
         NULL,
     };
- 
+
     for (int i = 0; messages[i] != NULL; i++) {
         int m = 0;
         for (; m < strlen(messages[i]) && m < seL4_MsgMaxLength; m++) {
@@ -621,7 +686,7 @@ int main(int c, char *argv[]) {
 
     /*? include_task_type_replace([("mcs-start", 'badge'), ("mcs-badge", 'badge')]) ?*/
     /*? include_task_type_replace([("mcs-start", 'fault'), ("mcs-fault", 'fault')]) ?*/
-    
+
     error = seL4_SchedContext_Bind(sched_context, spinner_tcb);
     ZF_LOGF_IF(error, "Failed to bind sched_context to spinner_tcb");
 
@@ -631,7 +696,7 @@ int main(int c, char *argv[]) {
     ZF_LOGF_IF(seL4_Fault_get_seL4_FaultType(fault) != seL4_Fault_Timeout, "Not a timeout fault");
     printf("Received timeout fault\n");
     ZF_LOGF_IF(seL4_Fault_Timeout_get_data(fault) != 5, "Incorrect data");
-    
+
     printf("Success!\n");
 
     return 0;
diff --git a/tutorials/notifications/notifications.md b/tutorials/notifications/notifications.md
index 00106a4c..121b3d62 100644
--- a/tutorials/notifications/notifications.md
+++ b/tutorials/notifications/notifications.md
@@ -7,18 +7,54 @@
 /*? declare_task_ordering(['ntfn-start', 'ntfn-shmem', 'ntfn-signal', 'ntfn-badge']) ?*/
 # Notifications and shared memory
 
+This tutorial covers notification objects.
+
+You will learn how to:
+1. Set up shared memory between tasks.
+2. Use notification objects for synchronisation between tasks.
+3. Use badges to differentiate notifications.
+
 ## Prerequisites
 
-1. [Set up your machine](https://docs.sel4.systems/HostDependencies).
-1. [Capabilities tutorial](https://docs.sel4.systems/Tutorials/capabilities)
-1. [Mapping tutorial](https://docs.sel4.systems/Tutorials/mapping)
-1. [Threads tutorial](https://docs.sel4.systems/Tutorials/threads)
+1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up)
+2. [Capabilities tutorial](https://docs.sel4.systems/Tutorials/capabilities)
+3. [Mapping tutorial](https://docs.sel4.systems/Tutorials/mapping)
+4. [Threads tutorial](https://docs.sel4.systems/Tutorials/threads)
+
+## Initialising
+
+/*? macros.tutorial_init("notifications") ?*/
+
+
+<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("notifications") ?*/
+
+Answers are also available in drop down menus under each section.
+</details>
+
+## CapDL Loader
+
+This tutorial uses the *capDL loader*, a root task which allocates statically
+ configured objects and capabilities.
 
-## Outcomes
+<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.
 
-1. Understand how to set up shared memory between tasks.
-2. Be able to use notification objects for synchronisation between tasks.
-4. Know how to use badges to differentiate notifications.
+More information about CapDL projects can be found [here](https://docs.sel4.systems/CapDL.html).
+
+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>
 
 ## Background
 
@@ -69,10 +105,10 @@ timer tutorial. <!--TODO link to timer tutorial -->
 
 ## Exercises
 
-These exercises guide you through a basic producer consumer set up using notifications and shared memory. The 
+These exercises guide you through a basic producer consumer set up using notifications and shared memory. The
 tutorial uses the capDL loader, and already has 2 producer processes (`producer_1.c` and `producer_2`) and 1 consumer
- process running (`consumer.c`). Each has access to a number of capabilities. 
- 
+ process running (`consumer.c`). Each has access to a number of capabilities.
+
 Each producer shares a buffer with the consumer, and the consumer processes data from both producers when it is
 available.
 
@@ -83,18 +119,18 @@ Waiting for producer
 ```
 ### Set up shared memory
 
-Both producers start and block immediately, waiting for the consumer to send an IPC with the address of the shared 
+Both producers start and block immediately, waiting for the consumer to send an IPC with the address of the shared
 mapping. We provide code below that sets up the shared page between producer 1 and the consumer:
 
-```c 
+```c
 /*-- filter TaskContent("ntfn-start", TaskContentType.ALL, subtask="shmem1", completion="Caught cap fault in send phase") -*/
     /* set up shared memory for consumer 1 */
     /* first duplicate the cap */
-    error = seL4_CNode_Copy(cnode, mapping_1, seL4_WordBits, 
+    error = seL4_CNode_Copy(cnode, mapping_1, seL4_WordBits,
                           cnode, buf1_frame_cap, seL4_WordBits, seL4_AllRights);
     ZF_LOGF_IFERR(error, "Failed to copy cap");
     /* now do the mapping */
-    error = seL4_ARCH_Page_Map(mapping_1, producer_1_vspace, BUF_VADDR, 
+    error = seL4_ARCH_Page_Map(mapping_1, producer_1_vspace, BUF_VADDR,
                                seL4_AllRights, seL4_ARCH_Default_VMAttributes);
     ZF_LOGF_IFERR(error, "Failed to map frame");
 
@@ -103,16 +139,21 @@ mapping. We provide code below that sets up the shared page between producer 1 a
 
 However, we do not map the second buffer in, so producer 2 crashes immediately.
 
-**Exercise** Understand the above code, and create a second shared page between `producer_2` and `consumer`. 
+**Exercise** Understand the above code, and create a second shared page between `producer_2` and `consumer`.
 
-```c 
+```c
 /*-- filter TaskContent("ntfn-start", TaskContentType.ALL, subtask="shmem2", completion="Caught cap fault in send phase") -*/
     // TODO share buf2_frame_cap with producer_2
 /*-- endfilter -*/
-/*-- filter ExcludeDocs() -*/
+
+```
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("ntfn-shmem", TaskContentType.COMPLETED, subtask="shmem2", completion="Waiting for producer") -*/
     /* set up shared memory for producer 2 */
-    error = seL4_CNode_Copy(cnode, mapping_2, seL4_WordBits, 
+    error = seL4_CNode_Copy(cnode, mapping_2, seL4_WordBits,
                             cnode, buf2_frame_cap, seL4_WordBits, seL4_AllRights);
     ZF_LOGF_IFERR(error, "Failed to copy cap");
    /* now do the mapping */
@@ -120,14 +161,14 @@ However, we do not map the second buffer in, so producer 2 crashes immediately.
                                seL4_AllRights, seL4_ARCH_Default_VMAttributes);
     ZF_LOGF_IFERR(error, "Failed to map frame");
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
 
 Whether this is successful will be visible after the next exercise when the consumers access their buffers. If the shared page setup for producer 2 is not correct, it will fail with a vm fault.
 
 ### Signal the producers to go
 
-At this point, both producers are waiting on the `empty` notification for a signal that the buffer is ready 
+At this point, both producers are waiting on the `empty` notification for a signal that the buffer is ready
 to be written to.
 
 **Exercise** signal both producers via the `buf1_empty` and `buf2_empty` notification objects.
@@ -136,13 +177,18 @@ to be written to.
 /*-- filter TaskContent("ntfn-start", TaskContentType.ALL, subtask="signal", completion="Waiting for producer") -*/
     // TODO signal both producers
 /*-- endfilter -*/
-/*-- filter ExcludeDocs() -*/
+```
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("ntfn-signal", TaskContentType.COMPLETED, subtask="signal", completion="Got badge") -*/
     seL4_Signal(buf1_empty);
     seL4_Signal(buf2_empty);
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
+
 
 ### Differentiate signals
 
@@ -164,13 +210,18 @@ which of the producers (it may be both) has produced data.
 
 **Exercise** Check the badge and signal the empty notification for the producers according to the bits set in the badge
  value.
- 
+
 ```c
 /*-- filter TaskContent("ntfn-start", TaskContentType.ALL, subtask="badge", completion="Got badge") -*/
-    // TODO, use the badge to check which producer has signalled you, and signal it back. Note that you 
+    // TODO, use the badge to check which producer has signalled you, and signal it back. Note that you
     // may recieve more than 1 signal at a time.
 /*-- endfilter -*/
-/*-- filter ExcludeDocs() -*/
+
+```
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("ntfn-badge", TaskContentType.COMPLETED, subtask="badge", completion="Success") -*/
         if (badge & 0b01) {
             assert(*buf1 == 1);
@@ -183,20 +234,20 @@ which of the producers (it may be both) has produced data.
             seL4_Signal(buf2_empty);
         }
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
 
 At this point, you should see signals from both producers being processed, and the final `Success!` message printed.
- 
+
 ### Further exercises
 
 That's all for the detailed content of this tutorial. Below we list other ideas for exercises you can try,
 to become more familiar with IPC.
 
 * Create a counting semaphore implementation using notification objects.
-* Create a bounded-buffer producer consumer with a buffer size greater than 1. 
+* Create a bounded-buffer producer consumer with a buffer size greater than 1.
+
 
-/*? macros.help_block() ?*/
 
 /*-- filter ExcludeDocs() -*/
 
@@ -204,7 +255,7 @@ to become more familiar with IPC.
 /*-- filter TaskContent("ntfn-start", TaskContentType.ALL, subtask="producer", completion="Waiting for producer") -*/
     seL4_Recv(endpoint, NULL);
     volatile long *buf = (volatile long *) seL4_GetMR(0);
-    
+
     for (int i = 0; i < 100; i++) {
         seL4_Wait(empty, NULL);
         printf("%d: produce\n", id);
@@ -291,7 +342,7 @@ int main(int c, char *argv[]) {
     seL4_Send(endpoint, seL4_MessageInfo_new(0, 0, 0, 1));
     seL4_SetMR(0, BUF_VADDR);
     seL4_Send(endpoint, seL4_MessageInfo_new(0, 0, 0, 1));
-    
+
     /* start single buffer producer consumer */
     volatile long *buf1 = (long *) buf1_frame;
     volatile long *buf2 = (long *) buf2_frame;
diff --git a/tutorials/threads/threads.md b/tutorials/threads/threads.md
index 3853d7ef..01235682 100644
--- a/tutorials/threads/threads.md
+++ b/tutorials/threads/threads.md
@@ -10,24 +10,54 @@
 /*- set progname = "threads" -*/
 
 # Threads
-
 This is a tutorial for using threads on seL4.
 
-## Prerequisites
-
-1. [Set up your machine](https://docs.sel4.systems/HostDependencies).
-1. [Capabilities tutorial](https://docs.sel4.systems/Tutorials/capabilities)
-1. [Mapping tutorial](https://docs.sel4.systems/Tutorials/mapping)
-
-## Outcomes
-
-1. Know the jargon TCB.
+In this tutorial, you will:
+1. Learn the jargon TCB.
 2. Learn how to start a thread in the same address space.
-3. Understand how to read and update TCB register state.
+3. Learn how to read and update TCB register state.
 4. Learn how to suspend and resume a thread.
 5. Understand thread priorities and their interaction with the seL4 scheduler.
 6. Gain a basic understanding of exceptions and debug fault handlers.
 
+## Prerequisites
+
+1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up)
+2. [Capabilities tutorial](https://docs.sel4.systems/Tutorials/capabilities)
+3. [Mapping tutorial](https://docs.sel4.systems/Tutorials/mapping)
+
+## CapDL Loader
+
+Previous tutorials have taken place in the root task where the starting CSpace layout is set by the
+seL4 boot protocol. This tutorial uses the *capDL loader*, a root task which allocates statically
+ configured objects and capabilities.
+
+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.
+
+More information about CapDL projects can be found [here](https://docs.sel4.systems/CapDL.html).
+
+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.
+
+## Initialising
+
+/*? macros.tutorial_init("threads") ?*/
+
+<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("threads") ?*/
+
+Answers are also available in drop down menus under each section.
+</details>
+
 ## Background
 
 ### Thread Control Blocks
@@ -200,14 +230,19 @@ int main(int c, char* arbv[]) {
     ZF_LOGF_IF(result, "Failed to retype thread: %d", result);
     seL4_DebugDumpScheduler();
 /*-- endfilter -*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("threads-retype", TaskContentType.COMPLETED, subtask='retype', completion="Failed to configure thread") -*/
     seL4_Error result = seL4_Untyped_Retype(tcb_untyped, seL4_TCBObject, seL4_TCBBits, root_cnode, 0, 0, tcb_cap_slot, 1);
     ZF_LOGF_IF(result, "Failed to retype thread: %d", result);
     seL4_DebugDumpScheduler();
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
+</details>
 
 Once the TCB has been created it will show up in the `seL4_DebugDumpScheduler()` output as
 `child of: 'tcb_threads'`. Throughout the tutorial you can use this syscall to debug some of the TCB attributes
@@ -232,7 +267,10 @@ as the current thread. Use the IPC buffer we have provided, but don't set a faul
     ZF_LOGF_IF(result, "Failed to configure thread: %d", result);
 /*-- endfilter -*/
 ```
-/*- filter ExcludeDocs() -*/
+
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
 
 ```c
 /*-- filter TaskContent("threads-configure", TaskContentType.COMPLETED, subtask='configure', completion="child of: 'tcb_threads'") -*/
@@ -240,7 +278,8 @@ as the current thread. Use the IPC buffer we have provided, but don't set a faul
     ZF_LOGF_IF(result, "Failed to configure thread: %d", result);
 /*-- endfilter -*/
 ```
-/*- endfilter -*/
+
+</details>
 
 
 You should now be getting the following error:
@@ -271,7 +310,9 @@ TCB capability, which has an MCP of 254.
     seL4_DebugDumpScheduler();
 /*-- endfilter -*/
 ```
-/*- filter ExcludeDocs() -*/
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
 
 ```c
 /*-- filter TaskContent("threads-priority", TaskContentType.COMPLETED, subtask='priority') -*/
@@ -280,8 +321,7 @@ TCB capability, which has an MCP of 254.
     seL4_DebugDumpScheduler();
 /*-- endfilter -*/
 ```
-
-/*- endfilter -*/
+</details>
 
 Fixing up the `seL4_TCB_SetPriority` call should allow you to see that the thread's priority is now
 set to the same as the main thread in the next `seL4_DebugDumpScheduler()` call.
@@ -330,7 +370,10 @@ you have at least set the instruction pointer (IP) correctly.
 
 /*-- endfilter -*/
 ```
-/*-- filter ExcludeDocs() -*/
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
 ```c
 /*-- filter TaskContent("threads-context", TaskContentType.COMPLETED, subtask='context', completion='Failed to start new thread') -*/
     seL4_UserContext regs = {0};
@@ -345,7 +388,7 @@ you have at least set the instruction pointer (IP) correctly.
     seL4_DebugDumpScheduler();
 /*-- endfilter -*/
 ```
-/*-- endfilter -*/
+</details>
 
 On success, you will see the following output:
 ```
@@ -369,7 +412,10 @@ Finally you are ready to start the thread, which makes the TCB runnable and elig
     ZF_LOGF_IFERR(error, "Failed to start new thread.\n");
 /*-- endfilter -*/
 ```
-/*- filter ExcludeDocs() -*/
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
 ```c
 /*-- filter TaskContent("threads-resume", TaskContentType.COMPLETED, subtask='resume', completion='Hello2: arg1 0, arg2 0, arg3 0') -*/
     // resume the new thread
@@ -377,7 +423,8 @@ Finally you are ready to start the thread, which makes the TCB runnable and elig
     ZF_LOGF_IFERR(error, "Failed to start new thread.\n");
 /*-- endfilter -*/
 ```
-/*-- endfilter -*/
+</details>
+
 
 If everything has been configured correctly, resuming the thread should result in the string
 `Hello2: arg1 0, arg2 0, arg3 0` followed by a fault.
@@ -391,9 +438,30 @@ for your target architecture.
 **Exercise** update the values written with `seL4_TCB_WriteRegisters` to pass the values 1, 2, 3 as arg1,
 arg2, and arg3 respectively.
 
+```c
+    seL4_UserContext regs = {0};
+    int error = seL4_TCB_ReadRegisters(tcb_cap_slot, 0, 0, sizeof(regs)/sizeof(seL4_Word), &regs);
+    ZF_LOGF_IFERR(error, "Failed to read the new thread's register set.\n");
+
+     // use valid instruction pointer
+    sel4utils_set_instruction_pointer(&regs, (seL4_Word) new_thread);
+    // use valid stack pointer
+    sel4utils_set_stack_pointer(&regs, tcb_stack_top);
+    // fix parameters to this invocation
+    error = seL4_TCB_WriteRegisters(tcb_cap_slot, 0, 0, sizeof(regs)/sizeof(seL4_Word), &regs);
+
+    ZF_LOGF_IFERR(error, "Failed to write the new thread's register set.\n"
+                  "\tDid you write the correct number of registers? See arg4.\n");
+    seL4_DebugDumpScheduler();
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
 ```c
 /*-- filter TaskContent("threads-context-2", TaskContentType.ALL, subtask='context', completion='Hello2: arg1 0x1, arg2 0x2, arg3 0x3') -*/
-    UNUSED seL4_UserContext regs = {0};
+
+UNUSED seL4_UserContext regs = {0};
     int error = seL4_TCB_ReadRegisters(tcb_cap_slot, 0, 0, sizeof(regs)/sizeof(seL4_Word), &regs);
     ZF_LOGF_IFERR(error, "Failed to write the new thread's register set.\n"
                   "\tDid you write the correct number of registers? See arg4.\n");
@@ -406,6 +474,9 @@ arg2, and arg3 respectively.
                   "\tDid you write the correct number of registers? See arg4.\n");
 /*-- endfilter -*/
 ```
+
+</details>
+
 ### Resolving a fault
 
 At this point, you have created and configured a new thread, and given it initial arguments.
@@ -457,40 +528,30 @@ You should be able to see that `arg2` is being dereferenced, but does not point
 
 **Exercise** pass a valid arg2, by passing the address of a global variable.
 
-Next, another fault will occur as the new thread expects `arg1` to be a pointer to a function.
 
-**Exercise** Pass the address of a function which outputs the argument which is passed to it, as `arg2`.
-
-Now you should have a new thread, which immediately calls the function passed in `arg2`.
-
-### Further exercises
-
-That's all for the detailed content of this tutorial. Below we list other ideas for exercises you can try,
-to become more familiar with TCBs and threading in seL4.
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+Create a new variable
+```c
+    int data = 42;
+```
 
-- Using different TCB invocations to change the new thread's attributes or objects
-- Investigate how setting different priorities affects when the threads are scheduled to run
-- Implementing synchronisation primitives using global memory.
-- Trying to repeat this tutorial in the root task where there are more resources available to
-  create more thread objects.
-- Another tutorial...
+And fix `sel4utils_arch_init_local_context`
 
-/*? macros.help_block() ?*/
+```c
+    sel4utils_arch_init_local_context((void*)new_thread,
+                                  (void *)1, (void *)&data, (void *)3,
+                                  (void *)tcb_stack_top, &regs);
+```
+</details>
 
-/*- filter ExcludeDocs() -*/
+Next, another fault will occur as the new thread expects `arg1` to be a pointer to a function.
 
-```c
-/*-- filter TaskContent("threads-fault", TaskContentType.COMPLETED, subtask='fault') -*/
-int data = 42;
+**Exercise** Pass the address of a function which outputs the argument which is passed to it, as `arg2`.
 
-int new_thread(void *arg1, void *arg2, void *arg3) {
-    printf("Hello2: arg1 %p, arg2 %p, arg3 %p\n", arg1, arg2, arg3);
-    void (*func)(int) = arg1;
-    func(*(int *)arg2);
-    while(1);
-}
-/*-- endfilter -*/
-```
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+Create a new function
 
 ```c
 /*-- filter TaskContent("threads-fault", TaskContentType.COMPLETED, subtask='func2', completion='Hello 3 42') -*/
@@ -500,6 +561,8 @@ int call_once(int arg) {
 /*-- endfilter -*/
 ```
 
+and fix `sel4utils_arch_init_local_context`
+
 ```c
 /*-- filter TaskContent("threads-fault", TaskContentType.COMPLETED, subtask='context') -*/
     UNUSED seL4_UserContext regs = {0};
@@ -517,6 +580,37 @@ int call_once(int arg) {
                   "\tDid you write the correct number of registers? See arg4.\n");
 /*- endfilter -*/
 ```
+</details>
+
+Now you should have a new thread, which immediately calls the function passed in `arg2`.
+
+### Further exercises
+
+That's all for the detailed content of this tutorial. Below we list other ideas for exercises you can try,
+to become more familiar with TCBs and threading in seL4.
+
+- Using different TCB invocations to change the new thread's attributes or objects
+- Investigate how setting different priorities affects when the threads are scheduled to run
+- Implementing synchronisation primitives using global memory.
+- Trying to repeat this tutorial in the root task where there are more resources available to
+  create more thread objects.
+
+
+
+/*- filter ExcludeDocs() -*/
+
+```c
+/*-- filter TaskContent("threads-fault", TaskContentType.COMPLETED, subtask='fault') -*/
+int data = 42;
+
+int new_thread(void *arg1, void *arg2, void *arg3) {
+    printf("Hello2: arg1 %p, arg2 %p, arg3 %p\n", arg1, arg2, arg3);
+    void (*func)(int) = arg1;
+    func(*(int *)arg2);
+    while(1);
+}
+/*-- endfilter -*/
+```
 
 ```c
 /*-- filter ELF(progname) --*/
diff --git a/tutorials/untyped/untyped.md b/tutorials/untyped/untyped.md
index 80a69607..efdf34af 100644
--- a/tutorials/untyped/untyped.md
+++ b/tutorials/untyped/untyped.md
@@ -10,18 +10,31 @@
 
 This tutorial provides an introduction to physical memory management on seL4.
 
+It covers:
+1. The jargon *untyped*, *device untyped*, and *bit size*.
+2. How to create objects from untyped memory in seL4.
+3. How to reclaim objects.
+
 ## Prerequisites
 
-1. [Set up your machine](https://docs.sel4.systems/HostDependencies).
-1. [Capabilities tutorial](https://docs.sel4.systems/Tutorials/capabilities)
+1. [Set up your machine](https://docs.sel4.systems/Tutorials/setting-up)
+2. [Capabilities tutorial](https://docs.sel4.systems/Tutorials/capabilities)
 
-## Outcomes
 
-By the end of this tutorial, you should be familiar with:
+## Initialising
+
+/*? macros.tutorial_init("untyped") ?*/
+
+<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("untyped") ?*/
+
+Answers are also available in drop down menus under each section.
+</details>
 
-1. The jargon *untyped*, *device untyped*, and *bit size*.
-2. Know how to create objects from untyped memory in seL4.
-3. Know how to reclaim objects.
 
 ## Background
 
@@ -223,7 +236,13 @@ This error happens because we are trying to create an untyped of size 0.
         }
     }
 /*-- endfilter -*/
-/*-- filter ExcludeDocs() -*/
+
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("untyped-next", TaskContentType.COMPLETED, subtask='setup', completion='Failed to set priority') -*/
     // list of general seL4 objects
     seL4_Word objects[] = {seL4_TCBObject, seL4_EndpointObject, seL4_NotificationObject};
@@ -244,9 +263,11 @@ This error happens because we are trying to create an untyped of size 0.
         }
     }
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
 
+</details>
+
+
 On success, the tutorial will progress further, printing "Failed to set priority"
 
 ### Create a TCB Object
@@ -267,7 +288,8 @@ The priority check is failing as `child_tcb` is an empty CSlot.
 /*-- endfilter -*/
 ```
 
-/*-- filter ExcludeDocs() -*/
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
 
 ```c
 /*-- filter TaskContent("untyped-tcb", TaskContentType.COMPLETED, subtask='tcb', completion='Endpoint cap is null cap') -*/
@@ -280,8 +302,8 @@ The priority check is failing as `child_tcb` is an empty CSlot.
     ZF_LOGF_IF(error != seL4_NoError, "Failed to set priority");
 /*-- endfilter -*/
 ```
+</details>
 
-/*-- endfilter -*/
 
 On success, the tutorial will progress further, printing "Endpoint cap is null cap".
 
@@ -301,7 +323,13 @@ The error you see now is caused be an invalid endpoint capability.
     uint32_t cap_id = seL4_DebugCapIdentify(child_ep);
     ZF_LOGF_IF(cap_id == 0, "Endpoint cap is null cap");
 /*-- endfilter -*/
-/*-- filter ExcludeDocs() -*/
+
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("untyped-ep", TaskContentType.COMPLETED, subtask='ep', completion='Failed to bind notification.') -*/
     // use the slot after child_tcb for the new endpoint cap:
     seL4_CPtr child_ep = child_tcb + 1;
@@ -311,10 +339,11 @@ The error you see now is caused be an invalid endpoint capability.
     uint32_t cap_id = seL4_DebugCapIdentify(child_ep);
     ZF_LOGF_IF(cap_id == 0, "Endpoint cap is null cap");
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
 
-On success, 'Failed to bind notification' should be output.
+</details>
+
+On success, the output will be "Failed to bind notification."
 
 ### Create a notification object
 
@@ -334,7 +363,8 @@ The next part of the tutorial attempts to use a notification object that does no
 /*-- endfilter -*/
 ```
 
-/*-- filter ExcludeDocs() -*/
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
 
 ```c
 /*-- filter TaskContent("untyped-ntfn", TaskContentType.COMPLETED, subtask='ntfn', completion='Failed to create endpoints..') -*/
@@ -348,7 +378,11 @@ The next part of the tutorial attempts to use a notification object that does no
 /*-- endfilter -*/
 ```
 
-/*-- endfilter -*/
+</details>
+
+On success, the output will be "Failed to create endpoints."
+
+
 
 ### Delete the objects
 
@@ -369,7 +403,12 @@ entire untyped object. However, this fails, because the untyped is already compl
 
     printf("Success\n");
 /*-- endfilter -*/
-/*-- filter ExcludeDocs() -*/
+```
+
+<details markdown='1'>
+<summary><em>Quick solution</em></summary>
+
+```c
 /*-- filter TaskContent("untyped-revoke", TaskContentType.COMPLETED, subtask='revoke', completion='Success') -*/
     error = seL4_CNode_Revoke(seL4_CapInitThreadCNode, child_untyped, seL4_WordBits);
     assert(error == seL4_NoError);
@@ -382,10 +421,11 @@ entire untyped object. However, this fails, because the untyped is already compl
 
     printf("Success\n");
 /*-- endfilter -*/
-/*-- endfilter -*/
 ```
 
-Once the tutorial is completed successfully, you should see the message "Success".
+</details>
+
+Once the tutorial is completed successfully, you should see the message "Success."
 
 ### Further exercises
 
@@ -395,8 +435,6 @@ to become more familiar with untyped objects and memory allocation in seL4.
 * Allocate objects at specific physical addresses.
 * Create a simple object allocator for allocating seL4 objects.
 
-/*? macros.help_block() ?*/
-
 /*-- filter ExcludeDocs() -*/
 
 ```c