[seL4] Re: next seL4 TSC meeting on Thu 25 Jul

On 23 Jul 2024, at 20:41, Bob Trower wrote: I'm too far out of the loop with respect to specifics, but I see that Ben Leslie wrote:

"I would prefer that seL4 focuses on providing a build system for building the kernel (and libsel4), and leave overall system building to the OS personality designer rather than dictating something for all seL4 based systems. Indeed this is the primary motivation of RFC-6."

Whatever people do, I would urge people to be very cautious about committing future development teams to arbitrary choices that canalize ('lock in') technical debt.

Not sure which of the agenda points gave that impression, but we're certainly not planning to do that. With respect to what Ben wrote in that RFC: seL4 (the kernel) does not and never has prescribed an overall build system for the rest of the system. In fact, Ben went on to prove that point by implementing the Microkit (formerly Core Platform), which would have been impossible if that was the case. Similarly, the proofs do not use the kernel build system either, yet have been working fine together with the kernel for more than 15 years over at least 3 entirely different kernel build system iterations. The most recent release of the kernel made it easier to export config and hardware information which can then be picked up in further builds. This should make using other build systems and other programming languages more convenient than it was before, but it has always been possible. User-level components that TS and the foundation provided have used cmake as their build system, and the CAmkES stack still does, because they have to use something and that is what people used when they wrote them. It's not mandated, it just was what that software stack provides hooks for and what tutorials etc were written for. As far as I can tell, this is mainly what people perceived as problematic and as mandating a specific build system. That is not entirely wrong (it certainly was the main suggested way of setting up a new project), but also not actually accurate. It certainly is not the case for the kernel itself. What the Microkit does better is making it easier to build components separately from each other, and explicitly demonstrating how to do that. I think that is a good direction and all makes sense to support, I'd just like to dispel this notion that this was in some way impossible before or forced on the user. Nothing really changed in the kernel build system to make this happen. Cheers, Gerwin