next seL4 TSC meeting on Thu 25 Jul
The Technical Steering Committee (TSC) of the seL4 Foundation will hold its next public meting on: - Sydney: Thu, 25 Jul, 4pm - Central Europe: Thu, 25 Jul, 8am - US West Coast (LA/SF): Thu, 25 Jul, 0:00h See also the seL4 calendar feed available from here: https://sel4.systems/contact/home.pml The meeting is by Zoom, and you can join from here: https://unsw.zoom.us/j/89949317341?pwd=JSC976ciVYmbDJByjSFH0chh78sCsg.1 Anyone interested can join the meeting and listen to the discussion and request to speak, which will be granted if time permits. Only TSC members can vote. The seL4 code of conduct applies to the meeting [1]. The agenda for the meeting so far is: - action items from last meeting - discuss new FPU RFC: https://github.com/seL4/rfcs/pull/26 - hear about progress on PMU, budget limit, device driver framework - make decision on old RFC-4: https://github.com/seL4/rfcs/pull/12 - any feedback on GitHub RFC implementation - bump version of cmake-format (will break current formatting) to reduce python dependency hell If there are other items that I missed or you think should be on the agenda, please let me know. If we can't get to an item this time, we can still schedule another meeting. Cheers, Gerwin (TSC chair) [1]: https://docs.sel4.systems/processes/conduct.html
On Fri, Jul 12, 2024 at 6:19 AM Gerwin Klein via Devel <devel@sel4.systems> wrote:
The Technical Steering Committee (TSC) of the seL4 Foundation will hold its next public meting on:
s/meting/meeting, looking back I notice the same typo me[e]ting in the previous TSC announcement. So presumably this typo needs to be fixed in a meeting announcement template.
- bump version of cmake-format (will break current formatting) to reduce python dependency hell
If there are other items that I missed or you think should be on the agenda, please let me know. If we can't get to an item this time, we can still schedule another meeting.
This item reminded me that in spring of next year end of standard support for ubuntu 20.4, along with that there are some versions which would be nice to bump, (I'm particularly interested in bumping cmake itself). I at least hope to have a look into what bumping that version enables. But curious if this could or should be done as part of a more coordinated effort to bump dependencies across the board at that time.
On Tue, Jul 23, 2024 at 3:53 AM Gerwin Klein <kleing@unsw.edu.au> wrote:
After reading the agenda which references EOL in particular, I should probably clarify my remarks as only now do I realize that the Ubuntu lifecycle timeline has changed since the last time host system requirements for building seL4 were updated. From what I gather starting earlier this year they now have paid 10 & 12 year Pro and Extended support in addition to the previous 5 year LTS window ("Standard support"). My hope is we can essentially ignore these new tiers of paid support and stick with the 5 year LTS window, updating host system requirements from 20.04 after 2025 which is before its extended support window officially ends in 2032.
Agenda updated with feedback from the mailing list and GitHub: - Action items from last meeting - Style and CI: - should we mandate rustfmt in style guide and CI? (code formatting, now that there is more Rust code) - should we mandate Rust clippy in CI? (Rust linter) - should we mandate or allow a Python linter in CI? Which one? (Options: ruff, mypy, flake8, pylint) - what level of lint failures do we tolerate? - bump version of cmake-format (will break current formatting) to reduce python dependency hell - should we bump the min version of cmake and when? (E.g. for EOL of Ubuntu 20.04) - RFCs: - discuss new FPU RFC: https://github.com/seL4/rfcs/pull/26 - hear about progress on PMU, budget limit, device driver framework - make decision on old RFC-4: https://github.com/seL4/rfcs/pull/12 - any feedback on GitHub RFC implementation Cheers, Gerwin
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. BobTrower On Mon, Jul 22, 2024 at 11:59 PM Gerwin Klein via Devel <devel@sel4.systems> wrote:
-- Bob Trower --- From Gmail webmail account. ---
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
participants (3)
-
Bob Trower -
Gerwin Klein -
Matt Rice