Resolve Spotless + Java 17

.github/workflows/release.yml

@@ -382,15 +382,6 @@ jobs:
           name: homebrew
           path: homebrew-k
 
-      - name: Delete Release
-        if: failure()
-        uses: actions/github-script@v7
-        with:
-          github-token: ${{secrets.GITHUB_TOKEN}}
-          script: |
-            const { owner, repo } = context.repo
-            await github.rest.repos.deleteRelease({ owner, repo, release_id: ${{ needs.set-release-id.outputs.release_id }} })
-
     outputs:
       bottle_path: ${{ steps.build.outputs.path }}
       bottle_path_remote: ${{ steps.build.outputs.path_remote }}

.github/workflows/test-pr.yml

@@ -344,6 +344,12 @@ jobs:
     needs: code-quality
     continue-on-error: true # Do not fail PRs due to MacOS builds at this time. Oct. 6, 2025
     steps:
+      - name: 'Set up Java 17'
+        uses: actions/setup-java@v4
+        with:
+          distribution: 'zulu'
+          java-version: 17
+
       - name: 'Check out code'
         uses: actions/checkout@v4
         with:
@@ -433,9 +439,11 @@ jobs:
           # Test the Homebrew formula validation and basic functionality
           cd homebrew-k
 
+          # Remove any existing tap to avoid remote mismatch errors
+          brew untap runtimeverification/k 2>/dev/null || true
+
           # Validate the formula syntax by installing it as a local tap
-          brew tap runtimeverification/k .
-          brew audit --strict kframework
+          brew tap runtimeverification/k "file://$(pwd)"
 
           # Test formula installation from source
           brew install --build-from-source kframework -v

flake.nix

