Merge branch 'develop' into _update-deps/runtimeverification/hs-backe…

…nd-booster

.github/workflows/release.yml

@@ -424,8 +424,8 @@ jobs:
       - name: 'Install pandoc/texlive/calibre'
         run: |
           sudo apt update --yes
-          sudo apt install --yes wget texlive-xetex
-          sudo wget -nv -O- https://download.calibre-ebook.com/linux-installer.sh | sh /dev/stdin version=5.44.0
+          sudo apt install --yes wget texlive-xetex libegl1 libopengl0
+          sudo wget -nv -O- https://download.calibre-ebook.com/linux-installer.sh | sh /dev/stdin version=6.29.0
           sudo wget https://github.com/jgm/pandoc/releases/download/2.18/pandoc-2.18-1-amd64.deb -O /tmp/pandoc.deb
           sudo dpkg -i /tmp/pandoc.deb
       - name: 'Checkout code and set up web build'

.github/workflows/test-pr.yml

@@ -230,9 +230,11 @@ jobs:
       - name: 'Build K Framework'
         run: GC_DONT_GC=1 nix build --print-build-logs .
 
+      - name: 'Smoke test K'
+        run: GC_DONT_GC=1 nix build --print-build-logs .#smoke-test
+
       # These tests take a really long time to run on other platforms, so we
       # skip them unless we're on the M1 runner.
       - name: 'Test K'
         if: ${{ matrix.os == 'self-macos-12' }}
         run: GC_DONT_GC=1 nix build --print-build-logs .#test
-

flake.nix

@@ -14,7 +14,7 @@
     llvm-backend.inputs.nixpkgs.follows = "haskell-backend/nixpkgs";
     flake-utils.url = "github:numtide/flake-utils";
     rv-utils.url = "github:runtimeverification/rv-nix-tools";
