Nix refactoring (#4500)

This PR is a preparatory of the K Nix build code that will allow us to further simplify downstream packages. Roughly, the steps taken here are: - Move some definitions from the set of K flake output packages into the K overlay; this lets us reference `k` directly from semantics that use the overlay, rather than `k-framework.${pkgs.system}.packages.k` as we do now. - Pull the bulk of the Pyk flake out into a standalone overlay expression; the actual build code in that overlay is identical. - Re-export Pyk from the K overlay using the extracted Pyk overlay. - Test both ways of referencing Pyk (via subdirectory flake, or via K attribute) in CI. Once this PR is merged, the next step will be to replace usages of Pyk as a standalone flake in downstream code to instead point at the corresponding K attribute. This simplifies version-bump and Nix input management in those projects. I have tested this against the WASM semantics downstream, and the suggested new method for referencing Pyk successfully builds there. --------- Co-authored-by: rv-jenkins <[email protected]>
runtimeverification · Jul 10, 2024 · 5e25c5b · 5e25c5b
1 parent 4a5587c
commit 5e25c5b
Show file tree

Hide file tree

Showing 5 changed files with 192 additions and 57 deletions.
diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
@@ -157,9 +157,6 @@ jobs:
     strategy:
       matrix:
         os: [ubuntu-latest, macos-14]
-    defaults:
-      run:
-        working-directory: ./pyk
     runs-on: ${{ matrix.os }}
     steps:
       - name: 'Check out code'
@@ -178,8 +175,10 @@ jobs:
           name: k-framework
           authToken: '${{ secrets.CACHIX_PUBLIC_TOKEN }}'
           skipPush: true
-      - name: 'Build pyk'
+      - name: 'Build original pyk flake'
         run: GC_DONT_GC=1 nix build --print-build-logs .#pyk-python310
+      - name: 'Build pyk provided by K'
+        run: GC_DONT_GC=1 nix build --print-build-logs ./pyk#pyk-python310
 
 
   compile-nix-flake:

diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -8,22 +8,36 @@
       inputs.nixpkgs.follows = "llvm-backend/nixpkgs";
     };
 
+    poetry2nix = {
+      url =
+        "github:nix-community/poetry2nix/626111646fe236cb1ddc8191a48c75e072a82b7c";
+      inputs.nixpkgs.follows = "llvm-backend/nixpkgs";
+    };
+
     nixpkgs.follows = "llvm-backend/nixpkgs";
     rv-utils.follows = "llvm-backend/rv-utils";
     flake-utils.follows = "llvm-backend/utils";
   };
 
   outputs = { self, nixpkgs, flake-utils, rv-utils, haskell-backend
-    , llvm-backend }:
+    , llvm-backend, poetry2nix }:
     let
       allOverlays = [
         (_: _: {
           llvm-version = 17;
           llvm-backend-build-type = "Release";
         })
+
         llvm-backend.overlays.default
+
         haskell-backend.overlays.z3
         haskell-backend.overlays.integration-tests
+
+        (import ./nix/pyk-overlay.nix {
+          inherit poetry2nix;
+          projectDir = ./pyk;
+        })
+
         (final: prev:
           let
             k-version =
@@ -54,7 +68,22 @@
             # this version of maven from nixpkgs 23.11. we can remove this version of maven once our nixpkgs catches up
             maven = prev.callPackage ./nix/maven.nix { };
 
-            k-framework = { haskell-backend-bins, llvm-kompile-libs }:
+            haskell-backend-bins = prev.symlinkJoin {
+              name = "kore-${haskell-backend.sourceInfo.shortRev or "local"}";
+              paths = let p = haskell-backend.packages.${prev.system};
+              in [
+                p.kore-exec
+                p.kore-match-disjunction
+                p.kore-parser
+                p.kore-repl
+                p.kore-rpc
+                p.kore-rpc-booster
+                p.kore-rpc-client
+                p.booster-dev
+              ];
+            };
+
+            mk-k-framework = { haskell-backend-bins, llvm-kompile-libs }:
               prev.callPackage ./nix/k.nix {
                 mvnHash = "sha256-HkAwMZq2vvrnEgT1Ksoxb5YnQ8+CMQdB2Sd/nR0OttU=";
                 manualMvnArtifacts = [
@@ -83,6 +112,15 @@
                 version = "${k-version}-${self.rev or "dirty"}";
                 inherit llvm-kompile-libs;
               };
+
+            k = final.mk-k-framework {
+              inherit (final) haskell-backend-bins;
+              llvm-kompile-libs = with prev; {
+                procps = [ "-I${procps}/include" "-L${procps}/lib" ];
+                openssl = [ "-I${openssl.dev}/include" "-L${openssl.out}/lib" ];
+                secp256k1 = [ "-I${secp256k1}/include" "-L${secp256k1}/lib" ];
+              };
+            };
           })
       ];
     in flake-utils.lib.eachSystem [
@@ -105,34 +143,12 @@
               ++ allOverlays;
           };
 
