Revert "Remove mavenix build" (#3805)

Reverts #3802

This appears to have broken the K CI

.github/workflows/test-pr.yml

@@ -51,6 +51,49 @@ jobs:
           version: 1.18.1
           args: "--dry-run --set-exit-if-changed"
 
+  nix-maven:
+    name: 'Nix: Maven'
+    runs-on: ubuntu-20.04
+    needs: format-check
+    steps:
+
+      - name: 'Check out code, set up Git'
+        uses: actions/checkout@v3
+        with:
+          submodules: recursive
+          fetch-depth: 0
+      - run: |
+          git config user.name devops
+          git config user.email [email protected]
+
+      - name: 'Install Nix'
+        uses: cachix/install-nix-action@v22
+        with:
+          install_url: https://releases.nixos.org/nix/nix-2.13.3/install
+          extra_nix_config: |
+            access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
+            substituters = http://cache.nixos.org https://hydra.iohk.io
+            trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ=
+
+      - name: 'Install Cachix'
+        uses: cachix/cachix-action@v12
+        with:
+          name: k-framework
+          authToken: '${{ secrets.CACHIX_PUBLIC_TOKEN }}'
+          skipPush: true
+
+      - name: 'Update Maven dependencies, push changes'
+        run: |
+          set -x
+          git checkout ${GITHUB_HEAD_REF}
+          if ! git diff --exit-code origin/${GITHUB_BASE_REF} origin/${GITHUB_HEAD_REF} \
+                -- $(find . -name pom.xml); then
+            nix run .#update-maven
+          fi
+          if git add nix/ && git commit -m 'Update Nix lock files'; then
+            git push
+          fi
+
   test-k:
     name: 'K Tests'
     runs-on: [self-hosted, linux, normal]
@@ -182,6 +225,7 @@ jobs:
           - runner: MacM1
             os: self-macos-12
     runs-on: ${{ matrix.runner }}
+    needs: [nix-maven]
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v3

README.md

@@ -416,27 +416,6 @@ Common build-time error messages:
       -   if you do not need the symbolic execution capabilities of the K Framework, disable them
           at build time (and remove the GHC dependency) by doing: `mvn package -Dhaskell.backend.skip`.
 
--   When building with nix and getting:
-    -   ```bash
-        error: hash mismatch in fixed-output derivation '/nix/store/wjz7gjqs3cch9lgdjhs1fnb8wfl352vd-k-6.1.0-dirty-maven-deps.drv':
-                specified: sha256-kLpjMj05uC94/5vGMwMlFzLKNFOKey◊Nvq/vmB6pHTAo=
-                    got:    sha256-fFlRqlLDZnVuoJniPvXjqdYEjnKxmFCEniavau/1gcQ=
-        error: 1 dependencies of derivation '/nix/store/79hazjbxp8829wpjvhh9c7kzc1m0ii22-k-6.1.0-dirty.drv' failed to build
-        ```
-
-        copy the `got:` hash (`sha256-fFlRqlLDZnVuoJniPvXjqdYEjnKxmFCEniavau/1gcQ=`) and replace it in `flake.nix`:
-
-        ```nix
-        k-framework = { haskell-backend-bins, llvm-kompile-libs }:
-            prev.callPackage ./nix/k.nix {
-                mvnHash = "sha256-fFlRqlLDZnVuoJniPvXjqdYEjnKxmFCEniavau/1gcQ=";
-                ...
-        ```
-    -   `[ERROR] Failed to execute goal ... org.apache.maven.artifact.resolver.ArtifactNotFoundException: The following artifacts could not be resolved: org.scala-lang:scala-compiler:jar:2.12.18 ...`
-        Add `"org.scala-lang:scala-compiler:2.12.18"` (without the `jar:`) to `manualMvnArtifacts` in `flake.nix`
-
-
-
 If something unexpected happens and the project fails to build, try `mvn clean` and
 rebuild the entire project. Generally speaking, however, the project should build incrementally
 without needing to be cleaned first.

flake.nix

@@ -10,22 +10,33 @@
     };
     nixpkgs.follows = "haskell-backend/nixpkgs";
     flake-utils.url = "github:numtide/flake-utils";
+    mavenix = {
+      url = "github:goodlyrottenapple/mavenix/0cbd57b2494d52909b27f57d03580acc66bf0298";
+      inputs.nixpkgs.follows = "haskell-backend/nixpkgs";
+      inputs.utils.follows = "flake-utils";
+    };
     llvm-backend = {
       url = "github:runtimeverification/llvm-backend";
       inputs.nixpkgs.follows = "haskell-backend/nixpkgs";
+      inputs.mavenix.follows = "mavenix";
       inputs.utils.follows = "flake-utils";
     };
     rv-utils.url = "github:runtimeverification/rv-nix-tools";