@@ -119,7 +119,7 @@
 
             mk-k-framework = { haskell-backend-bins, llvm-kompile-libs }:
               prev.callPackage ./nix/k.nix {
-                mvnHash = "sha256-aUomhCjSIBIQdavd3XojKJFdU74UURaKEVEKXiPTq1Q=";
+                mvnHash = "sha256-Hn+MfNow6H42ZUShNiJnZsZhlV5AkxlsYUaewxnaN1w=";
                 manualMvnArtifacts = [
                   "org.scala-lang:scala-compiler:2.13.13"
                   "ant-contrib:ant-contrib:1.0b3"

k-frontend/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java

@@ -571,7 +571,7 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
       switch (type) {
         case "Set":
           bagAtt = bagAtt.add(Att.IDEM(), "");
-          // fall through
+        // fall through
         case "Map":
           bagAtt = bagAtt.add(Att.COMM(), "");
           break;

k-frontend/src/main/java/org/kframework/kompile/DefinitionParsing.java

@@ -861,14 +861,14 @@ private Claim upClaim(K contents) {
     KApply ruleContents = (KApply) contents;
     List<org.kframework.kore.K> items = ruleContents.klist().items();
     return switch (ruleContents.klabel().name()) {
-      case "#ruleNoConditions" -> Claim(
-          items.get(0), BooleanUtils.TRUE, BooleanUtils.TRUE, ruleContents.att());
-      case "#ruleRequires" -> Claim(
-          items.get(0), items.get(1), BooleanUtils.TRUE, ruleContents.att());
-      case "#ruleEnsures" -> Claim(
-          items.get(0), BooleanUtils.TRUE, items.get(1), ruleContents.att());
-      case "#ruleRequiresEnsures" -> Claim(
-          items.get(0), items.get(1), items.get(2), ruleContents.att());
+      case "#ruleNoConditions" ->
+          Claim(items.get(0), BooleanUtils.TRUE, BooleanUtils.TRUE, ruleContents.att());
+      case "#ruleRequires" ->
+          Claim(items.get(0), items.get(1), BooleanUtils.TRUE, ruleContents.att());
+      case "#ruleEnsures" ->
+          Claim(items.get(0), BooleanUtils.TRUE, items.get(1), ruleContents.att());
+      case "#ruleRequiresEnsures" ->
+          Claim(items.get(0), items.get(1), items.get(2), ruleContents.att());
       default -> throw new AssertionError("Wrong KLabel for claim content");
     };
   }
@@ -877,14 +877,14 @@ private Rule upRule(K contents) {
     KApply ruleContents = (KApply) contents;
     List<org.kframework.kore.K> items = ruleContents.klist().items();
     return switch (ruleContents.klabel().name()) {
-      case "#ruleNoConditions" -> Rule(
-          items.get(0), BooleanUtils.TRUE, BooleanUtils.TRUE, ruleContents.att());
-      case "#ruleRequires" -> Rule(
-          items.get(0), items.get(1), BooleanUtils.TRUE, ruleContents.att());
-      case "#ruleEnsures" -> Rule(
-          items.get(0), BooleanUtils.TRUE, items.get(1), ruleContents.att());
-      case "#ruleRequiresEnsures" -> Rule(
-          items.get(0), items.get(1), items.get(2), ruleContents.att());
+      case "#ruleNoConditions" ->
+          Rule(items.get(0), BooleanUtils.TRUE, BooleanUtils.TRUE, ruleContents.att());
+      case "#ruleRequires" ->
+          Rule(items.get(0), items.get(1), BooleanUtils.TRUE, ruleContents.att());
+      case "#ruleEnsures" ->
+          Rule(items.get(0), BooleanUtils.TRUE, items.get(1), ruleContents.att());
+      case "#ruleRequiresEnsures" ->
+          Rule(items.get(0), items.get(1), items.get(2), ruleContents.att());
       default -> throw new AssertionError("Wrong KLabel for rule content");
     };
   }
@@ -895,8 +895,9 @@ private Context upContext(K contents) {
     return switch (ruleContents.klabel().name()) {
       case "#ruleNoConditions" -> Context(items.get(0), BooleanUtils.TRUE, ruleContents.att());
       case "#ruleRequires" -> Context(items.get(0), items.get(1), ruleContents.att());
-      default -> throw KEMException.criticalError(
-          "Illegal context with ensures clause detected.", contents);
+      default ->
+          throw KEMException.criticalError(
+              "Illegal context with ensures clause detected.", contents);
     };
   }
 
@@ -906,20 +907,22 @@ private ContextAlias upAlias(K contents) {
     return switch (ruleContents.klabel().name()) {
       case "#ruleNoConditions" -> ContextAlias(items.get(0), BooleanUtils.TRUE, ruleContents.att());
       case "#ruleRequires" -> ContextAlias(items.get(0), items.get(1), ruleContents.att());
-      default -> throw KEMException.criticalError(
-          "Illegal context alias with ensures clause detected.", contents);
+      default ->
+          throw KEMException.criticalError(
+              "Illegal context alias with ensures clause detected.", contents);
     };
   }
 
   private Configuration upConfiguration(K contents) {
     KApply configContents = (KApply) contents;
     List<K> items = configContents.klist().items();
     return switch (configContents.klabel().name()) {
-      case "#ruleNoConditions" -> Configuration(
-          items.get(0), BooleanUtils.TRUE, configContents.att());
+      case "#ruleNoConditions" ->
+          Configuration(items.get(0), BooleanUtils.TRUE, configContents.att());
       case "#ruleEnsures" -> Configuration(items.get(0), items.get(1), configContents.att());
-      default -> throw KEMException.compilerError(
-          "Illegal configuration with requires clause detected.", configContents);
+      default ->
+          throw KEMException.compilerError(
+              "Illegal configuration with requires clause detected.", configContents);
     };
   }
 

k-frontend/src/main/java/org/kframework/lsp/TextDocumentSyncHandler.java

@@ -734,8 +734,7 @@ public CompletableFuture<List<SelectionRange>> selectionRange(SelectionRangePara
                         }
                       } else if (mi
                           instanceof
-                          StringSentence
-                          ss) { // if we have caches, find the deepest term
+                          StringSentence ss) { // if we have caches, find the deepest term
                         String suffix =
                             ss.getType().equals(DefinitionParsing.configuration)
                                 ? "-" + RuleGrammarGenerator.CONFIG_CELLS

k-frontend/src/main/java/org/kframework/parser/KRead.java

@@ -56,10 +56,12 @@ public K prettyRead(
     return switch (inputMode) {
       case JSON, KAST -> deserialize(stringToParse, inputMode, source);
       case KORE -> new KoreParser(mod.sortAttributesFor()).parseString(stringToParse);
-      case PROGRAM -> def.parseSingleTerm(
-          mod, sort, startSymbolLocation, kem, files, stringToParse, source, partialParseDebug);
-      case RULE -> throw KEMException.internalError(
-          "Should have been handled directly by the kast front end: " + inputMode);
+      case PROGRAM ->
+          def.parseSingleTerm(
+              mod, sort, startSymbolLocation, kem, files, stringToParse, source, partialParseDebug);
+      case RULE ->
+          throw KEMException.internalError(
+              "Should have been handled directly by the kast front end: " + inputMode);
     };
   }
 
@@ -170,8 +172,9 @@ public static K deserialize(String stringToParse, InputModes inputMode, Source s
     return switch (inputMode) {
       case JSON -> JsonParser.parse(stringToParse);
       case KAST -> KastParser.parse(stringToParse, source);
-      default -> throw KEMException.criticalError(
-          "Unsupported input mode for deserialization: " + inputMode);
+      default ->
+          throw KEMException.criticalError(
+              "Unsupported input mode for deserialization: " + inputMode);
     };
   }
 }

k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferenceVisitor.java

@@ -113,8 +113,8 @@ public Either<Set<KEMException>, Term> apply(Term t) {
               inferencer.pop();
             }
             case UNKNOWN ->
-            // constraints coiuld not be solved, so error
-            throw KEMException.internalError("Could not solve sortconstraints.", t);
+                // constraints coiuld not be solved, so error
+                throw KEMException.internalError("Could not solve sortconstraints.", t);
             case UNSATISFIABLE -> {
               isMaximal = true;
               inferencer.pop();
@@ -127,14 +127,14 @@ public Either<Set<KEMException>, Term> apply(Term t) {
         hasAnotherSolution =
             switch (inferencer.status()) {
               case SATISFIABLE ->
-              // found another solution, keep going
-              true;
+                  // found another solution, keep going
+                  true;
               case UNKNOWN ->
-              // constraints could not be solved, so error
-              throw KEMException.internalError("Could not solve sort constraints.", t);
+                  // constraints could not be solved, so error
+                  throw KEMException.internalError("Could not solve sort constraints.", t);
               case UNSATISFIABLE ->
-              // no more solutions, terminate loop
-              false;
+                  // no more solutions, terminate loop
+                  false;
             };
       } while (hasAnotherSolution);
       // remove all models that are not maximal

k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferencer.java

@@ -254,8 +254,8 @@ private void replayConstraints(List<Constraint> constraints) {
           print(constraint.smt);
           println("))");
         }
-        case UNKNOWN -> throw KEMException.internalError(
-            "Could not solve sort constraints.", currentTerm);
+        case UNKNOWN ->
+            throw KEMException.internalError("Could not solve sort constraints.", currentTerm);
         case UNSATISFIABLE -> {
           println("(pop)");
           computeStatus();
@@ -866,8 +866,8 @@ private Status computeStatus() {
         case "sat" -> Status.SATISFIABLE;
         case "unsat" -> Status.UNSATISFIABLE;
         case "unknown", "timeout" -> Status.UNKNOWN;
-        default -> throw KEMException.internalError(
-            "Unexpected result from z3: " + result, currentTerm);
+        default ->
+            throw KEMException.internalError("Unexpected result from z3: " + result, currentTerm);
       };
     } catch (IOException e) {
       throw KEMException.internalError("Could not read from z3 process", e, currentTerm);

k-frontend/src/main/java/org/kframework/parser/json/JsonParser.java

@@ -272,8 +272,9 @@ public static Sentence toSentence(JsonObject data) {
         }
         return new Production(klabel, immutable(params), sort, immutable(pItems), att);
       }
-      default -> throw KEMException.criticalError(
-          "Unexpected node found in KAST Json term: " + data.getString("node"));
+      default ->
+          throw KEMException.criticalError(
+              "Unexpected node found in KAST Json term: " + data.getString("node"));
     }
   }
 
@@ -306,8 +307,9 @@ private static ProductionItem toProductionItem(JsonObject data) {
         String value = data.getString("value");
         return new Terminal(value);
       }
-      default -> throw KEMException.criticalError(
-          "Unexpected node found in ProductionItem Json term: " + data.getString("node"));
+      default ->
+          throw KEMException.criticalError(
+              "Unexpected node found in ProductionItem Json term: " + data.getString("node"));
     }
   }
 

llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java

@@ -102,10 +102,11 @@ public void accept(Backend.Holder h) {
     String llvmType =
         switch (options.llvmKompileType) {
           case "main", "search", "static", "library", "python", "c" -> options.llvmKompileType;
-          default -> throw KEMException.criticalError(
-              "Non-valid argument for --llvm-kompile-type: "
-                  + options.llvmKompileType
-                  + ". Expected [main|search|library|static|python|c]");
+          default ->
+              throw KEMException.criticalError(
+                  "Non-valid argument for --llvm-kompile-type: "
+                      + options.llvmKompileType
+                      + ". Expected [main|search|library|static|python|c]");
         };
 
     String llvmOutput = "interpreter";
@@ -238,11 +239,11 @@ private KException translateError(MatchingException ex, Map<String, String> hook
             getLocation(ex).orElse(null));
       }
 
-      case INTERNAL_ERROR -> throw KEMException.internalError(
-          ex.getMessage(), ex, getLocation(ex), getSource(ex));
+      case INTERNAL_ERROR ->
+          throw KEMException.internalError(ex.getMessage(), ex, getLocation(ex), getSource(ex));
 
-      case COMPILER_ERROR -> throw KEMException.compilerError(
-          ex.getMessage(), ex, getLocation(ex), getSource(ex));
+      case COMPILER_ERROR ->
+          throw KEMException.compilerError(ex.getMessage(), ex, getLocation(ex), getSource(ex));
     }
 
     throw KEMException.criticalError("Unhandled pattern matching exception", ex);

