update gradle

Author: wadoon

build.gradle

@@ -30,11 +30,11 @@ plugins {
 }
 
 sonar {
-  properties {
-    property "sonar.projectKey", "KeYProject_key"
-    property "sonar.organization", "keyproject"
-    property "sonar.host.url", "https://sonarcloud.io"
-  }
+    properties {
+        property "sonar.projectKey", "KeYProject_key"
+        property "sonar.organization", "keyproject"
+        property "sonar.host.url", "https://sonarcloud.io"
+    }
 }
 
 
@@ -85,50 +85,38 @@ subprojects {
     }
 
     dependencies {
-        implementation("org.slf4j:slf4j-api:2.0.16")
-        implementation("org.slf4j:slf4j-api:2.0.16")
-
-
-        compileOnly("org.jspecify:jspecify:1.0.0")
-        testCompileOnly("org.jspecify:jspecify:1.0.0")
-        def eisop_version = "3.42.0-eisop5"
-        compileOnly "io.github.eisop:checker-qual:$eisop_version"
-        compileOnly "io.github.eisop:checker-util:$eisop_version"
-        testCompileOnly "io.github.eisop:checker-qual:$eisop_version"
-        checkerFramework "io.github.eisop:checker-qual:$eisop_version"
-        checkerFramework "io.github.eisop:checker:$eisop_version"
-
-        testImplementation("org.assertj:assertj-core:3.27.3")
-        testImplementation("ch.qos.logback:logback-classic:1.5.15")
-        testImplementation 'org.junit.jupiter:junit-jupiter-api:5.11.4'
-        testImplementation 'org.junit.jupiter:junit-jupiter-params:5.11.4'
-        testImplementation project(':key.util')
+        implementation(libs.slf4j)
 
-        // test fixtures
-        testImplementation("com.fasterxml.jackson.dataformat:jackson-dataformat-yaml:2.18.2")
-        testImplementation("com.fasterxml.jackson.datatype:jackson-datatype-jsr310:2.18.2")
+        compileOnly(libs.jspecify)
+        testCompileOnly(libs.jspecify)
 
+        compileOnly(libs.eisopCheckerQual)
+        compileOnly(libs.eisopUtil)
+        testCompileOnly(libs.eisopCheckerQual)
+        checkerFramework(libs.eisopCheckerQual)
+        checkerFramework(libs.eisopChecker)
 
-
-        testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.11.4'
+        testImplementation(libs.bundles.testing)
+        testImplementation project(':key.util')
+        testRuntimeOnly(libs.junitEngine)
     }
 
-    tasks.withType(JavaCompile) {
+    tasks.withType(JavaCompile).configureEach {
         // Setting UTF-8 as the java source encoding.
         options.encoding = "UTF-8"
         // Setting the release to Java 21
         options.release = 21
     }
 
-    tasks.withType(Javadoc) {
+    tasks.withType(Javadoc).configureEach {
         failOnError = false
         options.addBooleanOption 'Xdoclint:none', true
         //options.verbose()
         options.encoding = 'UTF-8'
         options.addBooleanOption('html5', true)
     }
 
-    tasks.withType(Test) {//Configure all tests
+    tasks.withType(Test).configureEach {//Configure all tests
         systemProperty "test-resources", "src/test/resources"
         systemProperty "testcases", "src/test/resources/testcase"
         systemProperty "TACLET_PROOFS", "tacletProofs"
@@ -142,7 +130,7 @@ subprojects {
         maxParallelForks = 1 // weigl: test on master
     }
 
-    tasks.withType(Test) {
+    tasks.withType(Test).configureEach {
         useJUnitPlatform {
             includeEngines 'junit-jupiter'
         }
@@ -169,7 +157,7 @@ subprojects {
         }
     }
 
-    task testFast(type: Test) {
+    tasks.register('testFast', Test) {
         group "verification"
         useJUnitPlatform {
             excludeTags "slow", "performance", "interactive"
@@ -195,14 +183,14 @@ subprojects {
     // The following two tasks can be used to execute main methods from the project
     // The main class is set via "gradle -DmainClass=... execute --args ..."
     // see https://stackoverflow.com/questions/21358466/gradle-to-execute-java-class-without-modifying-build-gradle
-    task execute(type: JavaExec) {
+    tasks.register('execute', JavaExec) {
         description 'Execute main method from the project. Set main class via "gradle -DmainClass=... execute --args ..."'
         group "application"
         mainClass.set(System.getProperty('mainClass'))
         classpath = sourceSets.main.runtimeClasspath
     }
 
-    task executeInTests(type: JavaExec) {
+    tasks.register('executeInTests', JavaExec) {
         description 'Execute main method from the project (tests loaded). Set main class via "gradle -DmainClass=... execute --args ..."'
         group "application"
         mainClass.set(System.getProperty('mainClass'))
@@ -219,7 +207,7 @@ subprojects {
         ruleSets = ["category/java/errorprone.xml", "category/java/bestpractices.xml"]
     }
 
-    task pmdMainChanged(type: Pmd) {
+    tasks.register('pmdMainChanged', Pmd) {
         // Specify all files that should be checked
         def changedFiles = getChangedFiles()
         source pmdMain.source.filter { f -> f.getAbsoluteFile().toString() in changedFiles }
@@ -245,7 +233,7 @@ subprojects {
     }
 
 
-    task checkstyleMainChanged(type: Checkstyle) {
+    tasks.register('checkstyleMainChanged', Checkstyle) {
         // Specify all files that should be checked
         def changedFiles = getChangedFiles()
         source checkstyleMain.source.filter { f -> f.getAbsoluteFile().toString() in changedFiles }
@@ -273,20 +261,20 @@ subprojects {
     //         html.enabled = true
     //     }
     // }
-    tasks.withType(Pmd) {
+    tasks.withType(Pmd).configureEach {
         reports {
             xml.getRequired().set(true)
             html.getRequired().set(true)
         }
     }
 
-    task sourcesJar(type: Jar) {
+    tasks.register('sourcesJar', Jar) {
         description = 'Create a jar file with the sources from this project'
         from sourceSets.main.allJava
         archiveClassifier = 'sources'
     }
 
-    task javadocJar(type: Jar) {
+    tasks.register('javadocJar', Jar) {
         description = 'Create a jar file with the javadocs from this project'
         from javadoc
         archiveClassifier = 'javadoc'
@@ -491,15 +479,15 @@ subprojects {
     }
 }
 
-task start {
+tasks.register('start'){
     description "Use :key.ui:run instead"
     doFirst {
         println "Use :key.ui:run instead"
     }
 }
 
 // Generation of a JavaDoc across sub projects.
-task alldoc(type: Javadoc) {
+tasks.register('alldoc', Javadoc){
     group "documentation"
     description "Generate a JavaDoc across sub projects"
     def projects = subprojects
@@ -531,7 +519,7 @@ task alldoc(type: Javadoc) {
 }
 
 // Creates a jar file with the javadoc over all sub projects.
-task alldocJar(type: Zip) {
+tasks.register('alldocJar', Zip){
     dependsOn alldoc
     description 'Create a jar file with the javadoc over all sub projects'
     from alldoc

key.core/build.gradle

@@ -12,16 +12,11 @@ dependencies {
     api project(':key.ncore')
     //api group: group, name: 'recoderkey', version: '1.0'
     api project(':recoder')
-    implementation group: 'net.java.dev.javacc', name: 'javacc', version: '4.0'
-    implementation group: 'org.antlr', name: 'antlr-runtime', version: '3.5.3'
-    implementation group: 'antlr', name: 'antlr', version: '2.7.7'
 
-    javacc group: 'net.java.dev.javacc', name: 'javacc', version: '4.0'
-    antlr group: 'org.antlr', name: 'antlr', version: '3.5.3'   // use ANTLR version 3
-
-    antlr4 "org.antlr:antlr4:4.13.2"
-    api "org.antlr:antlr4-runtime:4.13.2"
-    //implementation group: 'com.google.guava', name: 'guava', version: '28.1-jre'
+    implementation(libs.javacc)
+    javacc(libs.javacc)
+    antlr4(libs.antlr)
+    api(libs.antlrRuntime)
 }
 
 // The target directory for JavaCC (parser generation)

key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java

@@ -9,7 +9,6 @@
 import java.nio.file.*;
 import java.util.*;
 import java.util.function.Consumer;
-import java.util.stream.Collectors;
 import java.util.stream.Stream;
 import java.util.zip.ZipFile;
 
@@ -33,12 +32,10 @@
 import de.uka.ilkd.key.speclang.SLEnvInput;
 import de.uka.ilkd.key.strategy.Strategy;
 import de.uka.ilkd.key.strategy.StrategyProperties;
-import de.uka.ilkd.key.util.ExceptionHandlerException;
 
 import org.key_project.util.collection.Pair;
 import org.key_project.util.java.IOUtil;
 
-import org.antlr.runtime.MismatchedTokenException;
 import org.jspecify.annotations.Nullable;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
@@ -348,51 +345,6 @@ protected void loadSelectedProof(LoadedPOContainer poContainer, ProofAggregate p
         }
     }
 
-    /**
-     * Find first 'non-wrapper' exception type in cause chain.
-     */
-    private Throwable unwrap(Throwable e) {
-        while (e instanceof ExceptionHandlerException || e instanceof ProblemLoaderException) {
-            e = e.getCause();
-        }
-        return e;
-    }
-
-    /**
-     * Tries to recover parser errors and make them human-readable, rewrap them into
-     * ProblemLoaderExceptions.
-     */
-    protected ProblemLoaderException recoverParserErrorMessage(Exception e) {
-        // try to resolve error message
-        final Throwable c0 = unwrap(e);
-        if (c0 instanceof org.antlr.runtime.RecognitionException re) {
-            final org.antlr.runtime.Token occurrence = re.token; // may be null
-            if (c0 instanceof org.antlr.runtime.MismatchedTokenException) {
-                if (c0 instanceof org.antlr.runtime.MissingTokenException mte) {
-                    // TODO: other commonly missed tokens
-                    final String readable = missedErrors.get(mte.expecting);
-                    final String token = readable == null ? "token id " + mte.expecting : readable;
-                    final String msg = "Syntax error: missing " + token
-                        + (occurrence == null ? "" : " at " + occurrence.getText()) + " statement ("
-                        + mte.input.getSourceName() + ":" + mte.line + ")";
-                    return new ProblemLoaderException(this, msg, mte);
-                    // TODO other ANTLR exceptions
-                } else {
-                    final org.antlr.runtime.MismatchedTokenException mte =
-                        (MismatchedTokenException) c0;
-                    final String genericMsg = "expected " + mte.expecting + ", but found " + mte.c;
-                    final String readable =
-                        mismatchErrors.get(new Pair<>(mte.expecting, mte.c));
-                    final String msg = "Syntax error: " + (readable == null ? genericMsg : readable)
-                        + " (" + mte.input.getSourceName() + ":" + mte.line + ")";
-                    return new ProblemLoaderException(this, msg, mte);
-                }
-            }
-        }
-        // default
-        return new ProblemLoaderException(this, "Loading proof input failed", e);
-    }
-
     /**
      * Creates a new FileRepo (with or without consistency) based on the settings.
      *
@@ -428,7 +380,7 @@ protected EnvInput createEnvInput(FileRepo fileRepo) throws IOException {
 
         if (filename.endsWith(".java")) {
             // java file, probably enriched by specifications
-            SLEnvInput ret = null;
+            SLEnvInput ret;
             if (file.getParentFile() == null) {
                 ret = new SLEnvInput(".", classPath, bootClassPath, profileOfNewProofs, includes);
             } else {
@@ -453,11 +405,11 @@ protected EnvInput createEnvInput(FileRepo fileRepo) throws IOException {
                 try (ZipFile bundle = new ZipFile(file)) {
                     proofs = bundle.stream().filter(e -> !e.isDirectory())
                             .filter(e -> e.getName().endsWith(".proof"))
-                            .map(e -> Paths.get(e.getName())).collect(Collectors.toList());
+                            .map(e -> Paths.get(e.getName())).toList();
                 }
                 if (!proofs.isEmpty()) {
                     // load first proof found in file
-                    proofFilename = proofs.get(0).toFile();
+                    proofFilename = proofs.getFirst().toFile();
                 } else {
                     // no proof found in bundle!
                     throw new IOException("The bundle contains no proof to load!");

key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java

@@ -36,7 +36,7 @@
 import org.key_project.util.collection.ImmutableSLList;
 import org.key_project.util.collection.Pair;
 
-import org.antlr.runtime.Token;
+import org.antlr.v4.runtime.Token;
 import org.jspecify.annotations.NonNull;
 import org.jspecify.annotations.Nullable;
 import org.slf4j.Logger;

key.ncore/build.gradle

@@ -1,16 +1,17 @@
 plugins {
 }
 
-description "Generic data strutures for terms and formulas without dependencies to a specific target programming language"
+description "Generic data structures for terms and formulas without " +
+        "dependencies to a specific target programming language"
 
 configurations { }
 
 dependencies {
     api project(':key.util')
-    implementation 'org.jspecify:jspecify:1.0.0'
+    implementation(libs.jspecify)
 }
 
-tasks.withType(Test) {
+tasks.withType(Test).configureEach {
     enableAssertions = true
 }
 

key.ui/build.gradle

@@ -20,13 +20,13 @@ dependencies {
     implementation project(":key.core.symbolic_execution")
     implementation project(":key.removegenerics")
 
-    api 'com.miglayout:miglayout-swing:11.4.2'
+    api(libs.miglayout)
 
     //logging implementation used by the slf4j
-    implementation 'ch.qos.logback:logback-classic:1.5.15'
+    implementation(libs.logback)
 
-    api 'org.key-project:docking-frames-common:1.1.3p1'
-    api 'org.key-project:docking-frames-core:1.1.3p1'
+    api(libs.dockingFramesCommon)
+    api(libs.dockingFramesCore)
 
     runtimeOnly project(":keyext.ui.testgen")
     runtimeOnly project(":keyext.caching")
@@ -35,7 +35,7 @@ dependencies {
     runtimeOnly project(":keyext.proofmanagement")
 }
 
-task createExamplesZip(type: Zip) {
+tasks.register('createExamplesZip', Zip) {
     description 'Create "examples.zip" containing all KeY examples'
     destinationDirectory = file("$buildDir/resources/main/")
     archiveFileName = "examples.zip"
@@ -71,7 +71,7 @@ run {
     jvmArgs += "-Dsun.awt.disablegrab=true"
 }
 
-task runWithProfiler(type: JavaExec) {
+tasks.register('runWithProfiler', JavaExec) {
     group("application")
     description("""Run key.ui with flight recoder enabled. 
                    See https://www.baeldung.com/java-flight-recorder-monitoring for a how to.""")

key.util/build.gradle

@@ -1,7 +1,7 @@
 description "Utility library of the key-project"
 
 dependencies {
-    implementation("org.jspecify:jspecify:1.0.0")
+    implementation(libs.jspecify)
 }
 
 checkerFramework {

keyext.proofmanagement/build.gradle

@@ -9,7 +9,7 @@ dependencies {
     implementation project(':key.core')
     implementation project(':key.ui')
 
-    implementation group: 'org.antlr', name: 'ST4', version: '4.3.4'
+    implementation(libs.stringtemplate)
 }
 
 application {

settings.gradle

@@ -1,3 +1,5 @@
+// https://docs.gradle.org/current/userguide/version_catalogs.html#sec:importing-catalog-from-file
+
 include "key.util"
 include "key.ui"
 include "key.ncore"