feat: add proofs as package

.github/workflows/nix.yaml

@@ -187,6 +187,22 @@ jobs:
           authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
       - name: Build
         run: nix build .#packages.x86_64-linux.guardonce --print-build-logs
+  x86_64-linux---packages---l4v:
+    name: x86_64-linux---packages---l4v
+    runs-on:
+      - ubuntu-latest
+    needs: []
+    steps:
+      - uses: actions/checkout@v4
+      - uses: cachix/install-nix-action@v25
+        with:
+          nix_path: nixpkgs=channel:nixos-unstable
+      - uses: cachix/cachix-action@v14
+        with:
+          name: dlr-ft
+          authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
+      - name: Build
+        run: nix build .#packages.x86_64-linux.l4v --print-build-logs
   x86_64-linux---packages---microkit-sdk:
     name: x86_64-linux---packages---microkit-sdk
     runs-on:

flake.nix

@@ -83,6 +83,12 @@
           camkes-deps = pkgs.python3Packages.camkes-deps;
 
 
+          #
+          ### Proofs
+          #
+          l4v = pkgs.l4v;
+
+
           #
           ### microkit(-sdk)
           #

overlay.nix

@@ -23,6 +23,8 @@ final: prev: {
   # https://android.googlesource.com/tools/repo
   fetchGoogleRepoTool = prev.callPackage pkgs/fetch-google-repo-tool.nix { };
 
+  # L4.verified
+  l4v = prev.callPackage pkgs/l4v.nix { };
 
   # microkit
   microkit-sdk = prev.callPackage pkgs/microkit-sdk.nix { };

pkgs/fetch-google-repo-tool.nix

@@ -15,6 +15,7 @@ lib.makeOverridable (
   , rev
   , name ? "source"
   , hash
+  , manifest ? "default.xml"
     # Problem
     #
     # `repo` allows for the manifest to just specify a branch, defaulting to the latest commit.
@@ -54,7 +55,7 @@ lib.makeOverridable (
       mkdir -- "$out" home
       export HOME="$PWD/home"
       cd "$out"
-      repo init --manifest-url=${escapeShellArg url} --no-repo-verify
+      repo init --manifest-url=${escapeShellArg url} --manifest-name=${escapeShellArg manifest} --no-repo-verify
 
       pushd .repo/manifests > /dev/null
       git fetch --all --tags

pkgs/l4v.nix

@@ -0,0 +1,76 @@
+{ stdenvNoCC
+, fetchGoogleRepoTool
+, which
+, isabelle
+, cmake
+, mlton
+, ninja
+, pkgsCross
+, python3Packages
+, openjdk_headless
+}:
+
+stdenvNoCC.mkDerivation (finalAttrs: {
+  pname = "L4.verified";
+  version = "1.11";
+
+  src = fetchGoogleRepoTool {
+    url = "https://github.com/seL4/verification-manifest";
+    rev = "2b434d1957eba420782f10f90e58f0b93ee3a4b7"; # 2024-10-11
+    manifest = "13.0.0.xml";
+    hash = "sha256-GTjofiun3TWlKdHRegWJNIitRzcZTGuSZQG1tmLpBg0=";
+  };
+  # src = fetchFromGitHub {
+  #   owner = "seL4";
+  #   repo = "l4v";
+  #   rev = "autocorres-${finalAttrs.version}";
+  #   hash = "sha256-Rv3lhx3CE7jW9P+nW3JiYZXnMmr+qFcAiK/TMziYxyE=";
+  # };
+
+  nativeBuildInputs = [
+    which
+    isabelle
+    mlton
+    openjdk_headless
+
+    cmake
+    ninja
+
+    # compilers
+    pkgsCross.aarch64-embedded.stdenv.cc.bintools.bintools
+    pkgsCross.aarch64-embedded.stdenv.cc.cc
+    pkgsCross.arm-embedded.stdenv.cc.bintools.bintools
+    pkgsCross.arm-embedded.stdenv.cc.cc
+    pkgsCross.riscv64-embedded.stdenv.cc.bintools.bintools
+    pkgsCross.riscv64-embedded.stdenv.cc.cc
+  ];
+
+  preUnpack = ''
+    HOME="$PWD/home"
+    mkdir --parent -- "$HOME"
+  '';
+
+  dontUseCmakeConfigure = true;
+
+  # preConfigure = ''
+  #   rm --force --recursive -- isabelle
+  #   ln --force --symbolic -- ${isabelle} isabelle
+  # '';
+
+  prePatch = ''
+    patchShebangs .
+  '';
+
+  preBuild = ''
+    cd l4v/proof
+  '';
+
+  buildPhase = ''
+    runHook preBuild
+
+    file /build/source/l4v/isabelle/bin/isabelle
+    make all
+
+    runHook postBuild
+  '';
+})