adding prerequisites back into tutes

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

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

@@ -19,6 +19,10 @@ 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)
+
 ## Initialising
 
 /*? macros.tutorial_init("camkes-vm-crossvm") ?*/

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

@@ -3,7 +3,7 @@
 
   Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
-  SPDX-License-Identifier: BSD-2-Clause
+  SPDX-License-Identifier: BSD-2-Clause - yay
 -->
 
 /*? 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']) ?*/
@@ -17,6 +17,10 @@ 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.
 
+## 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)
+
 ## CapDL Loader
 
 This tutorial uses the *capDL loader*, a root task which allocates statically

tutorials/capabilities/capabilities.md

@@ -3,7 +3,7 @@
 
   Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
-  SPDX-License-Identifier: BSD-2-Clause
+  SPDX-License-Identifier: BSD-2-Clause - yay
 -->
 
 /*? declare_task_ordering(['cnode-start', 'cnode-size', 'cnode-copy', 'cnode-delete', 'cnode-invoke']) ?*/
@@ -15,6 +15,11 @@ You will learn:
 2. How to invoke a capability.
 3. How to delete and copy CSlots.
 
+## Prerequisites
+
+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") ?*/

tutorials/dynamic-1/dynamic-1.md

@@ -3,7 +3,7 @@
 
   Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
-  SPDX-License-Identifier: BSD-2-Clause
+  SPDX-License-Identifier: BSD-2-Clause - yay
 -->
 
 /*? declare_task_ordering(
@@ -54,6 +54,11 @@ Outcomes:
         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
 

tutorials/dynamic-2/dynamic-2.md

@@ -62,6 +62,12 @@ Learning outcomes:
         multiple indexes concatenated into one. Understanding them well
         however, is important to understanding how capabilities work.
 
+## Prerequisites
+
+1. [Set up your machine](https://docs.sel4.systems/tutorials/setting-up)
+2. [Dynamic libraries: initialisation & threading](https://docs.sel4.systems/tutorials/dynamic-1)
+
+
 ## Initialising
 
 /*? macros.tutorial_init("dynamic-2") ?*/

tutorials/dynamic-3/dynamic-3.md

