update README

- remove obsolete options and settings - spell check - update github org URLs - update descriptions to current seL4 CI - update CLI instructions - markdown lint Signed-off-by: Gerwin Klein <[email protected]>
seL4 · May 13, 2024 · 6b140bc · 6b140bc
1 parent 071ef59
commit 6b140bc
Showing 1 changed file with 33 additions and 32 deletions.
diff --git a/README.md b/README.md
@@ -1,10 +1,11 @@
 <!--
+     Copyright 2024, Proofcraft Pty Ltd
      Copyright 2020, Data61, CSIRO
 
      SPDX-License-Identifier: CC-BY-SA-4.0
 -->
 
-# Dockerfiles for seL4, CAmkES, and L4v dependencies
+# Docker containers for seL4, CAmkES, and L4v dependencies
 
 ## Requirements
 
@@ -13,11 +14,11 @@
 
 It is recommended you add yourself to the docker group, so you can run docker commands without using sudo.
 
-
 ## Quick start
-To get a running build environment for sel4 and camkes, run:
 
-    git clone https://github.com/SEL4PROJ/seL4-CAmkES-L4v-dockerfiles.git
+To get a running build environment for seL4 and CAmkES, run:
+
+    git clone https://github.com/seL4/seL4-CAmkES-L4v-dockerfiles.git
     cd seL4-CAmkES-L4v-dockerfiles
     make user
 
@@ -27,15 +28,17 @@ Or to map a particular directory to the /host dir in the container:
 
 
 ## What is this?
-This repository contains dockerfiles which map out the dependencies for seL4, CAmkES, and L4v. It also contains some infrastructure to allow people to use the containers in a useful way.
 
-These dockerfiles are used as the basis for regression testing in the Trustworthy Systems group, and hence should represent a well tested and up to date environment
+This repository contains docker files which map out the dependencies for seL4, CAmkES, and L4v. It also contains some infrastructure to allow people to use the containers in a useful way.
+
+These docker files are used as the basis for regression testing in the seL4 Foundation, and hence should represent a well tested and up to date environment
 
 
 ## To run
-Get the repository of Dockerfiles by cloning them from GitHub:
 
-    git clone https://github.com/SEL4PROJ/seL4-CAmkES-L4v-dockerfiles.git
+Get the repository of docker files by cloning them from GitHub:
+
+    git clone https://github.com/seL4/seL4-CAmkES-L4v-dockerfiles.git
     cd seL4-CAmkES-L4v-dockerfiles
 
 To get an environment within the container, run:
@@ -81,6 +84,7 @@ to start the container interactively in your current directory, or:
 to execute commands in the container in your current directory.
 
 ### Example of compiling seL4 test
+
 Start by creating a new workspace on your machine:
 
     mkdir ~/sel4test
@@ -119,70 +123,67 @@ Compile and simulate seL4 test for x86-64:
 
     All is well in the universe
 
-
 ## Adding dependencies
-The images and dockerfiles for seL4/CAmkES/L4v only specify enough dependencies to pass the tests in the \*tests.dockerfile. The `extras.dockerfile` acts as a shim between the DockerHub images and the `user.dockerfile`.
 
-Adding dependencies into the `extras.dockerfile` will build them the next time you run `make user`, and then be cached from then on.
+The images and docker files for seL4/CAmkES/L4v only specify enough dependencies to pass the tests in the \*tests.docker file. The `extras.dockerfile` acts as a shim between the DockerHub images and the `user.dockerfile`.
 
+Adding dependencies into the `extras.dockerfile` will build them the next time you run `make user`, and then be cached from then on.
 
-## To build the local dockerfiles
+## To build the local Docker files
 
-To build the Dockerfiles locally, you will need to use the included `build.sh` script. It has a help menu:
+To build the Docker files locally, you will need to use the included `build.sh` script. It has a help menu:
 
     ./build.sh -h
