System configuration and building
seL4, CAmkES, and the C support libraries use the CMake family of tools to implement their build system. The seL4 build system refers to a collection of CMake scripts that manage:
- system configuration: configuration options such as platform flags and application settings,
- dependency structures: tracking build order dependencies, and
- builds: generating binary artefacts that can then be deployed on hardware.
This document covers how to use the seL4 build system to:
- perform system configuration and builds,
- incorporating the build system into a project, and
- produce kernel stand-alone configuration and builds
CMake basics
For a complete guide to CMake see the extensive documentation, but for the purposes here we will assume a particular workflow with CMake involving out-of-tree builds.
CMake is not itself a build tool, but rather is a build generator. This means that it generates build scripts, typically Makefiles or Ninja scripts, which will be then used by a tool like Make or Ninja to perform the actual build.
Pre-requisites
It is assumed that
- CMake of an appropriate version is installed.
- You are using the Ninja CMake generator.
- You have the required dependencies installed to build your project and understand how to check out repo collections.
Steps
Interfacing with other build systems
The page on standalone kernel builds shows how to generate a
bare kernel binary without user-level image or loader, for use in other build
system or in formal verification. The kernel build system produces .json
and
.yaml
files with information on the configuration that was used to produce the
binary, for consumption in other build systems.
Gotchas
List of easy mistakes that can be made when using CMake
- Configuration files passed to to cmake with
-C
must end in.cmake
, otherwise CMake will silently throw away your file