seL4 / microkit

Microkit - A simple operating system framework for the seL4 microkernel
Other
70 stars 37 forks source link

Add basic CI #24

Closed Ivan-Velickovic closed 9 months ago

Ivan-Velickovic commented 1 year ago

This patch attempts to bring basic CI to seL4CP. Currently, it only builds the SDK and then uploads the artefact for anyone to be able to download.

An example of a CI run is here: https://github.com/Ivan-Velickovic/sel4cp/actions/runs/4602867006.

There are some costs to consider with using GitHub provided CI however.

Other aspects to discuss:

lsf37 commented 1 year ago

From my side this would do for a start.

There are some costs to consider with using GitHub provided CI however.

  • They run in a virtualised environment, with other dependencies already installed and possibly other configuration that does not match the environment that a developer would use when building/using the SDK.
  • It is quite slow, takes about 5-6 minutes on a GitHub runner vs about one minute on my personal computer. Some of this time is due to having to install the dependencies each time the CI is run, which might actually be a good thing.

Not saying you should do this now, but it is possible to address both points above with a docker container (e.g. using ci-actions infrastructure), building a container with just the dependencies here so that it only needs to pull the container and not go through the install process every time.

The actual tests then run in the container, which also makes it very reproducible.

The tool chains are large, so pulling the container will still take some time, but it'll not be 6min.

If you really want to simulate the environment a developer might be running, you should probably take a full Ubuntu container or VM and go from there. That could be a test that runs less frequently (just because it takes longer and is likely to work if the minimal version works).

  • One of the issues I generally have with CI is that it is often hard to reproduce. In this patch all the setup is done in GitHub's YAML format, alternatively, we could do most of the setup in a shell script. This way people should be able to reproduce the CI results themselves, also it would make it easier for anyone wanting to set up their own CI for seL4CP.

That is one of the points of the ci-actions repo: the steps to reproduce are all shell or python scripts that are just called from CI. You can usually run them locally, and if it uses a container, you can pull the container and run the script inside it.

One thing you're currently missing is configuration control: which version of the seL4 CP is tested with which version of seL4. This may be clear currently, but it will evolve over time. There are two things to do: specifying which combination(s) you want tested and recording a log of which combination was actually tested (usually together with a record somewhere of which of these were successful). I think it's fine to hard code it for a start as it is here, but if we move it over later, we should probably introduce a manifest that records what is going on and which versions fit together (doesn't have to be user visible, just for CI).

Ivan-Velickovic commented 1 year ago

The thing I would like to avoid is succumbing to a Docker container. Everything should be just as easy to do on a real computer as in Docker. The reasoning for this is because I feel like adding more layers of software to this problem is not solving it, and I'm not convinced that Docker yields reproducible results without adding significant complexity and other maintenance problems. But, I'm not that experienced in this area, maybe I am wrong.

I agree that it would probably be slightly faster with a Docker container.

What I was looking for when reproducing the CI is let's say that I've made some changes to seL4CP and before I push I want to check that I haven't broken anything too drastically, I should just be able to do ./ci.sh and everything should build and run/test just like it does on CI. If the ci-actions repo does that already, then I'm happy with that.

lsf37 commented 1 year ago

The thing I would like to avoid is succumbing to a Docker container.

Don't worry, I'm not a fan either ;-). It does end up useful for some things, though.

Everything should be just as easy to do on a real computer as in Docker.

Absolutely. You'd be running exactly the same thing.

The reasoning for this is because I feel like adding more layers of software to this problem is not solving it, and I'm not convinced that Docker yields reproducible results without adding significant complexity and other maintenance problems. But, I'm not that experienced in this area, maybe I am wrong.

I agree that it would probably be slightly faster with a Docker container.

Docker would be purely for CI performance here, nothing in the build should need it. What it would be for is creating a state similar to what you have on your local machine where you develop and start the test run from there.

What I was looking for when reproducing the CI is let's say that I've made some changes to seL4CP and before I push I want to check that I haven't broken anything too drastically, I should just be able to do ./ci.sh and everything should build and run/test just like it does on CI. If the ci-actions repo does that already, then I'm happy with that.

Yes, but it's never quite so simple, because CI always needs to do more than what you do locally. Locally you already have a repo checked out, dependencies installed, a build config set up etc. CI first needs to do all that or get into a state that is like that. From then on, it should be the same, and yes, that should be a single command if possible.

As you can see in your GitHub action, 90% of CI is this install and setup (plus build matrix for tools/boards etc if it gets to that). The actual test run itself is usually the simplest part.

The ci-actions repo has a steps.sh script for each action that does everything that is needed. If you read that script, there is usually one single invocation that is the actual test. That is the command you would run locally.

If you don't mind the additional install steps and repo checkouts on your local machine, you can run steps.sh just from the shell (after setting some env variables to give it context), or it can run in a VM or inside a container if you want to make sure that it doesn't overwrite/ anything you care about or install things you don't want.

podhrmic commented 1 year ago

FYI the Rust Core Platform example works like a charm, it is based on this dockerfile.

lsf37 commented 1 year ago

FYI the Rust Core Platform example works like a charm, it is based on this dockerfile.

Very glad to hear that! The plan is to invest in some more documentation on the Rust side and then make it officially part of the foundation repositories.

Ivan-Velickovic commented 9 months ago

An additional check should be checking the result of mypy.