seL4 Documentation site

These are the sources for the seL4 Documentation site located at https://docs.sel4.systems. It is for cooperatively developing and sharing documentation on seL4.

See CONTRIBUTING.md for information on how to contribute. TL;DR click edit on the page in GitHub, make your changes and then submit a pull request.

Ask on the mailing list or open an issue if something doesn’t make sense.

We’ve tried to make sure the hosted site is WCAG 2.0 AA compliant. Please let us know if we have missed something.

Building the site

Install

Ruby

We recommend using rbenv to install the correct Ruby version.

On Mac, using homebrew:

brew install ruby-build rbenv
# follow the instructions this command shows, and start a new shell afterwards
rbenv init
# in the docs directory (root of this repo):
rbenv install

On apt-based Linux distributions (e.g. Ubuntu, Debian):

apt install rbenv
# follow the instructions this command shows, and start a new shell afterwards
rbenv init
# in the docs directory (root of this repo):
rbenv install

After these, you should be able to forget about rbenv, the Makefile will now see the correct Ruby version.

Node/JS

The doc site needs node version 20 or later at build time. The default node and npm of recent distribution should work fine:

apt install node

or on Mac:

brew install node

The Makefile does the rest of the JS dependency installation.

Rust

For building the Rust tutorials we need cargo. The easiest way to get Rust installed is via https://rustup.rs. Follow the instructions there. A default install for your platform will work for the doc site.

You can test if cargo is available after the installation by trying

cargo --version

Python

The build is tested with Python 3.9. More recent versions are likely to work as well. After installing Python via e.g. homebrew or apt, you can install the Python build dependencies with:

pip3 install --user camkes-deps

Linters

If you are using the lint checks, they require tidy and liquid-linter. If you just want to build the site, you can skip these.

• HTML output checking using tidy: make check_html_output
• Liquid syntax checking using liquid-linter: make check_liquid_syntax

Build

To build and host locally:

make serve
#   Server address: http://127.0.0.1:4000/
#   Server running... press ctrl-c to stop.

Or using Docker (you need Docker installed and running for this):

make docker_serve

Makefile and JEKYLL_ENV=production version

Jekyll environment flags can be used to provide some content only in a production environment.

One way we use this is to show data generated by rules in the Makefile and saved in \_data/generated.yml. If you want to serve the site locally in production mode there are make rules for this. You will need to call the make rule to generate the \_data/generated.yml also.

How the site is set up

Our documentation is contained in a collection of Markdown files stored in this repository. We use Jekyll to generate a static html website that is then hosted on GitHub pages. Our continuous integration is configured to regenerate and update the live site whenever a pull request is merged. There is a timestamp in the source that indicates when it was last generated. Additionally, each page has a timestamp and revision hash from when it was last updated located in the footer based on the git history.

The markdown pages are rendered using Kramdown, a ruby-based markdown converter that is configured to interpret the markdown files (.md) as GitHub flavoured markdown.

Compliance, style and formatting checks

WCAG 2.0 AA conformance

There is a make rule to check conformance to all testable statements from the guidelines. make check_conformance. It requires the site to be hosted locally (using make serve) and a local server of Automated Accessibility Testing Tool (AATT).

make check_conformance will output a file named conformance_results.xml which is a junit test suite output file that will contain a test case for each generated html file of the site. A make rule make check_conformance_errors will grep for failing test cases and output the html page name. The idea here is to detect if any pages are failing and then manually using the AATT tool’s web interface to check what parts of the page violate the guidelines.