Proper CI

[Ivan-Velickovic]

Initial CI has been added just to double-check PRs that look like they don't break anything.

We will of course need proper CI that also tests the SDK. This will include

• Tests of basic functionality that do not depend on specific hardware. Some tests exist, but not enough.
• Building and executing (when possible) the examples for each hardware platform.
• Figuring out every dependency Microkit has and what version of each dependency to pin it to. This needs to be done systematically, the only way I know of doing that is via Nix. We could look into a Docker container as well.
• Checking that the Microkit tool still type checks with mypy.
• Documenting how contributors can reproduce each step of CI.
• From https://github.com/seL4/microkit/pull/62, we should also test using non-GCC tools to produce a Microkit system.

We should also discuss whether to make available a 'mainline' build of the SDK for download for those who want to use the latest version.

[lsf37]

Looks like a good list. Additional ideas (not necessarily all for right now):

• Ideally, we'd also have an actual test suite that tests each feature with positive and negative tests (i.e. try things that should fail and make sure they do fail, such as writing to other PDs etc).
• This could over time include a regression test suite that collects things that have been fixed over time to make sure those are not re-introduced by other changes.
• Simulation tests can usually run on every PR, building for all hardware platforms possibly as well, but hardware tests should probably triggered by label only to not overload the machine queue. There is code for that in some of the other seL4 repos.

For dependency pinning: we should converge things so that the seL4 docker container has precisely what is needed and works for the SDK. Maria had a PR for that container a while ago, we could look at that again.

The closer the tool chains are to a default Debian or Ubuntu setup the better (or at least the fewer problems we will get from people who try defaults despite instructions).

[Ivan-Velickovic]

For dependency pinning: we should converge things so that the seL4 docker container has precisely what is needed and works for the SDK. Maria had a PR for that container a while ago, we could look at that again.

I guess given how bloated the Docker container is already, it probably wouldn't hurt to add the Microkit dependencies as well (the bloat is more of a Docker problem than seL4).

The closer the tool chains are to a default Debian or Ubuntu setup the better (or at least the fewer problems we will get from people who try defaults despite instructions).

Sure. It may be worth mentioning that doing things via default Ubuntu/Debian packages is not supported or has less support. We've already run into at least one case where apt does the wrong thing for one of Microkit's dependencies.

The real solution is probably to have less dependencies, but I'm not sure how feasible that is.

[Ivan-Velickovic]

• Ideally, we'd also have an actual test suite that tests each feature with positive and negative tests (i.e. try things that should fail and make sure they do fail, such as writing to other PDs etc).

Yes definitely.

Simulation tests can usually run on every PR, building for all hardware platforms possibly as well, but hardware tests should probably triggered by label only to not overload the machine queue. There is code for that in some of the other seL4 repos.

Sure. Most of the slowness of hardware testing comes from booting and loading binaries via the network, even though most of the Microkit tests would be very quick, I imagine it would still take a couple of minutes to run all of them on hardware.

[lsf37]

The real solution is probably to have less dependencies, but I'm not sure how feasible that is.

Yup, definitely the fewer the better.

[podhrmic]

Definitely excited about having a proper CI!

IMHO having another Docker image would be fine, especially because the python deps of microkit don't look that bad. Looking at the sel4 build script it seems like you get the most bloat right there?

About Nix - when it works, it works great, but we had a fair deal of problems with it (happy to chat more) so I wouldn't recommend it for Microkit.