Skip to content

Commit fc09a5c

Browse files
F-WRunTimeRobertorosmaninho
F-WRunTime
and
Robertorosmaninho
authored
Resolve Spotless + Java 17 (#4869)
Resolving TODO items from PR #4857 --------- Co-authored-by: Roberto Rosmaninho <robertogomes@dcc.ufmg.br>
1 parent ec6b3c2 commit fc09a5c

File tree

18 files changed

+85
-78
lines changed

18 files changed

+85
-78
lines changed

‎.github/workflows/release.yml‎

Lines changed: 0 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -382,15 +382,6 @@ jobs:
382382
name: homebrew
383383
path: homebrew-k
384384

385-
- name: Delete Release
386-
if: failure()
387-
uses: actions/github-script@v7
388-
with:
389-
github-token: ${{secrets.GITHUB_TOKEN}}
390-
script: |
391-
const { owner, repo } = context.repo
392-
await github.rest.repos.deleteRelease({ owner, repo, release_id: ${{ needs.set-release-id.outputs.release_id }} })
393-
394385
outputs:
395386
bottle_path: ${{ steps.build.outputs.path }}
396387
bottle_path_remote: ${{ steps.build.outputs.path_remote }}

‎.github/workflows/test-pr.yml‎

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -344,6 +344,12 @@ jobs:
344344
needs: code-quality
345345
continue-on-error: true # Do not fail PRs due to MacOS builds at this time. Oct. 6, 2025
346346
steps:
347+
- name: 'Set up Java 17'
348+
uses: actions/setup-java@v4
349+
with:
350+
distribution: 'zulu'
351+
java-version: 17
352+
347353
- name: 'Check out code'
348354
uses: actions/checkout@v4
349355
with:
@@ -433,9 +439,11 @@ jobs:
433439
# Test the Homebrew formula validation and basic functionality
434440
cd homebrew-k
435441
442+
# Remove any existing tap to avoid remote mismatch errors
443+
brew untap runtimeverification/k 2>/dev/null || true
444+
436445
# Validate the formula syntax by installing it as a local tap
437-
brew tap runtimeverification/k .
438-
brew audit --strict kframework
446+
brew tap runtimeverification/k "file://$(pwd)"
439447
440448
# Test formula installation from source
441449
brew install --build-from-source kframework -v

‎flake.lock‎

Lines changed: 3 additions & 3 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎flake.nix‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -119,7 +119,7 @@
119119

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

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -571,7 +571,7 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
571571
switch (type) {
572572
case "Set":
573573
bagAtt = bagAtt.add(Att.IDEM(), "");
574-
// fall through
574+
// fall through
575575
case "Map":
576576
bagAtt = bagAtt.add(Att.COMM(), "");
577577
break;

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

Lines changed: 27 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -861,14 +861,14 @@ private Claim upClaim(K contents) {
861861
KApply ruleContents = (KApply) contents;
862862
List<org.kframework.kore.K> items = ruleContents.klist().items();
863863
return switch (ruleContents.klabel().name()) {
864-
case "#ruleNoConditions" -> Claim(
865-
items.get(0), BooleanUtils.TRUE, BooleanUtils.TRUE, ruleContents.att());
866-
case "#ruleRequires" -> Claim(
867-
items.get(0), items.get(1), BooleanUtils.TRUE, ruleContents.att());
868-
case "#ruleEnsures" -> Claim(
869-
items.get(0), BooleanUtils.TRUE, items.get(1), ruleContents.att());
870-
case "#ruleRequiresEnsures" -> Claim(
871-
items.get(0), items.get(1), items.get(2), ruleContents.att());
864+
case "#ruleNoConditions" ->
865+
Claim(items.get(0), BooleanUtils.TRUE, BooleanUtils.TRUE, ruleContents.att());
866+
case "#ruleRequires" ->
867+
Claim(items.get(0), items.get(1), BooleanUtils.TRUE, ruleContents.att());
868+
case "#ruleEnsures" ->
869+
Claim(items.get(0), BooleanUtils.TRUE, items.get(1), ruleContents.att());
870+
case "#ruleRequiresEnsures" ->
871+
Claim(items.get(0), items.get(1), items.get(2), ruleContents.att());
872872
default -> throw new AssertionError("Wrong KLabel for claim content");
873873
};
874874
}
@@ -877,14 +877,14 @@ private Rule upRule(K contents) {
877877
KApply ruleContents = (KApply) contents;
878878
List<org.kframework.kore.K> items = ruleContents.klist().items();
879879
return switch (ruleContents.klabel().name()) {
880-
case "#ruleNoConditions" -> Rule(
881-
items.get(0), BooleanUtils.TRUE, BooleanUtils.TRUE, ruleContents.att());
882-
case "#ruleRequires" -> Rule(
883-
items.get(0), items.get(1), BooleanUtils.TRUE, ruleContents.att());
884-
case "#ruleEnsures" -> Rule(
885-
items.get(0), BooleanUtils.TRUE, items.get(1), ruleContents.att());
886-
case "#ruleRequiresEnsures" -> Rule(
887-
items.get(0), items.get(1), items.get(2), ruleContents.att());
880+
case "#ruleNoConditions" ->
881+
Rule(items.get(0), BooleanUtils.TRUE, BooleanUtils.TRUE, ruleContents.att());
882+
case "#ruleRequires" ->
883+
Rule(items.get(0), items.get(1), BooleanUtils.TRUE, ruleContents.att());
884+
case "#ruleEnsures" ->
885+
Rule(items.get(0), BooleanUtils.TRUE, items.get(1), ruleContents.att());
886+
case "#ruleRequiresEnsures" ->
887+
Rule(items.get(0), items.get(1), items.get(2), ruleContents.att());
888888
default -> throw new AssertionError("Wrong KLabel for rule content");
889889
};
890890
}
@@ -895,8 +895,9 @@ private Context upContext(K contents) {
895895
return switch (ruleContents.klabel().name()) {
896896
case "#ruleNoConditions" -> Context(items.get(0), BooleanUtils.TRUE, ruleContents.att());
897897
case "#ruleRequires" -> Context(items.get(0), items.get(1), ruleContents.att());
898-
default -> throw KEMException.criticalError(
899-
"Illegal context with ensures clause detected.", contents);
898+
default ->
899+
throw KEMException.criticalError(
900+
"Illegal context with ensures clause detected.", contents);
900901
};
901902
}
902903

@@ -906,20 +907,22 @@ private ContextAlias upAlias(K contents) {
906907
return switch (ruleContents.klabel().name()) {
907908
case "#ruleNoConditions" -> ContextAlias(items.get(0), BooleanUtils.TRUE, ruleContents.att());
908909
case "#ruleRequires" -> ContextAlias(items.get(0), items.get(1), ruleContents.att());
909-
default -> throw KEMException.criticalError(
910-
"Illegal context alias with ensures clause detected.", contents);
910+
default ->
911+
throw KEMException.criticalError(
912+
"Illegal context alias with ensures clause detected.", contents);
911913
};
912914
}
913915

914916
private Configuration upConfiguration(K contents) {
915917
KApply configContents = (KApply) contents;
916918
List<K> items = configContents.klist().items();
917919
return switch (configContents.klabel().name()) {
918-
case "#ruleNoConditions" -> Configuration(
919-
items.get(0), BooleanUtils.TRUE, configContents.att());
920+
case "#ruleNoConditions" ->
921+
Configuration(items.get(0), BooleanUtils.TRUE, configContents.att());
920922
case "#ruleEnsures" -> Configuration(items.get(0), items.get(1), configContents.att());
921-
default -> throw KEMException.compilerError(
922-
"Illegal configuration with requires clause detected.", configContents);
923+
default ->
924+
throw KEMException.compilerError(
925+
"Illegal configuration with requires clause detected.", configContents);
923926
};
924927
}
925928

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

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -734,8 +734,7 @@ public CompletableFuture<List<SelectionRange>> selectionRange(SelectionRangePara
734734
}
735735
} else if (mi
736736
instanceof
737-
StringSentence
738-
ss) { // if we have caches, find the deepest term
737+
StringSentence ss) { // if we have caches, find the deepest term
739738
String suffix =
740739
ss.getType().equals(DefinitionParsing.configuration)
741740
? "-" + RuleGrammarGenerator.CONFIG_CELLS

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

Lines changed: 9 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -56,10 +56,12 @@ public K prettyRead(
5656
return switch (inputMode) {
5757
case JSON, KAST -> deserialize(stringToParse, inputMode, source);
5858
case KORE -> new KoreParser(mod.sortAttributesFor()).parseString(stringToParse);
59-
case PROGRAM -> def.parseSingleTerm(
60-
mod, sort, startSymbolLocation, kem, files, stringToParse, source, partialParseDebug);
61-
case RULE -> throw KEMException.internalError(
62-
"Should have been handled directly by the kast front end: " + inputMode);
59+
case PROGRAM ->
60+
def.parseSingleTerm(
61+
mod, sort, startSymbolLocation, kem, files, stringToParse, source, partialParseDebug);
62+
case RULE ->
63+
throw KEMException.internalError(
64+
"Should have been handled directly by the kast front end: " + inputMode);
6365
};
6466
}
6567

@@ -170,8 +172,9 @@ public static K deserialize(String stringToParse, InputModes inputMode, Source s
170172
return switch (inputMode) {
171173
case JSON -> JsonParser.parse(stringToParse);
172174
case KAST -> KastParser.parse(stringToParse, source);
173-
default -> throw KEMException.criticalError(
174-
"Unsupported input mode for deserialization: " + inputMode);
175+
default ->
176+
throw KEMException.criticalError(
177+
"Unsupported input mode for deserialization: " + inputMode);
175178
};
176179
}
177180
}

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

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -113,8 +113,8 @@ public Either<Set<KEMException>, Term> apply(Term t) {
113113
inferencer.pop();
114114
}
115115
case UNKNOWN ->
116-
// constraints coiuld not be solved, so error
117-
throw KEMException.internalError("Could not solve sortconstraints.", t);
116+
// constraints coiuld not be solved, so error
117+
throw KEMException.internalError("Could not solve sortconstraints.", t);
118118
case UNSATISFIABLE -> {
119119
isMaximal = true;
120120
inferencer.pop();
@@ -127,14 +127,14 @@ public Either<Set<KEMException>, Term> apply(Term t) {
127127
hasAnotherSolution =
128128
switch (inferencer.status()) {
129129
case SATISFIABLE ->
130-
// found another solution, keep going
131-
true;
130+
// found another solution, keep going
131+
true;
132132
case UNKNOWN ->
133-
// constraints could not be solved, so error
134-
throw KEMException.internalError("Could not solve sort constraints.", t);
133+
// constraints could not be solved, so error
134+
throw KEMException.internalError("Could not solve sort constraints.", t);
135135
case UNSATISFIABLE ->
136-
// no more solutions, terminate loop
137-
false;
136+
// no more solutions, terminate loop
137+
false;
138138
};
139139
} while (hasAnotherSolution);
140140
// remove all models that are not maximal

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -254,8 +254,8 @@ private void replayConstraints(List<Constraint> constraints) {
254254
print(constraint.smt);
255255
println("))");
256256
}
257-
case UNKNOWN -> throw KEMException.internalError(
258-
"Could not solve sort constraints.", currentTerm);
257+
case UNKNOWN ->
258+
throw KEMException.internalError("Could not solve sort constraints.", currentTerm);
259259
case UNSATISFIABLE -> {
260260
println("(pop)");
261261
computeStatus();
@@ -866,8 +866,8 @@ private Status computeStatus() {
866866
case "sat" -> Status.SATISFIABLE;
867867
case "unsat" -> Status.UNSATISFIABLE;
868868
case "unknown", "timeout" -> Status.UNKNOWN;
869-
default -> throw KEMException.internalError(
870-
"Unexpected result from z3: " + result, currentTerm);
869+
default ->
870+
throw KEMException.internalError("Unexpected result from z3: " + result, currentTerm);
871871
};
872872
} catch (IOException e) {
873873
throw KEMException.internalError("Could not read from z3 process", e, currentTerm);

0 commit comments

Comments
 (0)