sel4test: make instructions linear

As #221 points out, copy/pasting the previous instructions linearly
without closely reading the text will lead to an error state (wrong
directory). Reorganise the code blocks so that they can be copy/pasted
and run step by step without running into errors. This also makes the
initial example more concrete.

Fixes #221

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Hardware/index.md

@@ -150,7 +150,7 @@ seL4 supports PC99-style Intel Architecture Platforms.
 Running seL4 in a simulator is a quick way to test it out and iteratively
 develop software. Note that feature support is then limited by the simulator.
 See the QEMU [Arm](qemu-arm-virt.html) and [RISCV](qemu-riscv-virt.html) targets
-and the [simulation instructions for sel4test](../projects/sel4test/#running-it)
+and the [simulation instructions for sel4test](../projects/sel4test/)
 for x86 for how to run seL4 using QEMU. Some hardware platforms support the
 `SIMULATION=1` option --- this will be marked on the respective platform page
 and will generally be good enough to run most of the seL4 test suite, but QEMU

projects/sel4test/index.md

@@ -63,16 +63,26 @@ which ones these are and their corresponding CMake configuration arguments, see
 the [Supported Platforms](../../Hardware) page.
 
 To start a build with a specific configuration we can create a new subdirectory
-from the project root and initialise it with `init-build`:
+from the project root and initialise it with `init-build`. In the example below
+we are using `ia32` as the platform, building in release mode, and with
+simulation support switched on.
 
 ```bash
 # create build directory
 mkdir build
 cd build
 # configure build directory
+../init-build.sh -DPLATFORM=ia32 -DRELEASE=TRUE -DSIMULATION=TRUE
+```
+
+The general more form of the last command is
+
+```sh
 ../init-build.sh -DPLATFORM=<platform-name> -DRELEASE=[TRUE|FALSE] -DSIMULATION=[TRUE|FALSE]
 ```
 
+See below for the full list of [available options](#configuration-options).
+
 This configures your build directory with the necessary CMake configuration for
 your chosen platform.
 
@@ -102,28 +112,23 @@ ninja
 
 ### IA32 Example
 
-We will now build seL4test for IA32, to run on the QEMU simulator.
+If you have followed the example instructions above, and `ninja` has completed
+successfully, the build will have produced boot images in the `images/`
+directory and a `simulate` script. It was produced, because we passed
+`-DSIMULATION=TRUE` to CMake. The option is available for hardware platforms
+that are marked as "Simulation target: yes" on their platform info page (e.g.
+for [IA32](../../Hardware/IA32.md)).
 
-Passing `-DSIMULATION=TRUE` to CMake produces a script to simulate our release
+Executing the `simulate` script will run QEMU and point it towards the image we
-IA32 build. The following commands will configure our CMake build:
-
-```bash
-mkdir ia32_build
-cd ia32_build
-../init-build.sh -DPLATFORM=ia32 -DRELEASE=TRUE -DSIMULATION=TRUE
-```
-
-Build it:
-
-```bash
-ninja
-```
-
-Executing the following commands will run QEMU and point it towards the image we
 just built:
 
 ```bash
 ./simulate
+```
+
+It should produce output such as the following
+
+```
 ...
 ELF-loading userland images from boot modules:
 size=0x1dd000 v_entry=0x806716f v_start=0x8048000 v_end=0x8225000 p_start=0x21f000 p_end=0x3fc000
@@ -143,8 +148,9 @@ Test BIND0003 passed
 ...
 ```
 
-To exit QEMU, press `Ctrl-a`, then `x`. The text `All is well in the
+To exit QEMU, press `Ctrl-a`, then `x`. In `DEBUG` configurations, there will be
-universe` indicates a successful build.
+error messages printed for negative tests. These are expected. The text `All is
+well in the universe` at the end indicates a successful run.
 
 ## Testing a Customised Kernel