mvn-lock/dependencies-lock.json

@@ -98,7 +98,7 @@
   }, {
     "groupId" : "com.google.googlejavaformat",
     "artifactId" : "google-java-format",
-    "version" : "1.18.1",
+    "version" : "1.28.0",
     "scope" : "compile",
     "type" : "jar",
     "optional" : false,

mvn-lock/haskell-backend/dependencies-lock.json

@@ -122,7 +122,7 @@
   }, {
     "groupId" : "com.google.googlejavaformat",
     "artifactId" : "google-java-format",
-    "version" : "1.18.1",
+    "version" : "1.28.0",
     "scope" : "compile",
     "type" : "jar",
     "optional" : false,

mvn-lock/k-distribution/dependencies-lock.json

@@ -122,7 +122,7 @@
   }, {
     "groupId" : "com.google.googlejavaformat",
     "artifactId" : "google-java-format",
-    "version" : "1.18.1",
+    "version" : "1.28.0",
     "scope" : "compile",
     "type" : "jar",
     "optional" : false,

mvn-lock/k-frontend/dependencies-lock.json

@@ -122,7 +122,7 @@
   }, {
     "groupId" : "com.google.googlejavaformat",
     "artifactId" : "google-java-format",
-    "version" : "1.18.1",
+    "version" : "1.28.0",
     "scope" : "compile",
     "type" : "jar",
     "optional" : false,

mvn-lock/llvm-backend/dependencies-lock.json

@@ -122,7 +122,7 @@
   }, {
     "groupId" : "com.google.googlejavaformat",
     "artifactId" : "google-java-format",
-    "version" : "1.18.1",
+    "version" : "1.28.0",
     "scope" : "compile",
     "type" : "jar",
     "optional" : false,

pom.xml

@@ -78,7 +78,7 @@
     <scala.minorVersion>13</scala.minorVersion>
     <scala.version>${scala.majorVersion}.${scala.minorVersion}</scala.version>
     <spotless.version>2.41.1</spotless.version>
-    <googleJavaFormat.version>1.18.1</googleJavaFormat.version>
+    <googleJavaFormat.version>1.28.0</googleJavaFormat.version>
     <scalafmt.version>3.7.17</scalafmt.version>
     <nativeDirs>**/src/main/native/**</nativeDirs>
     <spotless.excludes>${nativeDirs},.idea/**,**/com/davekoelle/**,**/target/**,LICENSE.md,web/toc.md,web/k-web-theme/**,**/*-kompiled/*.kore,k-distribution/include/kframework/kore/*,**/.kompile-*/**,**/.git/**,result/**,pyk/**,nix/resources/**</spotless.excludes>