Remove mavenix take 2 (#3806)

Switch from using mavenix to using `buildMavenPackage` back-ported from
the upcoming nixpkgs 23.11 stable release. This may increase build times
somewhat and updating maven dependencies will no longer be automatic,
but arguably the automation never works and It's difficult to figure out
why it's failing.

I've updated the README troubleshooting section with the two cases of
manual intervention, necessary with the new packaging solution, when
maven dependencies change.

The hash mismatch should only happen when deps change, but if we want to
automate this in ci then we can do something similar to:
https://github.com/runtimeverification/hs-backend-booster/blob/175f10b16ad50dd2bb50fcfe68cbcacd79760317/scripts/update-haskell-backend.sh#L21C3-L22

.github/workflows/test-pr.yml

@@ -51,49 +51,6 @@ jobs:
           version: v1.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]
@@ -225,7 +182,6 @@ 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,6 +416,27 @@ 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,33 +10,22 @@
     };
     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, mavenix, flake-compat }:
+  outputs = { self, nixpkgs, flake-utils, rv-utils, haskell-backend
+    , booster-backend, llvm-backend }:
     let
       allOverlays = [
         (_: _: {
           llvm-version = 15;
-          llvm-backend-build-type = "Release"; })
-        mavenix.overlay
+          llvm-backend-build-type = "Release";
+        })
         llvm-backend.overlays.default
         haskell-backend.overlays.z3
         haskell-backend.overlays.integration-tests
@@ -68,12 +57,23 @@
               '';
             };
           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-CF6MQRDMDTSAr3Z7y2yheRiWdA3V0JnnQxRr7UGPm18=";
+                manualMvnArtifacts = [
+                  "org.scala-lang:scala-compiler:2.12.18"
+                  "ant-contrib:ant-contrib:1.0b3"
+                  "org.apache.ant:ant-nodeps:1.8.1"
+                  "org.apache.maven.wagon:wagon-provider-api:1.0-alpha-6"
+                ];
+                inherit (final) maven;
                 inherit (prev) llvm-backend;
                 clang = prev."clang_${toString final.llvm-version}";
-                booster = booster-backend.packages.${prev.system}.kore-rpc-booster;
-                mavenix = { inherit (prev) buildMaven; };
+                booster =
+                  booster-backend.packages.${prev.system}.kore-rpc-booster;
                 haskell-backend = haskell-backend-bins;
                 inherit (haskell-backend) prelude-kore;
                 inherit src;
@@ -101,14 +101,13 @@
           # 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
@@ -120,7 +119,8 @@
         };
 
       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 {
@@ -131,23 +131,6 @@
             };
           };
 
-          # 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;
           };
@@ -207,7 +190,10 @@
             };
         };
         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;