Merge remote-tracking branch 'origin/develop' into _update-deps/runti…

…meverification/hs-backend-booster

.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;

kernel/src/main/java/org/kframework/compile/ResolveFreshConstants.java

@@ -249,8 +249,7 @@ public Module resolve(Module m) {
     if (m.name().equals(def.mainModule().name())) {
       if (!m.definedKLabels().contains(KLabels.GENERATED_TOP_CELL)) {
         RuleGrammarGenerator gen = new RuleGrammarGenerator(def);
-        ParseInModule mod =
-            RuleGrammarGenerator.getCombinedGrammar(gen.getConfigGrammar(m), true, files);
+        ParseInModule mod = RuleGrammarGenerator.getCombinedGrammar(gen.getConfigGrammar(m), files);
         ConfigurationInfoFromModule configInfo = new ConfigurationInfoFromModule(m);
         Sort topCellSort;
         try {
@@ -283,8 +282,7 @@ public Module resolve(Module m) {
     }
     if (m.localKLabels().contains(KLabels.GENERATED_TOP_CELL)) {
       RuleGrammarGenerator gen = new RuleGrammarGenerator(def);
-      ParseInModule mod =
-          RuleGrammarGenerator.getCombinedGrammar(gen.getConfigGrammar(m), true, files);
+      ParseInModule mod = RuleGrammarGenerator.getCombinedGrammar(gen.getConfigGrammar(m), files);
       Set<Sentence> newSentences =
           GenerateSentencesFromConfigDecl.gen(
               freshCell, BooleanUtils.TRUE, Att.empty(), mod.getExtensionModule());

kernel/src/main/java/org/kframework/kast/KastFrontEnd.java

@@ -139,8 +139,7 @@ public int run() {
         String stringToParse = FileUtil.read(options.stringToParse());
         Source source = options.source();
 
-        try (ParseInModule parseInModule =
-            RuleGrammarGenerator.getCombinedGrammar(mod, true, null)) {
+        try (ParseInModule parseInModule = RuleGrammarGenerator.getCombinedGrammar(mod, null)) {
           if (options.debugTokens)
             System.out.println(parseInModule.tokenizeString(stringToParse, source));
           else {
@@ -155,7 +154,7 @@ public int run() {
             // syntax
             // like casts, projections and others
             Module unparsingMod = parseInModule.getExtensionModule();
-            K parsed = new TreeNodesToKORE(Outer::parseSort, true).down(res._1().right().get());
+            K parsed = new TreeNodesToKORE(Outer::parseSort).down(res._1().right().get());
 
             if (options.expandMacros) {
               parsed =