@@ -47,6 +47,10 @@ Learning outcomes:
 - 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. [Dynamic libraries: IPC](https://docs.sel4.systems/tutorials/dynamic-2)
 
 ## Initialising
 

tutorials/dynamic-4/dynamic-4.md

@@ -3,7 +3,7 @@
 
   Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
-  SPDX-License-Identifier: BSD-2-Clause
+  SPDX-License-Identifier: BSD-2-Clause - yay
 -->
 
 /*? declare_task_ordering(
@@ -30,6 +30,11 @@ Learning outcomes:
 - 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. [Dynamic libraries: processes & elf loading](https://docs.sel4.systems/tutorials/dynamic-3)
+
 ## Initialising
 
 /*? macros.tutorial_init("dynamic-4") ?*/

tutorials/fault-handlers/fault-handlers.md

@@ -3,7 +3,7 @@
 
   Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
-  SPDX-License-Identifier: BSD-2-Clause
+  SPDX-License-Identifier: BSD-2-Clause - yay
 -->
 
 # Fault handling
@@ -22,6 +22,12 @@ You will learn:
 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/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") ?*/

tutorials/hello-camkes-0/hello-camkes-0.md

@@ -14,10 +14,16 @@ This tutorial is an introduction to CAmkES. This will involve introducing the CA
 static CAmkES application and describing its components.
 
 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.
+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.
+
+## Prerequisites
+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.
 
 ## Background
 

tutorials/hello-camkes-1/hello-camkes-1.md

@@ -3,7 +3,7 @@
 
   Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
-  SPDX-License-Identifier: BSD-2-Clause
+  SPDX-License-Identifier: BSD-2-Clause - yay
 -->
 
 # CAmkES Tutorial: Introduction to CAmkES
@@ -19,6 +19,10 @@ 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.
 
+## 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") ?*/
@@ -141,6 +145,8 @@ the second one was named `a2`? Then in order to call on that second
 
 ```
 /*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="define",completion="Booting all finished, dropped to user space") -*/
+assembly {
+    composition {
          component EmptyComponent empty;
          // TODO define an Echo and a Client component
 /*-- endfilter -*/
@@ -151,6 +157,9 @@ the second one was named `a2`? Then in order to call on that second
 
 ```
 /*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="define") -*/
+assembly {
+    composition {
+         component EmptyComponent empty;
          component Client client;
          component Echo echo;
 /*-- endfilter -*/
@@ -182,16 +191,20 @@ the second one was named `a2`? Then in order to call on that second
 
 ### Define an interface
 
-**Exercise** Define the interface for hello in `interfaces/HelloSimple.idl4`.
+**Exercise** Define the interface for hello in `interfaces/HelloSimple.idl4`. 
 
 ```c
 /* Simple RPC interface */
+procedure HelloSimple {
 /*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="interface") -*/
     /* TODO define RPC functions */
     /* hint 1: define at least one function that takes a string as input parameter. call it say_hello. no return value
      * hint 2: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application
      */
 /*-- endfilter -*/
+/*-- filter ExcludeDocs() -*/
+};
+/*-- endfilter -*/
 ```
 
 <details markdown='1'>
@@ -204,10 +217,21 @@ the second one was named `a2`? Then in order to call on that second
 ```
 </details>
 
-### Implement an RPC function
+### Implement a RPC function
 **Exercise** Implement the RPC hello function.
 
 ```c
+/*- filter File("components/Echo/src/echo.c") --*/
+/*-- filter ExcludeDocs() -*/
+/*
+ * CAmkES tutorial part 1: components with RPC. Server part.
+ */
+#include <stdio.h>
+
+/* generated header for our component */
+#include <camkes.h>
+/*-- endfilter -*/
+
 /*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="rpc") -*/
 /* Implement the RPC function. */
 /* hint 1: the name of the function to implement is a composition of an interface name and a function name:
@@ -220,6 +244,7 @@ the second one was named `a2`? Then in order to call on that second
  * hint 7: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application
  */
 /*-- endfilter -*/
+/*-- endfilter -*/
 ```
 
 
@@ -235,11 +260,28 @@ void hello_say_hello(const char *str) {
 ```
 </details>
 
-### Invoke an RPC function
+### Invoke a RPC function
 
 **Exercise** Invoke the RPC function in `components/Client/src/client.c`.
 
 ```c
+/*- filter File("components/Client/src/client.c") --*/
+/*-- filter ExcludeDocs() -*/
+/*
+ * CAmkES tutorial part 1: components with RPC. Client part.
+ */
+
+#include <stdio.h>
+
+/* generated header for our component */
+#include <camkes.h>
+
+/* run the control thread */
+int run(void) {
+    printf("Starting the client\n");
+    printf("-------------------\n");
+/*-- endfilter -*/
+
 /*-- 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:
@@ -250,6 +292,7 @@ void hello_say_hello(const char *str) {
      * hint 5: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application
      */
 /*-- endfilter -*/
+/*-- endfilter -*/
 ```
 
 <details markdown='1'>
@@ -261,6 +304,9 @@ void hello_say_hello(const char *str) {
     hello_say_hello(shello);
 /*-- endfilter -*/
 
+    printf("After the client\n");
+    return 0;
+}
 ```
 </details>
 
@@ -297,52 +343,13 @@ component Echo {
     provides HelloSimple hello;
 }
 
-assembly {
-    composition {
 /*? include_task_type_append([("hello", 'define')]) ?*/
 /*? include_task_type_append([("hello", 'connect')]) ?*/
-    }
-}
-/*-- endfilter -*/
-```
 
-```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>
-/*? include_task_type_append([("hello", 'rpc')]) ?*/
-/*-- endfilter -*/
-```
-
-```c
-/*- filter File("components/Client/src/client.c") --*/
-/*
- * CAmkES tutorial part 1: components with RPC. Client part.
- */
-
-#include <stdio.h>
-
-/* generated header for our component */
-#include <camkes.h>
-
-/* run the control thread */
-int run(void) {
-    printf("Starting the client\n");
-    printf("-------------------\n");
-
-/*? include_task_type_append([("hello", 'hello')]) ?*/
-
-    printf("After the client\n");
-    return 0;
+    }
 }
 /*-- endfilter -*/
 ```
-
 ```
 /*- filter File("interfaces/HelloSimple.idl4") --*/
 /* Simple RPC interface */

tutorials/hello-camkes-2/hello-camkes-2.md

@@ -15,6 +15,11 @@ Learn how to:
 - Represent and implement events in CAmkES.
 - Use Dataports.
 
+## 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

tutorials/hello-camkes-timer/hello-camkes-timer.md

@@ -24,6 +24,11 @@ The solutions to this tutorial primarily uses the method of manually defining
 hardware details. The solutions to the second part are also included, albeit
 commented out.
 
+## Prerequisites
+1. [Set up your machine](https://docs.sel4.systems/tutorials/setting-up)
+2. [CAmkES events tutorial](https://docs.sel4.systems/tutorials/hello-camkes-2)
+
+
 ## CapDL Loader
 
 This tutorial uses the *capDL loader*, a root task which allocates statically
@@ -294,7 +299,7 @@ After initialising the timer, we now need to start the timer. Do so by calling
 ```
 </details>
 
-### Implement an RPC interface
+### Implement a RPC interface
 Note that this task is to understand the existing code. You won't have
 to modify anything for this task.
 
@@ -669,7 +674,7 @@ timer_drv_t timer_drv;
 
 void irq_handle(void) {
     int error;
-
+    
 /*? include_task_type_append([("hello","part1-task4")]) ?*/
 
 /*? include_task_type_append([("hello","part1-task5")]) ?*/

tutorials/hello-world/hello-world.md

@@ -3,18 +3,21 @@
 
   Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
-  SPDX-License-Identifier: BSD-2-Clause
+  SPDX-License-Identifier: BSD-2-Clause - yay
 -->
 
 /*? declare_task_ordering(['hello-world', 'hello-world-mod']) ?*/
 # Hello, World!
 
 In this tutorial you will:
 
-- Run Hello, World! to ensure your setup is working correctly
-- Become familiar with the jargon *root task*
-- Build and simulate a seL4 project
-- Have a basic understanding of the role of the `CMakeLists.txt` file in applications
+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.

tutorials/interrupts/interrupts.md

@@ -11,11 +11,15 @@
 # Interrupts
 This tutorial covers seL4 interrupts.
 
-You will learn
-* the IRQControl capability's purpose.
-* How to obtain capabilities for specific interrupts.
-* How to handle interrupts and their relation with notification objects.
+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/tutorials/setting-up)
+2. [Notifications tutorial](https://docs.sel4.systems/tutorials/notifications)
 
 # Initialising
 

tutorials/ipc/ipc.md

@@ -11,12 +11,17 @@
 
 This tutorial is about interprocess communication (IPC), the microkernel mechanism for synchronous transmission of small amounts of data.
 
-You will learn
+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/tutorials/setting-up)
+2. [Capabilities tutorial](https://docs.sel4.systems/tutorials/capabilities)
+
 ## Initialising
 
 /*? macros.tutorial_init("ipc") ?*/

tutorials/mapping/mapping.md

@@ -12,6 +12,11 @@
 
 This tutorial provides an introduction to virtual memory management on seL4.
 
+## Prerequisites
+
+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("mapping") ?*/

tutorials/mcs/mcs.md

@@ -21,6 +21,20 @@ Learn:
 3. The jargon *passive server*.
 4. How to spawn round-robin and periodic threads.
 
+## Prerequisites
+
+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
 
 Then initialise the tutorial:

tutorials/notifications/notifications.md

@@ -3,7 +3,7 @@
 
   Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
-  SPDX-License-Identifier: BSD-2-Clause
+  SPDX-License-Identifier: BSD-2-Clause - yay
 -->
 
 /*? declare_task_ordering(['ntfn-start', 'ntfn-shmem', 'ntfn-signal', 'ntfn-badge']) ?*/
@@ -16,6 +16,13 @@ You will learn how to:
 2. Use notification objects for synchronisation between tasks.
 3. Use badges to differentiate notifications.
 
+## 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)
+4. [Threads tutorial](https://docs.sel4.systems/tutorials/threads)
+
 ## Initialising
 
 /*? macros.tutorial_init("notifications") ?*/

tutorials/threads/threads.md

@@ -3,7 +3,7 @@
 
   Copyright 2024, seL4 Project a Series of LF Projects, LLC.
 
-  SPDX-License-Identifier: BSD-2-Clause
+  SPDX-License-Identifier: BSD-2-Clause - yay
 -->
 
 /*? declare_task_ordering(['threads-start','threads-retype','threads-configure','threads-priority',
@@ -14,14 +14,20 @@
 # Threads
 This is a tutorial for using threads on seL4.
 
-In this tutorial, you will
+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

tutorials/untyped/untyped.md

@@ -12,11 +12,16 @@
 
 This tutorial provides an introduction to physical memory management on seL4.
 
-By the end of this tutorial, you should be familiar with:
-
+It covers:
 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.
+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/tutorials/setting-up)
+2. [Capabilities tutorial](https://docs.sel4.systems/tutorials/capabilities)
+
 
 ## Initialising