nix: refactor flake.nix for readability and easier testing

Refactoring some let binging into nix packages make it easier for testing. For example, we can now test the CBMC dependencies by running, `nix build .#cbmc`, and check the built dependencies in `results/bin/` The `litani` derivation is therefore needed to be adjusted so that the python runtime dependencies can be found. Signed-off-by: Thing-han, Lim <[email protected]>
pq-code-package · Nov 8, 2024 · 9072d07 · 9072d07
1 parent 998e425
commit 9072d07
Show file tree

Hide file tree

Showing 3 changed files with 109 additions and 115 deletions.
diff --git a/cbmc/default.nix b/cbmc/default.nix
@@ -1,32 +1,40 @@
 # SPDX-License-Identifier: Apache-2.0
-{ cbmc
+{ buildEnv
+, cbmc
 , fetchFromGitHub
 , callPackage
 , bitwuzla
 , ninja
+, cadical
 }:
-builtins.attrValues {
-  cbmc = cbmc.overrideAttrs (old: rec {
-    version = "6.3.1"; # remember to adjust this in ../flake.nix too
-    src = fetchFromGitHub {
-      owner = "diffblue";
-      repo = old.pname;
-      rev = "${old.pname}-${version}";
-      hash = "sha256-y3avPsVxtxSV+WB8TBbvnaNZ4WZltGRTcD+GPwTlp2E=";
-    };
-    patches = [
-      ./0001-Do-not-download-sources-in-cmake.patch
-    ];
-  });
-  litani = callPackage ./litani.nix { }; # 1.29.0
-  cbmc-viewer = callPackage ./cbmc-viewer.nix { }; # 3.9
 
-  z3 = callPackage ./z3.nix {
-    version = "4.13.3";
-    sha256 = "sha256-odwalnF00SI+sJGHdIIv4KapFcfVVKiQ22HFhXYtSvA=";
-  };
+buildEnv {
+  name = "pqcp-cbmc";
+  paths =
+    builtins.attrValues {
+      cbmc = cbmc.overrideAttrs (old: rec {
+        version = "6.3.1"; # remember to adjust this in ../flake.nix too
+        src = fetchFromGitHub {
+          owner = "diffblue";
+          repo = old.pname;
+          rev = "${old.pname}-${version}";
+          hash = "sha256-y3avPsVxtxSV+WB8TBbvnaNZ4WZltGRTcD+GPwTlp2E=";
+        };
+        patches = [
+          ./0001-Do-not-download-sources-in-cmake.patch
+        ];
+      });
+      litani = callPackage ./litani.nix { }; # 1.29.0
+      cbmc-viewer = callPackage ./cbmc-viewer.nix { }; # 3.9
+
+      z3 = callPackage ./z3.nix {
+        version = "4.13.3";
+        sha256 = "sha256-odwalnF00SI+sJGHdIIv4KapFcfVVKiQ22HFhXYtSvA=";
+      };
 
-  inherit
-    bitwuzla# 0.6.0
-    ninja; # 1.11.1
+      inherit
+        cadical#1.9.5
+        bitwuzla# 0.6.0
+        ninja; # 1.11.1
+    };
 }
diff --git a/cbmc/litani.nix b/cbmc/litani.nix
@@ -2,6 +2,7 @@
 
 { stdenvNoCC
 , fetchFromGitHub
+, python3Packages
 }:
 
 stdenvNoCC.mkDerivation {
@@ -16,12 +17,17 @@ stdenvNoCC.mkDerivation {
   dontConfigure = true;
   installPhase = ''
     mkdir -p $out/bin
-    cp litani $out/bin
+    install -Dm755 litani $out/bin/litani
     cp -r lib $out/bin
     cp -r templates $out/bin
   '';
   dontStrip = true;
   noAuditTmpdir = true;
+  propagatedBuildInputs = [
+    (python3Packages.python.withPackages
+      (pythonPackages: [ pythonPackages.jinja2 ])
+    )
+  ];
 
   meta = {
     description = "Litani metabuild system";

diff --git a/flake.nix b/flake.nix
@@ -17,97 +17,45 @@
     flake-parts.lib.mkFlake { inherit inputs; } {
       imports = [ ];
       systems = [ "x86_64-linux" "aarch64-linux" "aarch64-darwin" "x86_64-darwin" ];
-      perSystem = { pkgs, system, inputs', ... }:
+      perSystem = { config, pkgs, system, inputs', ... }:
         let
-          cbmcpkg = pkgs.callPackage ./cbmc { }; # 6.3.1
-          linters = builtins.attrValues {
-            clang-tools = pkgs.clang-tools.overrideAttrs {
-              unwrapped = pkgs.llvmPackages_17.clang-unwrapped;
-            };
-
-            inherit (pkgs)
-              nixpkgs-fmt
-              shfmt;
-
-            inherit (pkgs.python3Packages)
-              black;
-          };
-
-          glibc-join = p: p.buildPackages.symlinkJoin {
-            name = "glibc-join";
-            paths = [ p.glibc p.glibc.static ];
-          };
-
-          wrap-gcc = p: p.buildPackages.wrapCCWith {
-            cc = p.buildPackages.gcc13.cc;
-            bintools = p.buildPackages.wrapBintoolsWith {
-              bintools = p.buildPackages.binutils-unwrapped;
-              libc = glibc-join p;
-            };
-          };
-
-          x86_64-gcc = wrap-gcc pkgs.pkgsCross.gnu64;
-          aarch64-gcc = wrap-gcc pkgs.pkgsCross.aarch64-multiplatform;
-
           default_gcc = { cross ? true }:
             let
-              gcc =
-                if pkgs.stdenv.isDarwin
-                then [ ]
-                else
-                  if cross
-                  then
-                    if pkgs.stdenv.isAarch64
-                    then [ x86_64-gcc aarch64-gcc ]
-                    else [ aarch64-gcc x86_64-gcc ]
-                  else
-                    if pkgs.stdenv.isAarch64
-                    then [ aarch64-gcc ]
-                    else [ x86_64-gcc ];
-            in
-            gcc;
-
-          base =
-            builtins.attrValues {
-              inherit (pkgs.python3Packages)
-                pyyaml
-                python
-                click;
-            };
+              glibc-join = p: p.buildPackages.symlinkJoin {
+                name = "glibc-join";
+                paths = [ p.glibc p.glibc.static ];
+              };
+
+              wrap-gcc = p: p.buildPackages.wrapCCWith {
+                cc = p.buildPackages.gcc13.cc;
+                bintools = p.buildPackages.wrapBintoolsWith {
+                  bintools = p.buildPackages.binutils-unwrapped;
+                  libc = glibc-join p;
+                };
+              };
 
-          # cross is for determining whether to install the cross toolchain or not
+              x86_64-gcc = wrap-gcc pkgs.pkgsCross.gnu64;
+              aarch64-gcc = wrap-gcc pkgs.pkgsCross.aarch64-multiplatform;
+            in
+            if pkgs.stdenv.isDarwin
+            then [ ]
+            else if cross
+            then if pkgs.stdenv.isAarch64
+            then [ x86_64-gcc aarch64-gcc ]
+            else [ aarch64-gcc x86_64-gcc ]
+            else if pkgs.stdenv.isAarch64
+            then [ aarch64-gcc ]
+            else [ x86_64-gcc ];
+
+          # cross is for determining whether to install the cross toolchain or not 
           core = { cross ? true }:
-            default_gcc { cross = cross; } ++ base ++
+            [ (default_gcc { cross = cross; }) ] ++
             builtins.attrValues {
+              inherit (config.packages) base;
               inherit (pkgs)
                 qemu; # 8.2.4
             };
 
-          core_gcc48 = base ++ builtins.attrValues {
-            inherit (pkgs)
-              gcc48; #4.8
-          };
-
-          core_gcc49 = base ++ builtins.attrValues {
-            inherit (pkgs)
-              gcc49; #4.9
-          };
-
-          core_gcc7 = base ++ builtins.attrValues {
-            inherit (pkgs)
-              gcc7; #7
-          };
-
-          core_gcc11 = base ++ builtins.attrValues {
-            inherit (pkgs)
-              gcc11; #11
-          };
-
-          core_clang18 = base ++ builtins.attrValues {
-            inherit (pkgs)
-              clang_18; #18
-          };
-
           wrapShell = mkShell: attrs:
             mkShell (attrs // {
               shellHook = ''
@@ -124,10 +72,42 @@
             ];
           };
 
+          packages.linters = pkgs.buildEnv
+            {
+              name = "pqcp-linters";
+              paths = builtins.attrValues {
+                clang-tools = pkgs.clang-tools.overrideAttrs {
+                  unwrapped = pkgs.llvmPackages_17.clang-unwrapped;
+                };
+
+                inherit (pkgs)
+                  nixpkgs-fmt
+                  shfmt;
+
+                inherit (pkgs.python3Packages)
+                  black;
+              };
+            };
+
+          packages.cbmc = pkgs.callPackage ./cbmc { }; # 6.3.1
+
+          packages.base = pkgs.buildEnv {
+            name = "pqcp-base";
+            paths = builtins.attrValues {
+              inherit (pkgs.python3Packages)
+                pyyaml
+                python
+                click;
+            };
+          };
+
+
           devShells.default = wrapShell pkgs.mkShellNoCC {
-            packages = core { } ++ linters ++ cbmcpkg ++
+            packages =
+              core { } ++
               builtins.attrValues
                 {
+                  inherit (config.packages) linters cbmc;
                   inherit (pkgs)
                     direnv
                     nix-direnv;
@@ -136,15 +116,15 @@
 
           devShells.ci = wrapShell pkgs.mkShellNoCC { packages = core { cross = false; }; };
           devShells.ci-cross = wrapShell pkgs.mkShellNoCC { packages = core { }; };
-          devShells.ci-cbmc = wrapShell pkgs.mkShellNoCC { packages = core { cross = false; } ++ cbmcpkg; };
-          devShells.ci-cbmc-cross = wrapShell pkgs.mkShellNoCC { packages = core { } ++ cbmcpkg; };
-          devShells.ci-linter = wrapShell pkgs.mkShellNoCC { packages = linters; };
-
-          devShells.ci_clang18 = wrapShell pkgs.mkShellNoCC { packages = core_clang18; };
-          devShells.ci_gcc48 = wrapShell pkgs.mkShellNoCC { packages = core_gcc48; };
-          devShells.ci_gcc49 = wrapShell pkgs.mkShellNoCC { packages = core_gcc49; };
-          devShells.ci_gcc7 = wrapShell pkgs.mkShellNoCC { packages = core_gcc7; };
-          devShells.ci_gcc11 = wrapShell pkgs.mkShellNoCC { packages = core_gcc11; };
+          devShells.ci-cbmc = wrapShell pkgs.mkShellNoCC { packages = core { cross = false; } ++ [ config.packages.cbmc ]; };
+          devShells.ci-cbmc-cross = wrapShell pkgs.mkShellNoCC { packages = core { } ++ [ config.packages.cbmc ]; };
+          devShells.ci-linter = wrapShell pkgs.mkShellNoCC { packages = [ config.packages.linters ]; };
+
+          devShells.ci_clang18 = wrapShell pkgs.mkShellNoCC { packages = [ config.packages.base pkgs.clang_18 ]; };
+          devShells.ci_gcc48 = wrapShell pkgs.mkShellNoCC { packages = [ config.packages.base pkgs.gcc48 ]; };
+          devShells.ci_gcc49 = wrapShell pkgs.mkShellNoCC { packages = [ config.packages.base pkgs.gcc49 ]; };
+          devShells.ci_gcc7 = wrapShell pkgs.mkShellNoCC { packages = [ config.packages.base pkgs.gcc7 ]; };
+          devShells.ci_gcc11 = wrapShell pkgs.mkShellNoCC { packages = [ config.packages.base pkgs.gcc11 ]; };
         };
       flake = {
         # The usual flake attributes can be defined here, including system-