Properly submodule seL4

[podhrmic]

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]

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]

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]

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]

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]

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]

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

[podhrmic]

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]

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]

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.

[wucke13]

Just to chime in on this: I'm strongly against using Google's repo tool. I would much prefer a git submodule. It is the more vanilla, more common, by far better tool-supported approach. I also think that its usage in the rest of the seL4 ecosystem is a burden. I fully understand that there is a process centering around this tool (i.e. most seasoned seL4 contributors know how to use it and grew comfortably doing so), but that should not be the only decision driver in spreading its usage further.

[lsf37]

This decision is not really up to this repository. Using git submodules here would need a TSC discussion and decision.

We have had this discussion multiple times, and git submodules always were found insufficient (and in fact not be better supported by tools). If this is a fundamentally new situation, then I'm fine to put it on the agenda again. If it is just preference, the answer is "no", we have discussed this at length and decided against.

The experience with the one exception that has managed to sneak in (on the website repo, but also on other repos that are not under TSC control) is that the user experience with git submodules is strictly worse, people are more confused and make more mistakes with it.

[wucke13]

Understood. Please note, that I'm by no means a strong proponent for git submodules in general. I'm just strongly against git-repo. And for this particular use case (one dependency in the form of that repo with this commit), git submodules are just the simplest, most common substitute. There may be better options, just git-repo is not among them IMHO.

I totally agree that git submodules have sub-optimal UX, and I do not want to advocate for them as the advised substitute for git-repo in general.