nix: wrap the microkit SDK as a Nix package

[r4v3n6101]

General

Build microkit-sdk including microkit-tool, docs (actually a manual), boards/configs as a Nix package using flakes.

What's done

• SDK and microkit command in the out output, with MICROKIT_SDK set in a wrapper;
• manual in a separate doc output;
• optional board and configuration selection.

The package uses build_sdk.py and derives the seL4 revision from https://github.com/seL4/microkit-manifest repo.

Why?

Just so you could run typing only nix run github:seL4#microkit.
UX for development process.

[Indanz]

This should be outside of the Microkit repo, just like microkit-manifest is outside of it. Maybe in microkit-manifest, maybe not, but definitely not here. You don't want to commit hashes and shas, that's unmaintainable, except if it happens automatically on release.

I think some other people already made Nix packages for seL4 and/or Microkit, but I don't know if they shared it. The problem is maintaining it, someone has to do that somewhere. Are you volunteering?

[midnightveil]

Yeah, I use Nix and for sDDF we have a package in the repo that downloads the SDK (building from source is too slow).

Package definitions should belong with the distro or dependendants, otherwise we must maintain every distro.

The intended distribution model is as an SDK (at least until we decide otherwise).

#420 I sketched out a distro package for Fedora. I think it would be neat for us to maintain dnf/apt/etc repos. But I'm not sure how useful it is if you need specific versions of the SDK for different projects and being tied to system-wide updates.

[r4v3n6101]

Thanks for the feedback.

I initially put this here because the repository already has Nix flakes support, and keeping the SDK package alongside seemed convenient to me.

I made the package read the seL4 revision from the XML in microkit-manifest repo, so updating it could be done through nix flake update microkit-manifest (assuming build dependencies remain unchanged for sure).

After considering your comments, I agree that keeping the package outside this repo makes sense. I’m willing to take this work to nixpkgs and maintain the package there.

If you decide to revisit packaging here in the future, I’d be very happy to help and pick up the work again. For now, I’m fine with leaving this PR on hold, marking it as Draft or even closing it.

[Indanz]

I initially put this here because the repository already has Nix flakes support, and keeping the SDK package alongside seemed convenient to me.

That shouldn't be there either I think. But what's there is at least self-contained I think, and if it's actively used, then it's maintained by someone. It says it's "A flake for building microkit", that being here makes some sense, but it's unclear to me how your new thing differs exactly, as it also seems to build Microkit instead of using the SDK. And if you do use the SDK, you don't need the microkit repo and then this is the wrong place.

So the thing you added seems to handle a weird corner case where you want to use a specific SDK and build it from source, but then be able to do local modifications in only Microkit?

I made the package read the seL4 revision from the XML in microkit-manifest repo, so updating it could be done through nix flake update microkit-manifest (assuming build dependencies remain unchanged for sure).

But microkit-manifest has references to this repo, so you just introduced a circular dependency.

If you decide to revisit packaging here in the future, I’d be very happy to help and pick up the work again. For now, I’m fine with leaving this PR on hold, marking it as Draft or even closing it.

I'm fine if you tweak the existing Flake to add what you want (a package instead of a development shell?), but I don't think it should have hard-coded references to microkit-manifest or dependencies.

All in all it does sound that you mostly want a Nix version of microkit-manifest, that's probably best in its own repository like microkit-manifest is.

@wucke13, you're the Nix expert, what would you recommend?

[midnightveil]

