search

seL4 / microkit

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

Properly submodule seL4 #72

Open podhrmic opened 9 months ago

podhrmic commented 9 months ago

Can seL4 kernel be added as a submodule to Microkit? That way the build is always reproducible - I know you have a version listed in the README, but this will inevitably become outdated.

lsf37 commented 8 months ago

While I do agree that configuration management should definitely be formalised, we should not introduce yet another mechanism. The rest of the seL4 repos use Google repo manifests for this, we should do the same here.

I think for the microkit it would be important to make sure that it is useable without using the repo tool, but that looks achievable.

Ivan-Velickovic commented 8 months ago

I'm not convinced it would be outdated, both git submodules and repo have pretty horrific user-experiences so I don't want to force them on anyone.

Ivan-Velickovic commented 8 months ago

But I do agree with Gerwin that I guess because repo has been chosen for the eco-system we should at least remain consistent if we do use a tool to abstract over cloning a repository.

lsf37 commented 8 months ago

I'm not convinced it would be outdated, both git submodules and repo have pretty horrific user-experiences so I don't want to force them on anyone.

I agree with the user experience side, that's why I want it to be usable without.

But: a hash in a README is not good enough for automation, and if you imagine this going for 10 years or longer, you really need a machine-readable record of which versions fit together and were tested together, otherwise you won't be able to reproduce anything from the past. Apart from that, formal configuration management is a hard requirement for a lot certification schemes and it's not going to be good enough when it gets introduced at the point of certification. So something is definitely needed.

If done right, users should not have to interact with repo at all: in the ideal steady state, the microkit main branch tracks seL4 master branch, and microkit releases document which seL4 releases they are for. It's only CI or people who actually want to use it that should need to interact with it. Exceptions (like now) could still be documented in the README.

Ivan-Velickovic commented 8 months ago

Sure. I agree with all of that then. I think it's already usable without it so having a separate microkit-manifest repository should be all that is necessary? Then the only other thing to do is update the README to give people both options for acquiring the source code.

lsf37 commented 8 months ago

Yes, I think that makes sense. CI would then be updating the manifest to record which versions succeeded similar to the other manifests.

podhrmic commented 8 months ago

Roger that, repo works for me and it makes sense for consistency. AFAIK there is only one Microkit dependency, and that is seL4 kernel - is it possible to have the manifest in the same repo as Microkit? Otherwise you have a whole separate repository to hold a trivial manifest.

lsf37 commented 8 months ago

It's possible, see e.g. the rumprun repo, but I'm unsure if Ivan will like it :-)

I think the two manifest files have to be at the top level for the repo tool to work.

Ivan-Velickovic commented 8 months ago

I think having separate repositories can sometimes be confusing to outsiders, especially those new to seL4. I think it might just be simpler to have the manifest files with the source code.