This repository collects definitions for continuous integration (CI) tasks/actions for the repositories of the seL4 Foundation. While some of these might be useful more generally, most of them will be specific to the seL4 setup.
The idea is to concentrate most of the GitHub workflow definitions here in a single repository to avoid duplication, share code between actions, and to make it easier to replicate a similar CI setup on other platforms.
Shared JavaScript is in js/, and shared shell scripts are in scripts/
This repository also defines a number of GitHub action workflows that can be
called from other repositories. These are all files in .github/workflows that
define an on: workflow_call trigger. In particular:
- pr.yml for standard pull requests checks (gitlint, whitespace, shell checks, style)
- push.yml for standard push checks (links, licenses)
- sel4test-sim.yml for running the seL4 simulation tests
- sel4test-hw.yml for running the seL4 hardware tests
- sel4bench-hw.yml for running the seL4 hardware benchmarks
The following GitHub actions are available:
- AWS Proofs: run the l4v proofs on AWS
- Bashisms: check shell for non-portable shell scripts
- CAmkES Hardware Test: CAmkES test hardware runs
- CAmkES Tests: CAmkES test builds and simulations
- CAmkES Unit Tests: unit tests for the
camkes-toolrepository - CAmkES VM Tests: CAmkES VM tests
- CAmkES VM Hardware Tests: CAmkES VM hardware runs
- CParser Run: check seL4 PRs for C verification subset
- Git Diff Check: check for trailing whitespace and merge conflict markers
- Gitlint: run gitlint on pull requests
- Isabelle Mirror: mirrors the upstream Isabelle repository to git
- L4v Deploy: deploys l4v default.xml manifest after successful proof runs
- License Check: runs the FSFE reuse license tool
- Link Check: checks links in
.mdand.htmlfiles - Manifest Deploy: deploys default.xml manifests after successful tests
- m-arch of Platform: outputs the
marchof a given platform - Preprocess: run AST diff on preprocessed source for verified configurations
- Repo Checkout: checks out a
repocollection - RumpRun: rumprun hello-world simulation test
- RumpRun Hardware: rumprun hello-world test on hardware
- Run Proofs: run the l4v proofs in docker (not used in CI)
- seL4 Benchmark Builds: sel4bench image builds
- seL4 Benchmark Runs: run sel4bench images on hardware
- seL4 Benchmark Results: publish sel4bench results to the seL4 website
- seL4 Manual: build seL4 PDF manual
- seL4Test Hardware Builds: sel4test image builds
- seL4Test Hardware Runs: sel4test hardware runs
- seL4Test Hardware Run Matrix: matrix for sel4test hardware runs
- seL4Test Simulation: sel4test simulations for platforms with a simulation binary
- Standalone Kernel: standalone seL4 kernel compilation
- Style: coding style checks of the seL4 Foundation
- Thylint: basic Isabelle theory file linter
- Trigger: triggers a test run in the main repository of a repo manifest set
- Tutorials: run the seL4 tutorial tests (simulation only)
- Webserver Tests: builds for the seL4 webserver demo app
- Webserver Hardware Tests: hardware runs for the seL4 webserver demo app
Contributions are welcome!
See open issues for things than need work, there is also a list of good first issues if you are new to all this and want to get involved.
See the file CONTRIBUTING.md for more information.
See the directory LICENSES/ for a list of the licenses used in this repository, and the SPDX tag in file headers for the license of each file.