For cross platform development, a developer can choose to use the toolchains provided by the Linux distribution they are using.

NOTE: The apt-get and pip commands may need to be run with root privilege. If this is the case, pre-pend sudo to the command.

For an Ubuntu host machine, one would use apt-get:

apt-get update
apt-get install autoconf git build-essential realpath libxml2-utils python-tempita ccache ncurses-dev cmake ninja-build clang libssl-dev libsqlite3-dev libcunit1-dev expect
# Ubuntu provided toolchain pakcages
apt-get install gcc-arm-none-eabi gcc-arm-linux-gnueabi gcc-5-aarch64-linux-gnu

If the developer would like to cross compile for 32-bit x86 they may have to install the gcc-multilib package.

apt-get install gcc-multilib

It is important that when the developer is ready to build, that they use the correct tool prefix in the .config file or in the tool chain configuration menu when they are using menuconfig.

The official seL4 projects use Google’s repo tool to orchestrate project layout. The Google installation instructions show the following:

mkdir -p ~/bin
PATH=~/bin:$PATH
curl https://storage.googleapis.com/git-repo-downloads/repo > ~/bin/repo
chmod a+x ~/bin/repo

The developer needs to make sure that the location of the repo tool is in their $PATH environment variable. This may require making this change in their .bashrc file. To check if your system knows about the repo tool, run which repo at the command line. This will show the location of it, if there is nothing returned, the system doesn’t know where it is.

With these tools, the developer can build seL4 projects but there are more requirements for CAmkES based projects. Haskell is required for the Capability Description Language (CapDL):

curl -sSL https://get.haskellstack.org | sh

The seL4 developers conveniently provide the CAmkES python dependencies in a PyPi package:

pip install camkes-deps

Once a binary is built, the developer can test it with QEMU.

Ubuntu provides packages in their package manager:

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

The directory structure of the seL4 kernel, libraries, and tools are organized based on a repo manifest file, which pulls the correct git repositories and places them in a certain place. The make build tool can then be run at the root directory to build an image that is ready to be loaded by a bootloader or emulator.

The repo tool places everything such that the root directory is not tracked by git but the sub directories are still tracked by their respective repositories. This makes it relatively easy for build tool files to reference other projects and not muddy up the source trees with generated and compiled code.

A standard seL4 repo manifest is laid out like so:

.
├── apps -> projects/the-git-repo-for-your-app/apps
├── configs -> projects/the-git-repo-for-your-app/configs
├── include
├── kernel
├── libs
│   ├── libcpio -> ../projects/util_libs/libcpio
│   ├── libelf -> ../projects/util_libs/libelf
│   ├── libmuslc
│   ├── libplatsupport -> ../projects/util_libs/libplatsupport
│   ├── libsel4 -> ../kernel/libsel4
│   ├── libsel4bench -> ../projects/seL4_libs/libsel4bench
│   ├── libsel4camkes -> ../tools/camkes/libsel4camkes
│   ├── libsel4debug -> ../projects/seL4_libs/libsel4debug
│   ├── libsel4muslccamkes -> ../tools/camkes/libsel4muslccamkes
│   ├── libsel4muslcsys -> ../projects/seL4_libs/libsel4muslcsys
│   ├── libsel4platsupport -> ../projects/seL4_libs/libsel4platsupport
│   ├── libsel4simple -> ../projects/seL4_libs/libsel4simple
│   ├── libsel4simple-default -> ../projects/seL4_libs/libsel4simple-default
│   ├── libsel4sync -> ../projects/seL4_libs/libsel4sync
│   ├── libsel4utils -> ../projects/seL4_libs/libsel4utils
│   ├── libsel4vka -> ../projects/seL4_libs/libsel4vka
│   ├── libsel4vspace -> ../projects/seL4_libs/libsel4vspace
│   └── libutils -> ../projects/util_libs/libutils
├── projects
├── tools
│   ├── camkes
│   ├── capDL -> ../projects/capdl/capDL-tool
│   ├── common -> ../projects/seL4_tools/common-tool
│   ├── elfloader -> ../projects/seL4_tools/elfloader-tool
│   ├── kbuild -> ../projects/seL4_tools/kbuild-tool
│   ├── pruner
│   └── python-capdl -> ../projects/capdl/python-capdl-tool
├── Makefile -> projects/the-git-repo-for-your-app/Makefile
├── Kbuild -> projects/the-git-repo-for-your-app/Kbuild
└── Kconfig -> projects/the-git-repo-for-your-app/Kconfig

At first glance the directory structure can be somewhat intimidating. If you are ever confused where certain components might be, the main directories where source code is located are kernel and projects. The kernel directory is, obviously enough, where all the kernel code is. However, as can be seen in the previous listing, the apps directory is really a link to a directory under projects and so are some library directories under libs and some tools directories under tools. You can see where all of the directories are placed and linked to in the project manifest file. You can run the command repo manifest at the command line and it will print the contents of the currently used manifest file in .repo/manifest.xml. Each entry has a path, which is where the directory for that git repository is placed. The linkfile tags are where sub directories or files in that repository are linked to. You can also run the command find -type d -name ".git" to see where all of the git repositories are in the project tree.

