Merge remote-tracking branch 'origin/main' into pfeifer/3683hidePackageOptionFix

# By Alexander Weigl (48) and others
# Via GitHub (35) and others
* origin/main: (117 commits)
  Add containsGenerics method to sort
  spotless
  look in top-level project.key for includes to allow for dl escapes in Java files
  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
  ...

# Conflicts:
#	key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java

Author: wadoon

.github/workflows/gradle-publish.yml

@@ -1,4 +1,4 @@
-name: Nightly Deployer of Weekly Builds
+name: Weekly Builds of KeY
 
 on:
   workflow_dispatch:
@@ -9,32 +9,65 @@ permissions:
   contents: write
   id-token: write
 
+env:
+  JAVA_VERSION: 21
+
 
 jobs:
-  deploy:
+  build:
     runs-on: ubuntu-latest
     steps:
-      # weigl: Should produce fancier release notes, but needs some configuration
-      # # https://github.com/marketplace/actions/release-changelog-builder
-      # - name: "Build Changelog"
-      #   id: build_changelog
-      #   uses: mikepenz/release-changelog-builder-action@v3.7.0
-      #   with:
-      #     ignorePreReleases: true
-      #     fetchReviewers: true
-
       - uses: actions/checkout@v6
-      - name: Set up JDK 21
+      - name: Set up JDK ${{ env.JAVA_VERSION }}
         uses: actions/setup-java@v5
         with:
-          java-version: 21
+          java-version: ${{ env.JAVA_VERSION }}
           distribution: 'temurin'
+          cache: 'gradle'
 
       - name: Setup Gradle
         uses: gradle/actions/setup-gradle@v5
+
       - name: Build with Gradle
         run: ./gradlew --parallel assemble
 
+  doc:
+    needs: [build]
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v6
+      - name: Set up JDK ${{ env.JAVA_VERSION }}
+        uses: actions/setup-java@v5
+        with:
+          java-version: ${{ env.JAVA_VERSION }}
+          distribution: 'temurin'
+          cache: 'gradle'
+
+      - name: Setup Gradle
+        uses: gradle/actions/setup-gradle@v5
+
+      - name: Build Documentation with Gradle
+        run: ./gradlew alldoc
+
+      - name: Package
+        run: tar cvf key-javadoc.tar.xz build/docs/javadoc
+
+  deploy:
+    needs: [build, doc]
+    runs-on: ubuntu-latest
+    steps:
+      - name: Upload Javadoc
+        uses: actions/upload-artifact@v7
+        with:
+          name: javadoc
+          path: "javadoc.tar.xz"
+
+      - name: Upload ShadowJar
+        uses: actions/upload-artifact@v7
+        with:
+          name: shadowjars
+          path: "*/build/libs/*-exe.jar"
+
       - name: Delete previous nightly release
         continue-on-error: true
         env:
@@ -50,3 +83,25 @@ jobs:
           gh release create --generate-notes --title "Nightly Release" \
              --prerelease --notes-start-tag KEY-2.12.3 \
              nightly key.ui/build/libs/key-*-exe.jar
+
+  deploy-maven:
+    needs: [ build, doc ]
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v6
+      - name: Set up JDK ${{ env.JAVA_VERSION }}
+        uses: actions/setup-java@v5
+        with:
+          java-version: ${{ env.JAVA_VERSION }}
+          distribution: 'temurin'
+          cache: 'gradle'
+
+      - name: Setup Gradle
+        uses: gradle/actions/setup-gradle@v5
+
+      - name: Upload to SNAPSHOT repository
+        run: ./gradlew publishMavenJavaPublicationToKEYLABRepository
+        env:
+          BUILD_NUMBER: "SNAPSHOT"
+          GITLAB_DEPLOY_TOKEN: ${{ secrets.GITLAB_DEPLOY_TOKEN }}
+

.github/workflows/javadoc.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/nightlydeploy.yml

@@ -61,7 +61,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 }}
@@ -80,7 +80,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        test: [ testProveRules, testRunAllFunProofs, testRunAllInfProofs ]
+        test: [ testProveRules, testRunAllFunProofs, testRunAllInfProofs, testRunAllWdProofs ]
         os: [ ubuntu-latest ]
         java: [ 21 ]
     runs-on: ${{ matrix.os }}
@@ -102,7 +102,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/opttest.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 }}