> On 23 Jul 2024, at 20:41, Bob Trower <btro...@gmail.com> 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
_______________________________________________
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems
