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.
If you discover any missing dependencies and packages we welcome new contributions to the page. You can edit this section directly on GitHub.
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:
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)
Error: Python environment is externally managed
Some Linux distributions have changed how Python is managed. If you get an error saying the Python ‘environment is externally managed’ follow the instructions below. The first two steps are needed only once for setup.
python3 -m venv seL4-venv
./seL4-venv/bin/pip install sel4-deps
The following step is needed every time you start using the build environment in a new shell.
source ./seL4-venv/bin/activate
It is not important where the seL4-venv
directory is located.
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
.