(Yes, I actively use and maintain the Nix flake for building Microkit, and it is used in CI. Once inside that development environment it's just one command to build)

You don't even need a nix version of Microkit-manifest really - nix can just shell out to repo to fetch dependencies.

In a distro environment, using our flake doesn't make sense since it wants a consistent set of build dependencies. In a user environment it makes more sense to distribute the prebuilt .tar.gz files (like we do for sDDF: https://github.com/au-ts/sddf/blob/43d5574d0939418b20b74d8fdd2637b1cd4a1c5d/flake.nix#L118), and for developing Microkit itself it makes no sense to use a Nix package because it always builds clean which takes 30 minutes.

Unless there's some other use case I can't think of?

[Indanz]

Unless there's some other use case I can't think of?

To me the obvious use case would be to rebuild it with a custom kernel configuration, either because they want different seL4 config decisions, or add a KernelCustomDTSOverlay to tweak RAM/UARTS etc. But didn't Ivan recently add support for custom seL4 kernel binaries? Yes: --override-kernel. So with that, this makes even less sense.

@r4v3n6101, is --override-kernel what you have been missing, or do you really want just a source build of the SDK and package it as a Nix package for other reasons? (e.g. Nix based reproducible build.)

[wucke13]

I think some other people already made Nix packages for seL4 and/or Microkit, but I don't know if they shared it.

Hi 👋, https://github.com/DLR-FT/seL4-nix-utils/ is fairly comprehensive (but due to time constraints usually lagging behind one or two minor releases).

Yeah, I use Nix and for sDDF we have a package in the repo that downloads the SDK (building from source is too slow).

Might I ask why you have to rebuild the sdk when you change a driver? The SDK should be first, hence you build it once and be done with it.

Other than that, yes, the SDK building process of microkit is rather slow, in part due to being sequential; I think this is by design: the sdk is build seldomly; and sequential builds are easier to debug.

The intended distribution model is as an SDK (at least until we decide otherwise).

Please keep it that way, this is by far the easiest deployment model. Download a tar file full of statically linked binaries, prebuilt object code and a demo Makefil, done. This is peak packaging 😄. Practical, simple, universal.

After considering your comments, I agree that keeping the package outside this repo makes sense. I’m willing to take this work to nixpkgs and maintain the package there.

Hit me up if you need a review. Also, this flake uses an external Rust toolchain, if you want to learn how to do it with in-house means, checkout my packaging of microkit. You will not get something upstreamed in nixpkgs that uses oxalica's overlay.

That shouldn't be there either I think. But what's there is at least self-contained I think, and if it's actively used, then it's maintained by someone. It says it's "A flake for building microkit", that being here makes some sense, but it's unclear to me how your new thing differs exactly, as it also seems to build Microkit instead of using the SDK. And if you do use the SDK, you don't need the microkit repo and then this is the wrong place.

I gently disagree. If microkit, the repo, would expose a Nix package which builds the sdk, then for example for a feature branch you could litterally tell someone to nix shell github:seL4/microki/<branch-name/commit hash>#microkit-sdk and they would be in a devshell with the exact binary that you would also build on your machine, that is built by CI, etc...

So, there definitely is some merit to having it directly in the repo.

However, hop via the manifest repo is quite ugly in that sense. I would prefer (and this is also what I'm doing in my repo) hardcoding the commit hash of the seL4 kernel. That makes the package truly self contained (at the cost of duplicating what is in the manifest).

So the thing you added seems to handle a weird corner case where you want to use a specific SDK and build it from source, but then be able to do local modifications in only Microkit?

It's not an XOR. If you have a packge microkit-sdk, you can nix shell ...#microkit-sdk to get a shell with the fully build sdk available. Or you can nix develop ...#microkit-sdk to get a development shell with all tools required to build the sdk itself. So a single package can both serve as its final output, or the tool environment to interactively tinker with the build of the package itself.

For this reason I would actually like to see the microkit flake to expose only a package, instead of only a devShell, because the former automatically also becomes a devShell. But I do understand that this is a touch subject, and not everyone is keen on either having a reference to the -manifest repo or duplicating the seL4 commit id and tarball hash in the nix expressions.

So take my point of view purely as a hypothetical; I'm not pushing for this; I would just prefer it all things equal.

I'm fine if you tweak the existing Flake to add what you want (a package instead of a development shell?), but I don't think it should have hard-coded references to microkit-manifest or dependencies.

IMHO that is fundamentally impossible. The sdk package would need seL4, so it needs to know which specific version. There is no way to get that except for either one of these:

• submodule with seL4 kernel
• commit hash and tarball hash somwhere in this repo
• reference to microkit-manifest repo

My understanding is, that all three are disliked by the seL4 community...

All in all it does sound that you mostly want a Nix version of microkit-manifest, that's probably best in its own repository like microkit-manifest is.

Technically, this could be made part of the -manifest repo itself. There everything is local, and the manifest repo anyhow needs to be tagged with a version for each release; so automatically via that tag then also a nix expression would be available for each release. Technically, I think, that would be a compromise worth considering. Whether consensus for this could be found, well, that is not for me to answer 😄

You don't even need a nix version of Microkit-manifest really - nix can just shell out to repo to fetch dependencies.

Shameless self-plug: https://github.com/DLR-FT/seL4-nix-utils/blob/main/pkgs/fetch-google-repo-tool.nix

---

I think, in particular for microkit, there is not a very strong use-case for Nix. The SDK is not, well, elegant, but it is practical, quick, just perfectly adequate.

For other things, like the kernel itself, it makes more sense IMHO. Nix excels in letting downstream consumers override aspects of the upstream dependencies. This is also where we use the seL4-nix-utils most. But, all this makes only sense if technical ownership lays with someone from the inner circle; otherwise this is a frustration potential. With the devShell, this ownership seems to lay with @midnightveil . Would she be interested in stepping up from devShell to actual package, at the cost of one of the compromises I elaborated above?

I'm open for discussion and also willing to hop on a call for anything Nix + seL4, but no need to push this more than desired by the inner circle.

Take care 🙂

[midnightveil]

Yeah, I'm really not interested in having an extra source of truth for the seL4 version. We only just finally got back to having only one with the repo manifest :)

(unfortunately)

Might I ask why you have to rebuild the sdk when you change a driver? The SDK should be first, hence you build it once and be done with it.

We don't, it's just that if the first thing one had to do to use sDDF was compile Microkit it would be extremely unpleasant. So I'm opposed to binary-cache-less builds.

Other than that, yes, the SDK building process of microkit is rather slow, in part due to being sequential; I think this is by design: the sdk is build seldomly; and sequential builds are easier to debug.

Yeah. I want to speed it up. I have a PR which #479 but it didn't actually help much. I think something like the output of --multiline-with-logs from nix build would be useful if we went that way - at this point I'm not convinced it's worth the annoyance of making Nix required to build Microkit to use that.

What would help if we didn't have to rebuild most of rust-sel4 once per platform, it's the really slow part. 6 configs for 3 architectures (or maybe a few variants) is much more manageable than 6 configs for 3 boards.

I have some other local patches to hide a local of seL4 config options and make it so the only differences in libsel4 occurs due to actually important things (e.g. s2_start_l1 or debug configs etc) which would help reduce (strip plat-specifics then collate by general option sets). Butttt....

It looks like a generic AArch64 seL4 is wanted and so that will be noce too.---

(We should probably consider using the nixpkgs rust toolchain instead of oxalica.. but anyway)

[r4v3n6101]

I’d actually forgotten about nix develop! 😅
It seems like a nice way to get the build dependencies and go through the build step by step: unpack the sources (via unpackPhase), make changes and apply patches if needed, then configure and build (configurePhase and buildPhase). I like @wucke13 ’s suggestion even more than the current devShell, though keeping the existing shell for backwards compatibility would still make sense, right?

Regarding the long build times, I can’t really help with that yet, since I’m not familiar with the seL4 team’s build or dev process. One thing might be relevant to @midnightveil ’s point and it is that I made boards and configs configurable, so you can limit the build to what you need, for example:

package.override { boards = [ "rpi4b_1gb" ]; }

Personally, I’m using Microkit SDK for self-taught of a seL4 development process. I haven’t needed to modify Microkit itself yet, and all I used is the microkit tool. So my use case might not be very representative. Reading your comments, I’m realizing that the usual workflow with the SDK may be different from what I had.

As I’m still fairly new to the seL4 ecosystem, I’d really appreciate your suggestions on what direction would make sense for this PR and how it could be moved forward.