+    # needed by nix/flake-compat-k-unwrapped.nix
+    flake-compat = {
+      url = "github:edolstra/flake-compat";
+      flake = false;
+    };
   };
 
-  outputs = { self, nixpkgs, flake-utils, rv-utils, haskell-backend
-    , booster-backend, llvm-backend }:
+  outputs = { self, nixpkgs, flake-utils, rv-utils, haskell-backend, booster-backend
+    , llvm-backend, mavenix, flake-compat }:
     let
       allOverlays = [
         (_: _: {
           llvm-version = 15;
-          llvm-backend-build-type = "Release";
-        })
+          llvm-backend-build-type = "Release"; })
+        mavenix.overlay
         llvm-backend.overlays.default
         haskell-backend.overlays.z3
         haskell-backend.overlays.integration-tests
@@ -57,22 +68,12 @@
               '';
             };
           in {
-            # 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 }:
               prev.callPackage ./nix/k.nix {
-                mvnHash = "sha256-EvTLGyv648FT47yAWoM2imsZe+GJzIELHG5SvUws68A=";
-                manualMvnArtifacts = [
-                  "org.scala-lang:scala-compiler:2.12.18"
-                  "ant-contrib:ant-contrib:1.0b3"
-                  "org.apache.ant:ant-nodeps:1.8.1"
-                ];
-                inherit (final) maven;
                 inherit (prev) llvm-backend;
                 clang = prev."clang_${toString final.llvm-version}";
-                booster =
-                  booster-backend.packages.${prev.system}.kore-rpc-booster;
+                booster = booster-backend.packages.${prev.system}.kore-rpc-booster;
+                mavenix = { inherit (prev) buildMaven; };
                 haskell-backend = haskell-backend-bins;
                 inherit (haskell-backend) prelude-kore;
                 inherit src;
@@ -100,13 +101,14 @@
           # Temporarily required until a bug on pyOpenSSL is resolved for aarch64-darwin
           # https://github.com/NixOS/nixpkgs/pull/172397
           config.allowBroken = system == "aarch64-darwin";
-          overlays =
-            [ (final: prev: { llvm-backend-build-type = "FastBuild"; }) ]
+          overlays = [ (final: prev: { llvm-backend-build-type = "FastBuild"; }) ]
             ++ allOverlays;
         };
 
         haskell-backend-bins = pkgs.symlinkJoin {
-          name = "kore-${haskell-backend.sourceInfo.shortRev or "local"}";
+          name = "kore-${
+              haskell-backend.sourceInfo.shortRev or "local"
+            }";
           paths = let p = haskell-backend.packages.${system};
           in [
             p.kore-exec
@@ -118,8 +120,7 @@
         };
 
       in rec {
-        k-version =
-          pkgs.lib.removeSuffix "\n" (builtins.readFile ./package/version);
+        k-version = pkgs.lib.removeSuffix "\n" (builtins.readFile ./package/version);
 
         packages = rec {
           k = pkgs.k-framework {
@@ -130,6 +131,23 @@
             };
           };
 
+          # This is a copy of the `nix/update-maven.sh` script, which should be
+          # eventually removed. Having this inside the flake provides a uniform
+          # interface, i.e. we have `update-maven` in k and
+          # `update-cabal` in the haskell-backend.
+          # The first `nix-build` command below ensures k source is loaded into the Nix store.
+          # This command will fail, but only after loading the source.
+          # mavenix will not do this automatically because we it uses restrict-eval,
+          # and we are using filterSource, which is disabled under restrict-eval.
+          update-maven = pkgs.writeShellScriptBin "update-maven" ''
+            #!/bin/sh
+            ${pkgs.nix}/bin/nix-build --no-out-link -E 'import ./nix/flake-compat-k-unwrapped.nix' \
+              || echo "^~~~ expected error"
+
+            export PATH="${pkgs.gnused}/bin:$PATH"
+            ${pkgs.mavenix-cli}/bin/mvnix-update -l ./nix/mavenix.lock -E 'import ./nix/flake-compat-k-unwrapped.nix'
+          '';
+
           check-submodules = rv-utils.lib.check-submodules pkgs {
             inherit llvm-backend haskell-backend booster-backend;
           };
@@ -189,10 +207,7 @@
             };
         };
         defaultPackage = packages.k;
-        devShells.kore-integration-tests = pkgs.kore-tests (pkgs.k-framework {
-          inherit haskell-backend-bins;
-          llvm-kompile-libs = { };
-        });
+        devShells.kore-integration-tests = pkgs.kore-tests (pkgs.k-framework { inherit haskell-backend-bins; llvm-kompile-libs = {}; });
       }) // {
         overlays.llvm-backend = llvm-backend.overlays.default;
         overlays.z3 = haskell-backend.overlays.z3;