Setting up your machine to build seL4

This page describes how to set up your development host machine for building and running the seL4 kernel. There are additional steps if you are planning to use CAmkES or Rust on top of seL4. You do not need this step if you are using the Microkit, because it comes with pre-compiled seL4 binaries.

Get Google’s Repo tool

The primary way of obtaining and managing seL4 project sources is through Google’s repo tool. To start with, get repo by following the instructions in the section “Install” on the repo site.

See the [repo cheatsheet] page for a quick explanation of how we use repo.

Docker or native

To compile and use seL4 you can either:

• Recommended: follow the instructions here to use Docker for isolating the dependencies from your machine, or
• install the build dependencies below on your local OS

The following instructions describe how to set up the required dependencies on your local OS. This page assumes you are building in a Linux OS. We however encourage site contributions for build instructions in other OSes (e.g. macOS).

Ubuntu

These instructions are intended for Ubuntu LTS versions 20.04 and 22.04.

Base dependencies

The basic build package on Ubuntu is the build-essential package. To install run:

sudo apt-get update
sudo apt-get install build-essential

Additional base dependencies for building seL4 projects on Ubuntu include installing:

sudo apt-get install cmake ccache ninja-build cmake-curses-gui
sudo apt-get install libxml2-utils ncurses-dev
sudo apt-get install curl git doxygen device-tree-compiler xxd
sudo apt-get install u-boot-tools
sudo apt-get install python3-dev python3-pip python-is-python3
sudo apt-get install protobuf-compiler python3-protobuf

Simulating with QEMU

In order to run seL4 projects on a simulator you will need QEMU:

sudo apt-get install qemu-system-arm qemu-system-x86 qemu-system-misc

Cross-compiling for ARM targets

To build for ARM targets you will need a cross compiler:

sudo apt-get install gcc-arm-linux-gnueabi g++-arm-linux-gnueabi
sudo apt-get install gcc-aarch64-linux-gnu g++-aarch64-linux-gnu

(you can install the hardware floating point versions as well if you wish)

sudo apt-get install gcc-arm-linux-gnueabihf g++-arm-linux-gnueabihf

Cross-compiling for RISC-V targets

To build for RISC-V targets you will need a cross compiler:

It is recommended to build the toolchain from source.

git clone https://github.com/riscv/riscv-gnu-toolchain.git
cd riscv-gnu-toolchain
git submodule update --init --recursive
export RISCV=/opt/riscv
./configure --prefix="${RISCV}" --enable-multilib
make linux

After it is built, add the $RISCV/bin folder to your PATH. The built toolchain works for both 32-bit and 64-bit.

Alternatively, any pre-built toolchain with multilib enabled should work.

Building the seL4 manual

If you would like to build the seL4 manual, you will need the following LaTeX pacakges:

sudo apt-get install texlive texlive-latex-extra texlive-fonts-extra

Debian

The dependencies listed in our Docker files repository will work for a Debian Bullseye, most likely also for later releases. You can refer to this repository for an up-to-date list of base build dependencies. Specifically refer to the dependencies listed in the file here:

• Base Tools
• seL4
• LaTeX

Python

A number of Python packages are required to build seL4 and its manual. To install these you can run:

pip3 install --user setuptools sel4-deps

(Some distributions use pip for python3, others use pip3. Use the Python 3 version for your distribution)

python3 -m venv seL4-venv
./seL4-venv/bin/pip install sel4-deps

source ./seL4-venv/bin/activate

Test

To test whether your build environment works, we recommend running the seL4 test suite in quemu. For instance:

# target directory
mkdir sel4test
cd sel4test

# get the sources
repo init -u https://github.com/seL4/sel4test-manifest.git
repo sync

# create build directory
mkdir build
cd build

# configure build
../init-build.sh -DSIMULATION=TRUE -DAARCH32=TRUE -DPLATFORM=sabre

# build
ninja

# run
./simulate

This should start qemu and run a series of tests. Don’t worry if error messages appear, they are explicit tests for errors.

An output of All is well in the universe at the end indicates a successful test run. To exit qemu, press Ctrl-a, then x.