The subsections that follow here are purely OPTIONAL. If you read through them and think that they are for you, then you can follow them, if not, then your seL4/CAmkES development will not be hindered.

Another option for the ARM cross compilers may be to install the Linaro toolchains from their repositories. For the 5.4 2017 version, the developer can use wget and tar to retrieve the binary tools:

wget https://releases.linaro.org/components/toolchain/binaries/5.4-2017.05/aarch64-linux-gnu/gcc-linaro-5.4.1-2017.05-x86_64_aarch64-linux-gnu.tar.xz
tar -xvf gcc-linaro-5.4.1-2017.05-x86_64_aarch64-linux-gnu.tar.xz

Now the developer would need to move that toolchain directory to somewhere on their machine where they keep tool chains and add that path to the beginning of their $PATH environment variable. This allows for an easy way to have multiple cross compiling toolchains that don’t change anything about your host system environment.

One technique for exploring the code base is to generate a list of files for the main projects (kernel, libs, and your application project) and then feeding this list of files tools for code base navigation aid. One such tool is cscope. Here is an example use case:

# Save the file name list into a file. This follows symlinks and saves the path relative to the project root
find kernel/{src,include} -type f -name "*.[chxsS]" -exec realpath --relative-to=$PWD ( readlink -f {} ) \; > kernel.files
find projects/{seL4_libs,util_libs} -type f -name "*.[chxsS]" -exec realpath --relative-to=$PWD ( readlink -f {} ) \; > libs.files
find projects/sel4test/ -type f -name "*.[chxsS]" -exec realpath --relative-to=$PWD ( readlink -f {} ) \; > sel4test.files
# Combine the all of them into one
cat kernel.files libs.files sel4test.files > seL4.files
# Change the name of the file list file to the default cscope one
cp seL4.files cscope.files
# Run cscope to generate the cross reference database of the whole project
cscope -bk
# Now use it
cscope -d

cscope can be used in combination with text-editors and IDE’s to give a more seamless navigation and development experience.

Emacs users that use the xcscope.el package must make sure that they set the initial directory to the repo root directory (C-c s a). Then they can use key chords to jump to global definitions (C-c s g), find references (C-c s s ), and much more.

Data61 provides a dockerfile container that has all the necessary dependencies to create seL4 and CAmkES applications. This requires the developer to install docker on their host machine.

Example install steps are as follows. NOTE: Most of these commands require root privilege.

add-apt-repository "deb [arch=amd64] https://download.docker.com/linux/ubuntu $(lsb_release -cs) stable"
apt-get update
apt-get install docker-ce
groupadd docker
usermod -aG docker $USER

For the group changes to take place the developer must log out and back in.

If the host machine’s init system is systemd, docker can be started at boot with:

systemctl enable docker

With docker installed, clone the dockerfile repository and use make to build the container.

git clone https://github.com/SEL4PROJ/seL4-CAmkES-L4v-dockerfiles.git
cd seL4-CAmkES-L4v-dockerfiles/
make user

This process will take some time, but eventually the process should end with the following logs:

___
 |   _      _ |_      _   _ |_ |_
 |  |  |_| _) |_ \)/ (_) |  |_ | ) \/
                                   /
 __
(_      _ |_  _  _   _
__) \/ _) |_ (- ||| _)
    /
Hello, welcome to the sel4/CAmkES/L4v docker build environment
user@in-container:/host$

Now we add an alias that allows us to run container to start in the container.

echo $'alias container=\'make -C ~/path/to/seL4-CAmkES-L4v-dockerfiles user HOST_DIR=$(pwd)\'' >> ~/.bashrc

This alias makes it much easier to invoke the correct docker command from the command line.

The version of QEMU is a little dated in the Ubuntu repositories. The developer can choose to compile it themselves. This gives the latest board and architecture options to the developer to test their code on. They may need to install some development libraries if they aren’t installed already:

apt get install libglib2.0-dev zlib1g-dev libpixman-1-dev libsdl2*

Then they can proceed to clone, configure, build, and install. Here, the QEMU source is cloned into the ~/gitrepos directory. This can be any directory on the system that is used to build software packages.

mkdir -p ~/gitrepos
cd ~/gitrepos/
git clone https://github.com/qemu/qemu.git
cd qemu
git branch -va
# Checkout the branch you want
git checkout stable-2.11
# Look at the confgire help to see what targets are needed
./configure --help
./configure --target-list=$YOURLISTHERE
make
# run this as root if you want it installed system wide
make install

NOTE: Installing software this way is at your own risk and is not managed by your host system’s package manager.