Gerwin Klein

> Sorry this is on my (fairly large) todo list. All the information I have for now is this: > > When all the debug related functions and statements were...

No opinions from me on that one. Ideally, the concatenated C file that the verification sees should also be what the compiler gets, unless you are also planning to do...

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,...

> 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...

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

It's possible, see e.g. the [rumprun repo](https://github.com/seL4/rumprun-sel4-demoapps), but I'm unsure if Ivan will like it :-) I think the two manifest files have to be at the top level for...

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...

> Something I forgot to mention at the Summit is that because of the system description to CapDL translation validation, in the future it will not matter whether we trust...

Just to confirm: the plan is to converge all of this so it works together out of the box. It'll take a bit more time until it is there, but...

Copyright years should usually not be updated in bulk, at least not if the idea is to figure out the year of the most recent original copyright on the file....