Configuring and building an seL4 project
This page contains documentation for how to interact with and build a project that is using this build system. For new project development, see incorporating the build system.
Basic build initialisation
In the root directory of a seL4-based project, first create a separate build directory for the output binaries, then initialize CMake:
cmake -DCROSS_COMPILER_PREFIX=arm-linux-gnueabi- -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake <OTHER_COMMAND_LINE_OPTIONS_HERE> -G Ninja ..
We now break down each component in the above invocation:
-Ddefines a variable, in the form
CROSS_COMPILER_PREFIXspecifies the toolchain for cross-compilation, which cannot be changed after build directory initialisation. For further details, please see “Cross Compiling” below.
CMAKE_TOOLCHAIN_FILEwhich indicates that CMake should load the specified file as a ‘toolchain’ file. A toolchain file is able to set up the C compiler, linker etc., for building the project. In the example we assume a typical project layout, where seL4 is in the ‘kernel’ directory, at the top level. The gcc.cmake’ file from the seL4 repository sets up C compilers and linkers using the
-G Ninjatells CMake to generate Ninja build scripts as opposed to GNU Makefiles. Only Ninja scripts are supported by parts of the kernel.
..is the path to the top-level
CMakeLists.txtfile describing this project, which in this case is placed in the root directory of the project.
We also provide a shorthand wrapping script which abstracts the above into a shorter command:
../init-build -DCROSS_COMPILER_PREFIX=arm-linux-gnueabi- <COMMAND_LINE_OPTIONS_HERE>
After configuration, you can build the project by invoking ninja:
After the build has completed, the resulting binaries will be in the
Types of Options
CMake has two types of configuration options:
- Boolean options, which are are either
- String options, which can be set to any value, subject to restrictions set by the project authors.
String options can have ‘hints’, which specify can one of several fixed values. CMake configuration editors respect these and provide a radio selection.
Many projects have some degree of customisation available via configuration options. Once the build directory is initialised, you can use the following approaches to bring up a user-interface for option configuration:
- Graphical configuration:
In both cases the path
. should resolve to the same directory used in the build configuration.
Changing option values
Any changes to configuration options will not be reflected in the user interface unless explicitly
requested by using
(c)onfigure, which may result in changes to the options available.
For example if option
A depends on boolean option
A will not show up until
B is enabled and
(c)onfigure is used to reprocess the CMake files.
To exit the configuration interface, use
(g)enerate and exit or
(q)uit without generation. CMake
will not permit generation if the configuration is incomplete (
(c)onfigure must be run and all
To rebuild after changing configuration options, invoke ninja:
Many of our projects support multiple configurations, where the following broad approaches are used to present simple options to the user:
- CMake cache scripts: These files can assign initial values to any number of configuration variables. By combining one or more of these together you can configure an entire system.
- Meta configuration options: Meta configuration options are normally
passed as initial
-DVAR=FOOcommand line arguments to CMake and will be programatically inspected by projects’ CMake scripts to (re)configure the system.
CMake cache scripts:
CMake cache scripts provide subsets of preconfigured options, which allow the user of a project to
avoid manually setting each option. Cache scripts have the file extension
Projects may provide cache script files which each contain the cache
settings necessary to configure a single feature or option. By combining
.cmake files, a project can be initialised in a specific way.
Cache script configurations are provided
-C <file> to
cmake when initialising the build directory.
For example, given a typical project structure,
one might invoke
init-build.sh with several of
cache scripts as arguments.
Multiple cached scripts can be specified on the command line, although if the same option is set twice
only one value is used. Consider an example with several cache scripts for setting the architecture
x86.cmake) and for setting build options (
The intended usage is that one architectural cache file is used, and one build options file, as
cmake -C../projects/awesome_project/configs/arm.cmake -C../projects/awesome_project/configs/debug.cmake -DCROSS_COMPILER_PREFIX=arm-linux-gnueabi- -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja ..
While nothing prevents the usage of both
x86.cmake at the same time, this does not
make sense, and only one value for each option will be used. For projects with multiple cache scripts,
check which can be used together.
Meta configuration options:
Some seL4 projects provide top-level variables which, used across projects, have the same behaviour. These options are as follows:
-DPLATFORM=<YOUR_PREFERENCE>: Selects the target system for the resulting binaries. Valid values for this variable are the first value (preceding the semicolon) on each line of the
config_choicedirective for each architecture:
-DRELEASE: Set to
1: Turning this off compiles a debug build. Turning it on compiles the project without debugging features enabled.
-DVERIFICATION: Set to
1: This is used to generate the version of the seL4 kernel source which is VERIFIABLE. This does not produce a binary for the verified kernel platform.
-DSMP: Set to
1: Turns SMP (symmetric multiprocessing) support on or off. By default it will enable support for up to 4 processors. To explicitly set the maximum number of supported CPUs, try setting
-DSIMULATION: Set to
1: This produces a build of the project which is suited for running in an emulator such as QEMU.
For more information on configuring, building and running the sel4test suite, please see the main page on seL4test.
Cross compilation refers to compiling a program for a target machine which is different from the machine you are using to compile the program.
Generally, in order to cross-compile, a separate compiler is required which specifically targets the foreign machine.
For ARM-based targets:
You can use the following command line options when when cross-compiling for an ARM-based machine:
-DAARCH32=TRUE: Tells the build system that you are building for a 32-bit ARM target. This will cause the build system to assume that you have a cross compiler installed which targets a system with the triplet name
-DAARCH32HF=TRUE: Tells the build system you’re building for a 32-bit ARM target which has hardware floating point support. Assumes you have a cross- compiler installed which targets
-DAARCH64=TRUE: Tells the build system you’re building for a 64-bit ARM target. Assumes you have a cross-compiler installed which targets
Another option is to explicitly specify the toolchain through
which can be used to set the prefix of the
cross-compiler to use.
For RISC-V based targets:
You can use the following options when cross compiling for a RISC-V target:
-DRISCV32=TRUE: Tells the build system that you are building for a 32-bit RISC-V target. This will cause the build system to assume that you have a cross- compiler installed which targets a system with the triplet name
-DRISCV64=TRUE: Tells the build system you’re building for a 64-bit RISC-V target. Assumes you have a cross-compiler installed which targets
Like ARM, you can explicitly specify the toolchain through
which can be used to set the prefix of the
cross-compiler to use.
CMAKE_BUILD_TYPE option appears in CMake configuration editors and allows users to configure
that build type (release, debug etc.). Note that this option is not respected by the seL4 kernel.
Building with Clang
The kernel as well as, some other projects, can be built using the clang compiler. To select this configuration,
-DTRIPLE variable must be set in the initial configuration step i.e pass in as an argument to the
The value of the
TRIPLE should be the target for which you are compiling.
../init-build -DTRIPLE=x86_64-linux-gnu <COMMAND_LINE_OPTIONS_HERE>
CROSS_COMPILER_PREFIX argument is unnecessary and ignored when compiling with clang. When building for arm based targets, the target
TRIPLE will be equal
CROSS_COMPILER_PREFIX (when using gcc) without the trailing ‘-‘.
Using clang to compile for RISC-V based targets is currently not supported.