On 1/22/20, Heiser, Gernot (Data61, Kensington NSW) <gernot.hei...@data61.csiro.au> wrote: > > However, there is always going to be some in-house experimental code, > especially student work, that never makes it out. >
That's exactly the kind of thing that I think might be a problem for UX/RT because it means that the development process isn't truly community-based. UX/RT won't have any such thing as "in-house code" (except for code that hasn't yet been committed). All development will be public (except security fixes under temporary embargoes). I want UX/RT to be as easy as possible to contribute to, and that should include contributing to the kernel (which be much less necessary in general with a microkernel OS, but for stuff like platform support it will still be necessary). Even just having a copyright-assignment-equivalent CLA would very likely scare off a lot of companies (and some individuals) from contributing. Things are already difficult enough in the industry at large for alternative OSes, and I don't want excessive barriers to contribution to be the thing that keeps UX/RT from succeeding. > > We’re doing our best to make things more open, but we have very limited > resources, resulting at times in a divergence between intent and reality. > The forthcoming seL4 Foundation should help. > > Forking is a very bad idea. If you modify the kernel, you’re breaking > verification, and it’s no longer seL4. And it will be one job of the > Foundation to ensure that only things that *are* seL4 are called seL4. > I really don't want to fork it unless I have to (and if I did I would rename my fork of course). I just know that my priorities for UX/RT (a general-purpose "better Linux than Linux" OS for production use) seem to be rather different from the those of the seL4 developers (research on static deeply embedded systems), and the development process isn't fully open, and that could possibly lead to differences requiring a fork in the future. On 1/22/20, Heiser, Gernot (Data61, Kensington NSW) <gernot.hei...@data61.csiro.au> wrote: > PRs that don’t affect verification will be accepted subject to standard > quality control (and availability of a CLA). These are not frequent, but > happen. Typically they are platform ports. > > One of the things we’d like to set up is a way for developers to check this > for themselves, which should certainly help contributions. Not sure when > this will be ready. > This does sound promising, but it still might not be quite open enough for my liking. Ideally UX/RT should be at least as easy to contribute to as Linux. > The same applies, in principle, to PRs that come with proof updates. We > haven’t seen one of these yet. > > The bar will be higher if the change affects kernel semantics (even if > accompanied by proof), as we need to ensure that the design stays clean and > principled. > That's fair. I don't plan to accept changes that go against the design philosophy with UX/RT either. _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
