Merge remote-tracking branch 'origin/main' into weigl/key-javaparser3

# By Drodt (29) and others
# Via Drodt (5) and GitHub (5)
* origin/main: (32 commits)
  Add containsGenerics method to sort
  Simplify
  Remove tokens file
  Fix inst with sort depending fn
  Fix parsing of proof files
  Fix proof loading/storing when generics are instantiated in NoFindTaclets
  Some documentation
  Fix test classes
  Slightly improve error messages
  Fix taclets for datatypes w/ polymorphic params
  Prepare datatype handling
  Spotless
  Finish example; slight fixes
  Fix fns and preds parsing; add test
  Fix SortDepFn and add test
  Start on polymorphic sorts and functions
  directly creating issues in Github inside KeY
  Bump the gradle-deps group across 1 directory with 9 updates
  Bump actions/upload-artifact in the github-actions-deps group
  Fix inst with sort depending fn
  ...

# Conflicts:
#	build.gradle
#	key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortInstantiations.java

Author: wadoon

.github/workflows/nightlydeploy.yml

@@ -57,13 +57,13 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Upload Javadoc
-        uses: actions/upload-artifact@v6
+        uses: actions/upload-artifact@v7
         with:
           name: javadoc
           path: "javadoc.tar.xz"
 
       - name: Upload ShadowJar
-        uses: actions/upload-artifact@v6
+        uses: actions/upload-artifact@v7
         with:
           name: shadowjars
           path: "*/build/libs/*-exe.jar"

.github/workflows/opttest.yml

@@ -30,7 +30,7 @@ jobs:
         run: ./gradlew --continue ${{ matrix.tests }}
 
       - name: Upload test results
-        uses: actions/upload-artifact@v6
+        uses: actions/upload-artifact@v7
         if: success() || failure()
         with:
           name: test-results-${{ matrix.tests }}

.github/workflows/tests.yml

@@ -60,7 +60,7 @@ jobs:
         run: ./gradlew --continue -DjacocoEnabled=true :${{ matrix.modules }}:test
 
       - name: Upload test results
-        uses: actions/upload-artifact@v6
+        uses: actions/upload-artifact@v7
         if: success() || failure()
         with:
           name: test-results-${{ matrix.os }}-${{ matrix.modules }}
@@ -101,7 +101,7 @@ jobs:
         run: ./gradlew --continue ${{ matrix.test }}
 
       - name: Upload test results
-        uses: actions/upload-artifact@v6
+        uses: actions/upload-artifact@v7
         if: success() || failure()        # run this step even if previous step failed
         with:
           name: test-results-${{ matrix.test }}

.github/workflows/tests_winmac.yml

@@ -46,7 +46,7 @@ jobs:
         run: ./gradlew --continue -x :key.core.symbolic_execution:test -x :key.core.proof_references:test test
 
       - name: Upload test results
-        uses: actions/upload-artifact@v6
+        uses: actions/upload-artifact@v7
         if: success() || failure()
         with:
           name: unit-test-results-${{matrix.test}}-${{ matrix.os }}-${{ matrix.java }}
@@ -86,7 +86,7 @@ jobs:
         run: ./gradlew --continue ${{ matrix.test }}
 
       - name: Upload test results
-        uses: actions/upload-artifact@v6
+        uses: actions/upload-artifact@v7
         if: success() || failure()        # run this step even if a previous step failed
         with:
           name: integration-test-results-${{matrix.test}}-${{ matrix.os }}-${{ matrix.java }}

build.gradle

@@ -8,26 +8,17 @@ plugins {
     id("eclipse")  //support for Eclipse
 
     // Code formatting
-    id "com.diffplug.spotless" version "8.2.1"
+    id "com.diffplug.spotless" version "8.3.0"
 
     // EISOP Checker Framework
     id "org.checkerframework" version "0.6.61"
 
-    id("org.sonarqube") version "7.2.2.6593"
+    id("org.sonarqube") version "7.2.3.7755"
 
     // Plugin for publishing via the new Nexus API
     id "io.github.gradle-nexus.publish-plugin" version "2.0.0"
-
-    id 'test-report-aggregation'
 }
 
-reporting {
-    reports {
-        testAggregateTestReport(AggregateTestReport) {
-            testSuiteName = "test"
-        }
-    }
-}
 
 // Configure this project for use inside IntelliJ:
 idea {
@@ -73,7 +64,7 @@ subprojects {
 
     dependencies {
         implementation("org.slf4j:slf4j-api:2.0.17")
-        testImplementation("ch.qos.logback:logback-classic:1.5.27")
+        testImplementation("ch.qos.logback:logback-classic:1.5.32")
 
 
         compileOnly("org.jspecify:jspecify:1.0.0")
@@ -85,11 +76,11 @@ subprojects {
         checkerFramework "io.github.eisop:checker-qual:$eisop_version"
         checkerFramework "io.github.eisop:checker:$eisop_version"
 
-        testImplementation("ch.qos.logback:logback-classic:1.5.27")
+        testImplementation("ch.qos.logback:logback-classic:1.5.32")
         testImplementation("org.assertj:assertj-core:3.27.7")
-        testImplementation("ch.qos.logback:logback-classic:1.5.27")
+        testImplementation("ch.qos.logback:logback-classic:1.5.32")
 
-        testImplementation(platform("org.junit:junit-bom:5.14.2"))
+        testImplementation(platform("org.junit:junit-bom:5.14.3"))
         testImplementation ("org.junit.jupiter:junit-jupiter-api")
         testImplementation ("org.junit.jupiter:junit-jupiter-params")
         testRuntimeOnly ("org.junit.jupiter:junit-jupiter-engine")
@@ -98,8 +89,8 @@ subprojects {
         testImplementation project(':key.util')
 
         // test fixtures
-        testImplementation("com.fasterxml.jackson.dataformat:jackson-dataformat-yaml:2.21.0")
-        testImplementation("com.fasterxml.jackson.datatype:jackson-datatype-jsr310:2.21.0")
+        testImplementation("com.fasterxml.jackson.dataformat:jackson-dataformat-yaml:2.21.1")
+        testImplementation("com.fasterxml.jackson.datatype:jackson-datatype-jsr310:2.21.1")
 
         testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine'
     }

gradle/wrapper/gradle-wrapper.jar

@@ -1,6 +1,6 @@
 distributionBase=GRADLE_USER_HOME
 distributionPath=wrapper/dists
-distributionUrl=https\://services.gradle.org/distributions/gradle-9.3.1-bin.zip
+distributionUrl=https\://services.gradle.org/distributions/gradle-9.4.0-bin.zip
 networkTimeout=10000
 validateDistributionUrl=true
 zipStoreBase=GRADLE_USER_HOME

gradle/wrapper/gradle-wrapper.properties

@@ -10,5 +10,5 @@ application {
 
 dependencies {
     implementation project(":key.core")
-    implementation 'ch.qos.logback:logback-classic:1.5.27'
+    implementation 'ch.qos.logback:logback-classic:1.5.32'
 }

gradlew

@@ -381,6 +381,8 @@ GREATEREQUAL
 :   '>' '=' | '\u2265'
       ;
 
+OPENTYPEPARAMS : '<[';
+CLOSETYPEPARAMS : ']>';
 
 WS:  [ \t\n\r\u00a0]+ -> channel(HIDDEN); //U+00A0 = non breakable whitespace
 STRING_LITERAL:'"' ('\\' . | ~( '"' | '\\') )* '"' ;