-        build.sh [-r] -b [sel4|camkes|l4v] -s [binary_decomp|cakeml|camkes_vis|riscv|rust|sysinit|] -s ... -e MAKE_CACHES=no -e ...
+        build.sh [-r] -b [sel4|camkes|l4v] -s [binary_decomp|cakeml|camkes_vis|riscv|rust|sysinit] -s ... -e MAKE_CACHES=no -e ...
 
          -r     Rebuild docker images (don't use the docker cache)
          -v     Verbose mode
          -s     Strict mode
          -e     Build arguments (NAME=VALUE) to docker build. Use a -e for each build arg.
          -p     Pull base image first. Rather than build the base image,
                 get it from the web first
-
-        Sneaky hints:
-         - To build 'prebuilt' images, you can run:
-               build.sh -b [riscv|cakeml]
-           but it will take a while!
-         - You can actually run this with '-b sel4-rust', or any other existing image,
-           but it will ruin the sorting of the name.
+         -a     Supply x86_64 for building Intel images, and arm64 for Arm images.
+                Defaults to x86_64 on x86-based hosts and arm64 on ARM64 hosts.
 
 ### Example builds
 
 To build the seL4 image, run:
 
-`./build.sh -b sel4`
+    ./build.sh -b sel4
 
 Note that the `-b` flag stands for the `base image`. There are 3 base images: `sel4`, `camkes`, and `l4v`. Each base image includes the previous one, i.e.: the `camkes` image has everything the `sel4` image has, plus the camkes dependencies.
 
 To add additional software to the image, you can use the `-s` flag, to add `software`. For example:
 
-`./build.sh -b sel4 -s riscv  # This adds the RISCV compilers`
+    ./build.sh -b camkes -s cakeml  # This adds the CakeML compiler
 
-`./build.sh -b sel4 -s riscv -s rust  # This adds the RISCV compilers and a rust compiler`
+    ./build.sh -b sel4 -s cakeml -s rust  # This adds the CakeML compiler and Rust compiler
 
 You can also pass configuration variables through to docker (in docker terms, these are `BUILD_ARGS`) by using the `-e` flag. For example, you can turn off priming the build caches:
 
-`./build.sh -b sel4 -e MAKE_CACHES=no`
+    ./build.sh -b sel4 -e MAKE_CACHES=no
 
 To speed things up, you can ask to pull the base image from DockerHub first with the `-p` flag:
 
-`./build.sh -p -b sel4 -s riscv  # This adds the RISCV compilers`
-
-
+    # This adds the CakeML compiler and pulls camkes from DockerHub
+    ./build.sh -p -b camkes -s cakeml
 
 ## Security
+
 Running Docker on your machine has its own security risks which you should be aware of. Be sure to read the Docker documentation.
 
 Of particular note in this case, your UID and GID are being baked into an image. Any other user on the host who is part of the docker group could spawn a separate container of this image, and hence have read and write access to your files. Of course, if they are part of the docker group, they could do this anyway, but it just makes it a bit easier.
 
 Use at your own risk.
 
-
 ## Released images on DockerHub
 
-The Trustworthy Systems group pushes "known working" images to DockerHub under the `trustworthysystems/` DockerHub organisation. Images with the `:latest` tag are the ones currently in use in the Trustworthy Systems regression system, and so are considered to be "known working". Furthermore, each time an image is pushed out, it is tagged with a YYYY_MM_DD formatted date.
+The seL4 CI pushes "known working" images to DockerHub under the [`trustworthysystems/` DockerHub organisation][1]. Images with the `:latest` tag are the ones currently in use in the seL4 CI system, and so are considered to be "known working". Furthermore, each time an image is pushed out, it is tagged with a `YYYY_MM_DD` formatted date.
+
+To ensure (fairly) reproducible builds of docker images, the images are built using Debian Snapshot (an apt repository that can be pinned to a date in time). When changes are made to the scripts or Docker files in this repo, they are built against a "known working" date of Debian Snapshot - in other words, a date in which we were able to build all the Docker images, and they passed all of our tests. This avoids issues where something in Debian Testing or Unstable has changed and causes apt conflicts, or a newer version breaks the seL4 build process.
 
-To ensure (fairly) reproducible builds of docker images, the images are built using Debian Snapshot (an apt repository that can be pinned to a date in time). When changes are made to the scripts or Dockerfiles in this repo, they are built against a "known working" date of Debian Snapshot - in other words, a date in which we were able to build all the Docker images, and they passed all of our tests. This avoids issues where something in Debian Testing or Unstable has changed and causes apt conflicts, or a newer version breaks the seL4 build process.
+<!-- Currently not the case:
+Internally, the seL4 CI system will, once a week, attempt to build the docker images using regular apt (not using Snapshot), and if successful, will update the "known working" date. This means on the next build of the docker images that gets pushed out will be using this bumped Snapshot date. Typically, the further in time we get from a Debian release, the more packages we need to fetch from Testing or Unstable, and as such, the less likely this automatic bumping is to work, due to above mentioned issues. With some human intervention, it can usually be fixed up fairly easily. However, even without intervention, the "known working" images will continue to function and build.
+-->
 
-Internally, the Trustworthy Systems regression system will, once a week, attempt to build the docker images using regular apt (not using Snapshot), and if successful, will update the "known working" date. This means on the next build of the docker images that gets pushed out will be using this bumped Snapshot date. Typically, the further in time we get from a Debian release, the more packages we need to fetch from Testing or Unstable, and as such, the less likely this automatic bumping is to work, due to above mentioned issues. With some human intervention, it can usually be fixed up fairly easily. However, even without intervention, the "known working" images will continue to function and build.
+[1]: https://hub.docker.com/u/trustworthysystems