-    mavenix.url = "github:goodlyrottenapple/mavenix";
+    mavenix.url = "github:nix-community/mavenix";
     # needed by nix/flake-compat-k-unwrapped.nix
     flake-compat = {
       url = "github:edolstra/flake-compat";
@@ -113,6 +113,7 @@
         };
 
       in rec {
+        k-version = pkgs.lib.removeSuffix "\n" (builtins.readFile ./package/version);
 
         packages = rec {
           k = pkgs.k-framework {
@@ -149,11 +150,26 @@
                 "llvm-backend/src/main/native/llvm-backend";
             };
 
+          smoke-test = with pkgs;
+            stdenv.mkDerivation {
+              name = "k-${k-version}-${self.rev or "dirty"}-smoke-test";
+              unpackPhase = "true";
+              buildInputs = [ fmt gmp mpfr k ];
+              buildPhase = ''
+                echo "module TEST imports BOOL endmodule" > test.k
+                kompile test.k --syntax-module TEST --backend llvm
+                rm -rf test-kompiled
+                kompile test.k --syntax-module TEST --backend haskell
+              '';
+              installPhase = ''
+                runHook preInstall
+                touch "$out"
+                runHook postInstall
+              '';
+            };
+
           test = with pkgs;
-            let
-              k-version =
-                lib.removeSuffix "\n" (builtins.readFile ./package/version);
-            in stdenv.mkDerivation {
+            stdenv.mkDerivation {
               name = "k-${k-version}-${self.rev or "dirty"}-test";
               src = lib.cleanSource
                 (nix-gitignore.gitignoreSourcePure [ ./.gitignore ]

k-distribution/src/main/scripts/lib/checkJava

@@ -1,5 +1,5 @@
 #!/usr/bin/env bash
-MIN_VERSION="8"
+MIN_VERSION="17"
 echoerr() { echo "$@" 1>&2; }
 
 if type -p java >/dev/null; then

kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java

@@ -201,8 +201,7 @@ public void convert(boolean heatCoolEq, String prelude, StringBuilder semantics,
         SetMultimap<KLabel, Rule> functionRules = HashMultimap.create();
         for (Rule rule : sortedRules) {
             K left = RewriteToTop.toLeft(rule.body());
-            if (left instanceof KApply) {
-                KApply kapp = (KApply) left;
+            if (left instanceof KApply kapp) {
                 Production prod = production(kapp);
                 if (prod.att().contains(Att.FUNCTION()) || rule.att().contains(Att.ANYWHERE()) || ExpandMacros.isMacro(rule)) {
                     functionRules.put(kapp.klabel(), rule);
@@ -1696,38 +1695,23 @@ private Production production(KApply term, boolean instantiatePolySorts) {
     }
 
     private static String convertBuiltinLabel(String klabel) {
-      switch(klabel) {
-      case "#Bottom":
-        return "\\bottom";
-      case "#Top":
-        return "\\top";
-      case "#Or":
-        return "\\or";
-      case "#And":
-        return "\\and";
-      case "#Not":
-        return "\\not";
-      case "#Floor":
-        return "\\floor";
-      case "#Ceil":
-        return "\\ceil";
-      case "#Equals":
-        return "\\equals";
-      case "#Implies":
-        return "\\implies";
-      case "#Exists":
-        return "\\exists";
-      case "#Forall":
-        return "\\forall";
-      case "#AG":
-        return "allPathGlobally";
-      case "weakExistsFinally":
-        return ONE_PATH_OP;
-      case "weakAlwaysFinally":
-        return ALL_PATH_OP;
-      default:
-        throw KEMException.compilerError("Unsuppored kore connective in rule: " + klabel);
-      }
+        return switch (klabel) {
+            case "#Bottom" -> "\\bottom";
+            case "#Top" -> "\\top";
+            case "#Or" -> "\\or";
+            case "#And" -> "\\and";
+            case "#Not" -> "\\not";
+            case "#Floor" -> "\\floor";
+            case "#Ceil" -> "\\ceil";
+            case "#Equals" -> "\\equals";
+            case "#Implies" -> "\\implies";
+            case "#Exists" -> "\\exists";
+            case "#Forall" -> "\\forall";
+            case "#AG" -> "allPathGlobally";
+            case "weakExistsFinally" -> ONE_PATH_OP;
+            case "weakAlwaysFinally" -> ALL_PATH_OP;
+            default -> throw KEMException.compilerError("Unsuppored kore connective in rule: " + klabel);
+        };
     }
 
     public static void convert(KLabel klabel, StringBuilder sb) {
@@ -1858,14 +1842,12 @@ private void convert(Map<Att.Key, Boolean> attributes, Att att, StringBuilder sb
                     convertStringVarList(location, freeVarsMap, strVal, sb);
                 } else {
                     switch (strKey) {
-                        case "unit":
-                        case "element":
-                            Production prod = production(KApply(KLabel(strVal)));
-                            convert(prod.klabel().get(), prod.params(), sb);
-                            sb.append("()");
-                            break;
-                        default:
-                            sb.append(StringUtil.enquoteKString(strVal));
+                    case "unit", "element" -> {
+                        Production prod = production(KApply(KLabel(strVal)));
+                        convert(prod.klabel().get(), prod.params(), sb);
+                        sb.append("()");
+                    }
+                    default -> sb.append(StringUtil.enquoteKString(strVal));
                     }
                 }
                 sb.append(")");
@@ -1911,18 +1893,13 @@ private static String[] asciiReadableEncodingKoreCalc() {
     public static String[] asciiReadableEncodingKore = asciiReadableEncodingKoreCalc();
 
     private static void convert(String name, StringBuilder sb) {
-        switch(name) {
-        case "module":
-        case "endmodule":
-        case "sort":
-        case "hooked-sort":
-        case "symbol":
-        case "hooked-symbol":
-        case "alias":
-        case "axiom":
+        switch (name) {
+        case "module", "endmodule", "sort", "hooked-sort", "symbol", "hooked-symbol", "alias", "axiom" -> {
             sb.append(name).append("'Kywd'");
             return;
-        default: break;
+        }
+        default -> {
+        }
         }
         StringBuilder buffer = new StringBuilder();
         StringUtil.encodeStringToAlphanumeric(buffer, name, asciiReadableEncodingKore, identChar, "'");

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

@@ -53,8 +53,7 @@ public Boolean unit() {
             @Override
             public Boolean apply(KApply k) {
                 if (mod.attributesFor().get(k.klabel()).getOrElse(() -> Att.empty()).contains(Att.MAINCELL())) {
-                    if (k.items().get(0) instanceof KSequence) {
-                        KSequence seq = (KSequence) k.items().get(0);
+                    if (k.items().get(0) instanceof KSequence seq) {
                         if (seq.items().size() > 1 && seq.items().get(0) instanceof KVariable) {
                             return true;
                         }

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

@@ -48,11 +48,9 @@ public Sentence apply(Module m, Sentence s) {
             return s;
         }
 
-        if (s instanceof RuleOrClaim) {
-            RuleOrClaim rule = (RuleOrClaim) s;
+        if (s instanceof RuleOrClaim rule) {
             return rule.newInstance(apply(rule.body(), m, rule instanceof Claim), rule.requires(), rule.ensures(), rule.att());
-        } else if (s instanceof Context) {
-            Context context = (Context) s;
+        } else if (s instanceof Context context) {
             return new Context(apply(context.body(), m, false), context.requires(), context.att());
         } else {
             return s;
@@ -74,8 +72,7 @@ private boolean shouldConsider(List<K> items, boolean isClaim) {
             return true;
         } else if (items.size() == 2 && isClaim) {
             K second = items.get(1);
-            if(second instanceof KApply) {
-                KApply app = (KApply) second;
+            if(second instanceof KApply app) {
                 return app.klabel() == KLabels.GENERATED_COUNTER_CELL;
             }
         }
@@ -88,8 +85,7 @@ private boolean canAddImplicitKCell(K item) {
             return false;
         }
 
-        if (item instanceof KRewrite) {
-            final KRewrite rew = (KRewrite) item;
+        if (item instanceof final KRewrite rew) {
             return Stream.concat(
                             IncompleteCellUtils.flattenCells(rew.left()).stream(),
                             IncompleteCellUtils.flattenCells(rew.right()).stream())

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

@@ -21,8 +21,7 @@ public class AddImplicitCounterCell {
     public AddImplicitCounterCell() {}
 
     public Sentence apply(Module m, Sentence s) {
-        if(s instanceof Claim) {
-            Claim claim = (Claim) s;
+        if(s instanceof Claim claim) {
             return claim.newInstance(apply(claim.body(), m), claim.requires(), claim.ensures(), claim.att());
         }
         return s;

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

@@ -181,8 +181,7 @@ Optional<Integer> getLevel(K k) {
                 }
             }
             return Optional.empty();
-        } else if (k instanceof  KRewrite) {
-            KRewrite rew = (KRewrite) k;
+        } else if (k instanceof KRewrite rew) {
             List<K> cells = IncompleteCellUtils.flattenCells(rew.left());
             cells.addAll(IncompleteCellUtils.flattenCells(rew.right()));
             Optional<Integer> level = Optional.empty();
@@ -205,8 +204,7 @@ Optional<Integer> getLevel(K k) {
     }
 
     Optional<KLabel> getParent(K k) {
-        if (k instanceof KApply) {
-            final KApply app = (KApply) k;
+        if (k instanceof final KApply app) {
             if (KLabels.CELLS.equals(app.klabel())) {
                 List<K> items = app.klist().items();
                 if (items.isEmpty()) {
@@ -246,10 +244,9 @@ Optional<KLabel> getParent(K k) {
     }
 
     K concretizeCell(K k) {
-        if (!(k instanceof KApply)) {
+        if (!(k instanceof KApply app)) {
             return k;
         } else {
-            KApply app = (KApply) k;
             KLabel target = app.klabel();
             if (cfg.isLeafCell(target)) {
                 return k;
@@ -291,17 +288,15 @@ K concretizeCell(K k) {
     }
 
     K concretize(K term) {
-        if (term instanceof KApply) {
-            KApply app = (KApply) term;
+        if (term instanceof KApply app) {
             KApply newTerm = KApply(app.klabel(), KList(app.klist().stream()
                     .map(this::concretize).collect(Collectors.toList())), app.att());
             if (cfg.isParentCell(newTerm.klabel())) {
                 return concretizeCell(newTerm);
             } else {
                 return newTerm;
             }
-        } else if (term instanceof KRewrite) {
-            KRewrite rew = (KRewrite) term;
+        } else if (term instanceof KRewrite rew) {
             return KRewrite(concretize(rew.left()), concretize(rew.right()));
         } else if (term instanceof KSequence) {
             return KSequence(((KSequence) term).stream()
@@ -314,11 +309,9 @@ K concretize(K term) {
     }
 
     public Sentence concretize(Sentence m) {
-        if (m instanceof RuleOrClaim) {
-            RuleOrClaim r = (RuleOrClaim) m;
+        if (m instanceof RuleOrClaim r) {
             return r.newInstance(concretize(r.body()), r.requires(), r.ensures(), r.att());
-        } else if (m instanceof Context) {
-            Context c = (Context) m;
+        } else if (m instanceof Context c) {
             return new Context(concretize(c.body()), c.requires(), c.att());
         } else {
             return m;