Host Dependencies
This page describes how to set up your host machine to build and run seL4 and its supported projects. To compile and use seL4 you can either:
- Recommended: Use Docker to isolate the dependencies from your machine. Detailed instructions for using Docker for building seL4, Camkes, and L4v can be found here.
- Install the following dependencies 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 building in alternative OSes (e.g. macOS).
Get Google’s Repo tool
The primary way of obtaining and managing seL4 project source is through the use of Google’s repo tool. To get repo, follow the instructions described in the section “Installing Repo” here.
See the RepoCheatsheet page for a quick explanation of how we use Repo.
seL4 Build Dependencies
To build seL4-based projects, ensure you have installed the dependencies described in the Base Build Dependencies and Python Dependencies sections below.
Base Build Dependencies
To establish a usable development environment it is important to install your distributions basic build packages.
Ubuntu
The following instructions cover the build dependencies tested on Ubuntu 18.04 LTS. Note that earlier versions of Ubuntu (e.g. 16.04) may not be sufficient for building as some default development packages are stuck at older versions (e.g CMake 3.5.1, GCC 5.4 for 16.04). As dependencies and packages may be frequently changed, deprecated or updated these instructions may become out of date. If you discover any missing dependencies and packages we welcome new contributions to the page.
Note that we require a minimum CMake version of 3.12.0 while Ubuntu 18.04 contains 3.10.2. In order to correct this, a custom installation of CMake may be required which can be downloaded from: https://cmake.org/download/
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 python-dev python-pip python3-dev python3-pip
sudo apt-get install libxml2-utils ncurses-dev
sudo apt-get install curl git doxygen device-tree-compiler
sudo apt-get install u-boot-tools
sudo apt-get install protobuf-compiler python-protobuf
To build for ARM targets you will need a cross compiler. In addition, to run seL4 projects on a simulator you will need qemu
. Installation of these additional base dependencies include running:
sudo apt-get install gcc-arm-linux-gnueabi g++-arm-linux-gnueabi
sudo apt-get install gcc-aarch64-linux-gnu g++-aarch64-linux-gnu
sudo apt-get install qemu-system-arm qemu-system-x86 qemu-system-misc
(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
Debian
For Debian Stretch or later
The dependencies listed in our docker files repository will work for a Debian installation. You can refer to this repository for an up-to-date list of base build dependencies. Specifically refer to the dependencies listed in the:
The version of cmake
in Debian stretch is too old to build seL4 projects (buster and later are OK). If you are on stretch, install cmake
from stretch-backports:
Add the stretch-backports repository like this (substitute a local mirror for ftp.debian.org
if you like)
sudo sh -c "echo 'deb http://ftp.debian.org/debian stretch-backports main' > /etc/apt/sources.list.d/backports.list"
Then install cmake
with
sudo apt-get update
sudo apt-get -t stretch-backports install cmake
Python Dependencies
Regardless of your Linux distribution, python dependencies are required to build seL4, the manual and its proofs. To install you can run:
pip3 install --user setuptools
pip3 install --user sel4-deps
# Currently we duplicate dependencies for python2 and python3 as a python3 upgrade is in process
pip install --user setuptools
pip install --user sel4-deps
(Some distributions use pip
for python3 and pip2
for python2; others uses pip
for python2 and pip3
for python3. Use the Python 3 version for your distribution)
CAmkES Build Dependencies
To build a CAmkES based project on seL4, additional dependencies need to be installed on your host machine. Projects using CAmkES (the seL4 component system) need Haskell and some extra python libraries in addition to the standard build tools. The following instructions cover the CAmkES build dependencies for Ubuntu/Debian. Please ensure you have installed the dependencies listed in sections sel4 Build Dependencies and Get Google’s Repo tool prior to building a CAmkES project.
Python Dependencies
The python dependencies required by the CAmkES build toolchain can be installed via pip:
pip3 install --user camkes-deps
# Currently we duplicate dependencies for python2 and python3 as a python3 upgrade is in process
pip install --user camkes-deps
Haskell Dependencies
The CAmkES build toolchain additionally requires Haskell. You can install the Haskell stack on your distribution by running:
curl -sSL https://get.haskellstack.org/ | sh
If you prefer not to bypass your distribution’s package manager, you can do
sudo apt-get install haskell-stack
Build Dependencies
Ubuntu
Tested on Ubuntu 18.04 LTS
Install the following packages on your Ubuntu machine:
sudo apt-get install clang gdb
sudo apt-get install libssl-dev libclang-dev libcunit1-dev libsqlite3-dev
sudo apt-get install qemu-kvm
Debian
For Debian Stretch or later
The dependencies listed in our docker files repository will work for a Debian installation. You can refer to this repository for an up-to-date list of base build dependencies. Specifically refer to the dependencies listed in the:
Proof and Isabelle Dependencies
Proof Dependencies
Linux Packages - Debian
On Buster or Bullseye, to run all proofs against the ARMv7-A architecture you will need to install the following packages:
sudo apt-get install \
python3 python3-pip python3-dev \
gcc-arm-none-eabi build-essential libxml2-utils ccache \
ncurses-dev librsvg2-bin device-tree-compiler cmake \
ninja-build curl zlib1g-dev texlive-fonts-recommended \
texlive-latex-extra texlive-metapost texlive-bibtex-extra \
rsync
There is no package for the MLton compiler on Buster or Bullseye, so you will need to install it from the MLton website.
The Haskell Stack package is unavailable on Bullseye and out-of-date on Buster, so you will need to install it from the Haskell Stack website.
Linux Packages - Ubuntu
On Ubuntu 18.04, to run all proofs against the ARMv7-A architecture you will need to install the following packages:
sudo apt-get install \
python3 python3-pip python3-dev \
gcc-arm-none-eabi build-essential libxml2-utils ccache \
ncurses-dev librsvg2-bin device-tree-compiler cmake \
ninja-build curl zlib1g-dev texlive-fonts-recommended \
texlive-latex-extra texlive-metapost texlive-bibtex-extra \
mlton-compiler haskell-stack
Python
The build system for the seL4 kernel requires several python packages:
sudo pip3 install --upgrade pip
sudo pip3 install sel4-deps
Haskell Stack
After installing
haskell-stack, make sure
you’ve adjusted your PATH
to include $HOME/.local/bin
, and that you’re
running an up-to-date version:
stack upgrade --binary-only
which stack # should be $HOME/.local/bin/stack
MacOS
Other than the cross-compiler gcc
toolchain, setup on MacOS should be similar
to that on Ubuntu. To set up a cross-compiler, try the following:
- Install
XCode
from the AppStore and its command line tools. If you are running MacPorts, you have these already. Otherwise, after you have XCode installed, rungcc --version
in a terminal window. If it reports a version, you’re set. Otherwise it should pop up a window and prompt for installation of the command line tools. - Install the seL4 Python dependencies, for instance using
sudo easy_install sel4-deps
.easy_install
is part of Python’ssetuptools
. - Install the
misc/scripts/cpp
wrapper for clang, by putting it in~/bin
, or somewhere else in yourPATH
.
Isabelle Setup
After the repository is set up using repo
with
seL4/verification-manifest
, you should have following directory
structure, where l4v
is the repository you are currently looking at:
verification/
isabelle/
l4v/
seL4/
To set up Isabelle for use in l4v/
, assuming you have no previous
installation of Isabelle, run the following commands in the directory
verification/l4v/
:
mkdir -p ~/.isabelle/etc
cp -i misc/etc/settings ~/.isabelle/etc/settings
./isabelle/bin/isabelle components -a
./isabelle/bin/isabelle jedit -bf
./isabelle/bin/isabelle build -bv HOL-Word
These commands perform the following steps:
- create an Isabelle user settings directory.
- install L4.verified Isabelle settings.
These settings initialise the Isabelle installation to use the standard
Isabelle
contrib
tools from the Munich Isabelle repository and set up paths such that multiple Isabelle repository installations can be used side by side without interfering with each other. - download
contrib
components from either the Munich or TS repository. This includes Scala, a Java JDK, PolyML, and multiple external provers. You should download these, even if you have these tools previously installed elsewhere to make sure you have the right versions. Depending on your internet connection, this may take some time. - compile and build the Isabelle PIDE jEdit interface.
- build basic Isabelle images, including
HOL-Word
to ensure that the installation works. This may take a few minutes.
Alternatively, it is possible to use the official Isabelle2020 release
bundle for your platform from the Isabelle website. In this case, the
installation steps above can be skipped, and you would replace the directory
verification/isabelle/
with a symbolic link to the Isabelle home directory
of the release version. Note that this is not recommended for development,
since Google repo will overwrite this link when you synchronise repositories
and Isabelle upgrades will have to be performed manually as development
progresses.