-        haskell-backend-bins = pkgs.symlinkJoin {
-          name = "kore-${haskell-backend.sourceInfo.shortRev or "local"}";
-          paths = let p = haskell-backend.packages.${system};
-          in [
-            p.kore-exec
-            p.kore-match-disjunction
-            p.kore-parser
-            p.kore-repl
-            p.kore-rpc
-            p.kore-rpc-booster
-            p.kore-rpc-client
-            p.booster-dev
-          ];
-        };
-
       in rec {
         k-version =
           pkgs.lib.removeSuffix "\n" (builtins.readFile ./package/version);
 
         packages = rec {
-          k = pkgs.k-framework {
-            inherit haskell-backend-bins;
-            llvm-kompile-libs = with pkgs; {
-              procps = [ "-I${procps}/include" "-L${procps}/lib" ];
-              openssl = [ "-I${openssl.dev}/include" "-L${openssl.out}/lib" ];
-              secp256k1 = [ "-I${secp256k1}/include" "-L${secp256k1}/lib" ];
-            };
-          };
+          inherit (pkgs) k pyk pyk-python310 pyk-python311;
 
           check-submodules = rv-utils.lib.check-submodules pkgs {
             inherit llvm-backend haskell-backend;
@@ -195,14 +211,13 @@
         };
         defaultPackage = packages.k;
         devShells.kore-integration-tests = pkgs.kore-tests (pkgs.k-framework {
-          inherit haskell-backend-bins;
+          inherit (pkgs) haskell-backend-bins;
           llvm-kompile-libs = { };
         });
       }) // {
         overlays.llvm-backend = llvm-backend.overlays.default;
         overlays.z3 = haskell-backend.overlays.z3;
 
         overlay = nixpkgs.lib.composeManyExtensions allOverlays;
-
       };
 }
diff --git a/nix/pyk-overlay.nix b/nix/pyk-overlay.nix
@@ -0,0 +1,27 @@
+{ poetry2nix, projectDir }:
+(final: prev:
+  let
+    mkPyk = python:
+      let
+        p2n = poetry2nix.lib.mkPoetry2Nix { pkgs = prev; };
+      in p2n.mkPoetryApplication {
+        inherit projectDir;
+        python = python;
+        groups = [ ];
+        # We remove `"dev"` from `checkGroups`, so that poetry2nix does not try to resolve dev dependencies.
+        checkGroups = [ ];
+        overrides = p2n.defaultPoetryOverrides.extend
+          (self: super: {
+            pygments = super.pygments.overridePythonAttrs
+            (
+              old: {
+                buildInputs = (old.buildInputs or [ ]) ++ [ super.hatchling ];
+              }
+            );
+          });
+      };
+  in rec {
+    pyk = pyk-python310;
+    pyk-python310 = mkPyk prev.python310;
+    pyk-python311 = mkPyk prev.python311;
+  })
diff --git a/pyk/flake.nix b/pyk/flake.nix
@@ -15,32 +15,10 @@
   outputs = { self, nixpkgs, flake-utils, rv-utils, poetry2nix }:
     {
       # Nixpkgs overlay providing the application
-      overlay = final: prev:
-        let
-          mkPyk = python:
-            let
-              p2n = poetry2nix.lib.mkPoetry2Nix { pkgs = prev; };
-            in p2n.mkPoetryApplication {
-              python = python;
-              projectDir = ./.;
-              groups = [ ];
-              # We remove `"dev"` from `checkGroups`, so that poetry2nix does not try to resolve dev dependencies.
-              checkGroups = [ ];
-              overrides = p2n.defaultPoetryOverrides.extend
-                (self: super: {
-                  pygments = super.pygments.overridePythonAttrs
-                  (
-                    old: {
-                      buildInputs = (old.buildInputs or [ ]) ++ [ super.hatchling ];
-                    }
-                  );
-                });
-            };
-        in rec {
-          pyk = pyk-python310;
-          pyk-python310 = mkPyk prev.python310;
-          pyk-python311 = mkPyk prev.python311;
-        };
+      overlay = (import ../nix/pyk-overlay.nix {
+        inherit poetry2nix;
+        projectDir = ./.;
+      });
     } // (flake-utils.lib.eachDefaultSystem (system:
       let
         pkgs = import nixpkgs {