From facf623fc59cdc28a54e603cfb405deed8d2224d Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Tue, 30 Dec 2025 04:47:54 +0100 Subject: [PATCH 1/4] update optional test. colon not allowed in artifact names --- .github/workflows/opttest.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/opttest.yml b/.github/workflows/opttest.yml index 768a3663e4..26528e5f9d 100644 --- a/.github/workflows/opttest.yml +++ b/.github/workflows/opttest.yml @@ -13,7 +13,7 @@ jobs: matrix: os: [ubuntu-latest, windows-latest] java: [21] - tests: [":key.core.proof_references:test", ":key.core.symbolic_execution:test"] + name: ["proof_references", "symbolic_execution"] runs-on: ${{matrix.os}} steps: - uses: actions/checkout@v6 @@ -27,13 +27,13 @@ jobs: - name: Setup Gradle uses: gradle/actions/setup-gradle@v5 - name: Test with Gradle - run: ./gradlew --continue ${{ matrix.tests }} + run: ./gradlew --continue :key.core.${{ matrix.name }}:test - name: Upload test results uses: actions/upload-artifact@v6 if: success() || failure() with: - name: test-results-${{ matrix.tests }} + name: test-results-${{ matrix.name }} path: | **/build/test-results/*/*.xml **/build/reports/ From 223afb422eebca49ebadb7af6a4f553dfb5b84a0 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Tue, 30 Dec 2025 04:59:59 +0100 Subject: [PATCH 2/4] Fix and extend the broad release tests * setup-smt updated to version 0.3.0 to support more z3/cvc5 versions * executes the smt tests * execute tests with different z3/cvc5 on different platform for different java versions # Conflicts: # .github/workflows/sonarqube.yml # .github/workflows/tests_winmac.yml --- .github/old_workflows/deletecache.yml | 34 - .github/old_workflows/labeler.yml | 14 - .github/old_workflows/mega-lint.yml | 80 - .github/old_workflows/test-report.yml | 16 - .github/qodana.starter.full.xml | 7016 ------------------------- .github/workflows/release-tests.yml | 158 + .github/workflows/sonarqube.yml | 49 - .github/workflows/tests.yml | 1 + .github/workflows/tests_winmac.yml | 98 - 9 files changed, 159 insertions(+), 7307 deletions(-) delete mode 100644 .github/old_workflows/deletecache.yml delete mode 100644 .github/old_workflows/labeler.yml delete mode 100644 .github/old_workflows/mega-lint.yml delete mode 100644 .github/old_workflows/test-report.yml delete mode 100644 .github/qodana.starter.full.xml create mode 100644 .github/workflows/release-tests.yml delete mode 100644 .github/workflows/sonarqube.yml delete mode 100644 .github/workflows/tests_winmac.yml diff --git a/.github/old_workflows/deletecache.yml b/.github/old_workflows/deletecache.yml deleted file mode 100644 index 8376a396fc..0000000000 --- a/.github/old_workflows/deletecache.yml +++ /dev/null @@ -1,34 +0,0 @@ -name: cleanup caches by a branch -on: - pull_request: - types: - - closed - workflow_dispatch: - -jobs: - cleanup: - runs-on: ubuntu-latest - steps: - - name: Check out code - uses: actions/checkout@v3 - - - name: Cleanup - run: | - gh extension install actions/gh-actions-cache - - REPO=$ - BRANCH=$ - - echo "Fetching list of cache key" - cacheKeysForPR=$(gh actions-cache list -R $REPO -B $BRANCH | cut -f 1 ) - - ## Setting this to not fail the workflow while deleting cache keys. - set +e - echo "Deleting caches..." - for cacheKey in $cacheKeysForPR - do - gh actions-cache delete $cacheKey -R $REPO -B $BRANCH --confirm - done - echo "Done" - env: - GH_TOKEN: $ diff --git a/.github/old_workflows/labeler.yml b/.github/old_workflows/labeler.yml deleted file mode 100644 index 41134d5a18..0000000000 --- a/.github/old_workflows/labeler.yml +++ /dev/null @@ -1,14 +0,0 @@ -name: "Pull Request Labeler" -on: [pull_request, pull_request_target] - -jobs: - triage: - permissions: - contents: read - pull-requests: write - runs-on: ubuntu-latest - steps: - - uses: actions/labeler@v4 - with: - sync-labels: true - repo-token: "${{ secrets.GITHUB_TOKEN }}" diff --git a/.github/old_workflows/mega-lint.yml b/.github/old_workflows/mega-lint.yml deleted file mode 100644 index 93a3b2f001..0000000000 --- a/.github/old_workflows/mega-lint.yml +++ /dev/null @@ -1,80 +0,0 @@ -name: MegaLinter - -on: - # Trigger mega-linter at every push. Action will also be visible from Pull Requests to main - push: # Comment this line to trigger action only on pull-requests (not recommended if you don't pay for GH Actions) - pull_request: - branches: [master, main] - -env: # Comment env block if you do not want to apply fixes - # Apply linter fixes configuration - APPLY_FIXES: all # When active, APPLY_FIXES must also be defined as environment variable (in github/workflows/mega-linter.yml or other CI tool) - APPLY_FIXES_EVENT: pull_request # Decide which event triggers application of fixes in a commit or a PR (pull_request, push, all) - APPLY_FIXES_MODE: commit # If APPLY_FIXES is used, defines if the fixes are directly committed (commit) or posted in a PR (pull_request) - -concurrency: - group: ${{ github.ref }}-${{ github.workflow }} - cancel-in-progress: true - -jobs: - build: - name: MegaLinter - runs-on: ubuntu-latest - steps: - # Git Checkout - - name: Checkout Code - uses: actions/checkout@v3 - with: - token: ${{ secrets.PAT || secrets.GITHUB_TOKEN }} - fetch-depth: 0 # If you use VALIDATE_ALL_CODEBASE = true, you can remove this line to improve performances - - # MegaLinter - - name: MegaLinter - id: ml - # You can override MegaLinter flavor used to have faster performances - # More info at https://megalinter.github.io/flavors/ - uses: oxsecurity/megalinter@v6 - env: - # All available variables are described in documentation - # https://megalinter.github.io/configuration/ - VALIDATE_ALL_CODEBASE: ${{ github.event_name == 'push' && github.ref == 'refs/heads/main' }} # Validates all source when push on main, else just the git diff with main. Override with true if you always want to lint all sources - GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} - # ADD YOUR CUSTOM ENV VARIABLES HERE OR DEFINE THEM IN A FILE .mega-linter.yml AT THE ROOT OF YOUR REPOSITORY - # DISABLE: COPYPASTE,SPELL # Uncomment to disable copy-paste and spell checks - - # Upload MegaLinter artifacts - - name: Archive production artifacts - if: ${{ success() }} || ${{ failure() }} - uses: actions/upload-artifact@v3 - with: - name: MegaLinter reports - path: | - megalinter-reports - mega-linter.log - - # Create pull request if applicable (for now works only on PR from same repository, not from forks) - - name: Create Pull Request with applied fixes - id: cpr - if: steps.ml.outputs.has_updated_sources == 1 && (env.APPLY_FIXES_EVENT == 'all' || env.APPLY_FIXES_EVENT == github.event_name) && env.APPLY_FIXES_MODE == 'pull_request' && (github.event_name == 'push' || github.event.pull_request.head.repo.full_name == github.repository) && !contains(github.event.head_commit.message, 'skip fix') - uses: peter-evans/create-pull-request@v4 - with: - token: ${{ secrets.PAT || secrets.GITHUB_TOKEN }} - commit-message: "[MegaLinter] Apply linters automatic fixes" - title: "[MegaLinter] Apply linters automatic fixes" - labels: bot - - name: Create PR output - if: steps.ml.outputs.has_updated_sources == 1 && (env.APPLY_FIXES_EVENT == 'all' || env.APPLY_FIXES_EVENT == github.event_name) && env.APPLY_FIXES_MODE == 'pull_request' && (github.event_name == 'push' || github.event.pull_request.head.repo.full_name == github.repository) && !contains(github.event.head_commit.message, 'skip fix') - run: | - echo "Pull Request Number - ${{ steps.cpr.outputs.pull-request-number }}" - echo "Pull Request URL - ${{ steps.cpr.outputs.pull-request-url }}" - - # Push new commit if applicable (for now works only on PR from same repository, not from forks) - - name: Prepare commit - if: steps.ml.outputs.has_updated_sources == 1 && (env.APPLY_FIXES_EVENT == 'all' || env.APPLY_FIXES_EVENT == github.event_name) && env.APPLY_FIXES_MODE == 'commit' && github.ref != 'refs/heads/main' && (github.event_name == 'push' || github.event.pull_request.head.repo.full_name == github.repository) && !contains(github.event.head_commit.message, 'skip fix') - run: sudo chown -Rc $UID .git/ - - name: Commit and push applied linter fixes - if: steps.ml.outputs.has_updated_sources == 1 && (env.APPLY_FIXES_EVENT == 'all' || env.APPLY_FIXES_EVENT == github.event_name) && env.APPLY_FIXES_MODE == 'commit' && github.ref != 'refs/heads/main' && (github.event_name == 'push' || github.event.pull_request.head.repo.full_name == github.repository) && !contains(github.event.head_commit.message, 'skip fix') - uses: stefanzweifel/git-auto-commit-action@v4 - with: - branch: ${{ github.event.pull_request.head.ref || github.head_ref || github.ref }} - commit_message: "[MegaLinter] Apply linters fixes" diff --git a/.github/old_workflows/test-report.yml b/.github/old_workflows/test-report.yml deleted file mode 100644 index 4fc333c65f..0000000000 --- a/.github/old_workflows/test-report.yml +++ /dev/null @@ -1,16 +0,0 @@ -name: 'Test Report' -on: - workflow_run: - workflows: ['CI'] # runs after CI workflow - types: - - completed -jobs: - report: - runs-on: ubuntu-latest - steps: - - uses: dorny/test-reporter@v1 - with: - artifact: test-results # artifact name - name: JUnit Tests # Name of the check run which will be created - path: '*.xml' # Path to test results (inside artifact .zip) - reporter: java-junit # Format of test results diff --git a/.github/qodana.starter.full.xml b/.github/qodana.starter.full.xml deleted file mode 100644 index 1b7e1c7dc3..0000000000 --- a/.github/qodana.starter.full.xml +++ /dev/null @@ -1,7016 +0,0 @@ - - - - \ No newline at end of file diff --git a/.github/workflows/release-tests.yml b/.github/workflows/release-tests.yml new file mode 100644 index 0000000000..e9773a670a --- /dev/null +++ b/.github/workflows/release-tests.yml @@ -0,0 +1,158 @@ +name: Broad Release Tests + +on: + workflow_dispatch: + schedule: + - cron: '0 5 * * 1' # every monday morning + +env: + z3: '4.13.4' # default z3 version + cvc5: '1.3.2' # default cvc5 version + + +jobs: + unit-tests: + strategy: + fail-fast: true + matrix: + os: [ macos-latest, ubuntu-latest, windows-latest ] + java: [ 21, 25 ] + continue-on-error: false + runs-on: ${{ matrix.os }} + env: + GH_TOKEN: ${{ github.token }} + steps: + - uses: actions/checkout@v6 + + - name: Set up JDK ${{matrix.java}} + uses: actions/setup-java@v5 + with: + java-version: ${{ matrix.java }} + distribution: 'temurin' + cache: 'gradle' + + - name: Setup SMT solvers + uses: keyproject/setup-smt@v0 + with: + cvc5Version: ${{ env.cvc5 }} + z3Version: ${{ env.z3 }} + + - name: z3 version + run: z3 --version + + - name: cvc5 version + run: cvc5 --version + + - name: Setup Gradle + uses: + gradle/actions/setup-gradle@v5 + + - name: Test mandatory modules with Gradle + run: ./gradlew test --continue -x :key.core.symbolic_execution:test -x :key.core.proof_references:test + + - name: Test optional modules with Gradle + run: ./gradlew :key.core.symbolic_execution:test -x :key.core.proof_references:test + + - name: Upload test results + uses: actions/upload-artifact@v6 + if: success() || failure() + with: + name: unit-test-results-${{matrix.test}}-${{ matrix.os }}-${{ matrix.java }} + path: | + **/build/test-results/*/*.xml + **/build/reports/ + !**/jacocoTestReport.xml + + + + integration-tests: + env: + GH_TOKEN: ${{ github.token }} + continue-on-error: false + strategy: + fail-fast: true + matrix: + test: [ testProveRules, testRunAllFunProofs, testRunAllInfProofs, testProveSMTLemmas, testStrictSMT ] + os: [ macos-latest, ubuntu-latest, windows-latest ] + java: [ 21, 25 ] + z3: [ '4.13.4', '4.14.1', '4.15.4' ] + cvc5: [ '1.3.2', '1.2.1' ] + + runs-on: ${{ matrix.os }} + steps: + - uses: actions/checkout@v6 + - name: Set up JDK ${{matrix.java}} + uses: actions/setup-java@v5 + with: + java-version: ${{ matrix.java }} + distribution: 'temurin' + cache: 'gradle' + + - name: Setup SMT solvers + uses: keyproject/setup-smt@v0 + with: + cvc5Version: ${{ env.cvc5 }} + z3Version: ${{ env.z3 }} + + - name: Setup Gradle + uses: gradle/actions/setup-gradle@v5 + + - name: "Running tests: ${{ matrix.test }}" + run: ./gradlew --continue ${{ matrix.test }} + + - name: Upload test results + uses: actions/upload-artifact@v6 + if: success() || failure() # run this step even if a previous step failed + with: + name: integration-test-results-${{matrix.test}}-${{ matrix.os }}-${{ matrix.java }} + path: | + **/build/test-results/*/*.xml + key.core/build/reports/runallproofs/* + **/build/reports/ + !**/jacocoTestReport.xml + + smt-tests: + env: + GH_TOKEN: ${{ github.token }} + continue-on-error: false + strategy: + fail-fast: true + matrix: + test: [ testProveSMTLemmas, testStrictSMT ] + os: [ macos-latest, ubuntu-latest, windows-latest ] + java: [ 21 ] + z3: [ '4.13.4', '4.14.1', '4.15.4' ] + cvc5: [ '1.3.2', '1.2.1' ] + runs-on: ${{ matrix.os }} + steps: + - uses: actions/checkout@v6 + - name: Set up JDK ${{matrix.java}} + uses: actions/setup-java@v5 + with: + java-version: ${{ matrix.java }} + distribution: 'temurin' + cache: 'gradle' + + - name: Setup SMT solvers + uses: keyproject/setup-smt@v0.3.0 + with: + cvc5Version: ${{ matrix.cvc5 }} + z3Version: ${{ matrix.z3 }} + + - name: Setup Gradle + uses: gradle/actions/setup-gradle@v5 + + - name: "Running tests: ${{ matrix.test }}" + run: ./gradlew --continue ${{ matrix.test }} + + - name: Upload test results + uses: actions/upload-artifact@v6 + if: success() || failure() # run this step even if a previous step failed + with: + name: smt-test-results-${{matrix.test}}-${{ matrix.os }}-${{ matrix.java }}-${{matrix.z3}}-${{matrix.cvc5}} + path: | + **/build/test-results/*/*.xml + key.core/build/reports/runallproofs/* + **/build/reports/ + !**/jacocoTestReport.xml + diff --git a/.github/workflows/sonarqube.yml b/.github/workflows/sonarqube.yml deleted file mode 100644 index e861d23b23..0000000000 --- a/.github/workflows/sonarqube.yml +++ /dev/null @@ -1,49 +0,0 @@ -## Copied from SonarCloud - -name: SonarCloud -on: - push: - branches: - - main - pull_request: - types: [opened, synchronize, reopened] - -jobs: - build: - name: Build and analyze - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@v6 - with: - fetch-depth: 0 # Shallow clones should be disabled for a better relevancy of analysis - - name: Set up JDK 21 - uses: actions/setup-java@v5 - with: - java-version: 21 - distribution: 'zulu' - - name: Cache SonarCloud packages - uses: actions/cache@v5 - with: - path: ~/.sonar/cache - key: ${{ runner.os }}-sonar - restore-keys: ${{ runner.os }}-sonar - - name: Cache Gradle packages - uses: actions/cache@v5 - with: - path: ~/.gradle/caches - key: ${{ runner.os }}-gradle-${{ hashFiles('**/*.gradle') }} - restore-keys: ${{ runner.os }}-gradle - - - name: Generate and submit dependency graph - uses: gradle/actions/dependency-submission@v5 - with: - build-scan-publish: true - build-scan-terms-of-use-url: "https://gradle.com/terms-of-service" - build-scan-terms-of-use-agree: "yes" - - - name: Build and analyze - env: - GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} # Needed to get PR information, if any - SONAR_TOKEN: ${{ secrets.SONAR_TOKEN }} - GRADLE_OPTS: "-Xmx6g -XX:MaxMetaspaceSize=512m -Dfile.encoding=UTF-8" - run: ./gradlew --parallel --continue -DjacocoEnabled=true -x :key.core.symbolic_execution:test -x :key.core.proof_references:test classes testClasses :key.util:test jacocoTestReport sonar \ No newline at end of file diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 51910bfe92..0dbf0b6dd3 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -8,6 +8,7 @@ on: branches: - "main" - "KeY-*" + - "releases/*" merge_group: permissions: diff --git a/.github/workflows/tests_winmac.yml b/.github/workflows/tests_winmac.yml deleted file mode 100644 index 497019b40e..0000000000 --- a/.github/workflows/tests_winmac.yml +++ /dev/null @@ -1,98 +0,0 @@ -name: Broad Release Tests - -on: - workflow_dispatch: - schedule: - - cron: '0 5 * * 1' # every monday morning - -permissions: - checks: write - -jobs: - unit-tests: - strategy: - fail-fast: false - matrix: - os: [macos-latest, ubuntu-latest, windows-latest] - java: [21,23] - continue-on-error: true - runs-on: ${{ matrix.os }} - env: - GH_TOKEN: ${{ github.token }} - steps: - - uses: actions/checkout@v6 - - - name: Setup SMT solvers - uses: keyproject/setup-smt@v0 - - - name: z3 version - run: z3 --version - - - name: cvc5 version - run: cvc5 --version - - - - name: Set up JDK ${{matrix.java}} - uses: actions/setup-java@v5 - with: - java-version: ${{ matrix.java }} - distribution: 'corretto' - cache: 'gradle' - - - name: Setup Gradle - uses: - gradle/actions/setup-gradle@v5 - - name: Test with Gradle - 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 - if: success() || failure() - with: - name: unit-test-results-${{matrix.test}}-${{ matrix.os }}-${{ matrix.java }} - path: | - **/build/test-results/*/*.xml - **/build/reports/ - !**/jacocoTestReport.xml - - - integration-tests: - env: - GH_TOKEN: ${{ github.token }} - continue-on-error: true - strategy: - fail-fast: false - matrix: - test: [testProveRules, testRunAllFunProofs, testRunAllInfProofs] - os: [ macos-latest, ubuntu-latest, windows-latest ] - java: [21] - runs-on: ${{ matrix.os }} - steps: - - uses: actions/checkout@v6 - - - name: Setup SMT solvers - uses: keyproject/setup-smt@v0 - - - name: Set up JDK 21 - uses: actions/setup-java@v5 - with: - java-version: ${{ matrix.java }} - distribution: 'corretto' - cache: 'gradle' - - - name: Setup Gradle - uses: gradle/actions/setup-gradle@v5 - - name: "Running tests: ${{ matrix.test }}" - run: ./gradlew --continue ${{ matrix.test }} - - - name: Upload test results - uses: actions/upload-artifact@v6 - if: success() || failure() # run this step even if a previous step failed - with: - name: integration-test-results-${{matrix.test}}-${{ matrix.os }}-${{ matrix.java }} - path: | - **/build/test-results/*/*.xml - key.core/build/reports/runallproofs/* - **/build/reports/ - !**/jacocoTestReport.xml - From ef1168c3deeffa0f030db3461350cbf7b7d1c34e Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Wed, 7 Jan 2026 18:05:01 +0100 Subject: [PATCH 3/4] adapting tests after KeY-meeting --- .github/workflows/release-tests.yml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/.github/workflows/release-tests.yml b/.github/workflows/release-tests.yml index e9773a670a..785654b44c 100644 --- a/.github/workflows/release-tests.yml +++ b/.github/workflows/release-tests.yml @@ -63,7 +63,6 @@ jobs: **/build/reports/ !**/jacocoTestReport.xml - integration-tests: env: @@ -72,11 +71,11 @@ jobs: strategy: fail-fast: true matrix: - test: [ testProveRules, testRunAllFunProofs, testRunAllInfProofs, testProveSMTLemmas, testStrictSMT ] + test: [ testProveRules, testRunAllFunProofs, testRunAllInfProofs, testProveSMTLemmas ] os: [ macos-latest, ubuntu-latest, windows-latest ] java: [ 21, 25 ] - z3: [ '4.13.4', '4.14.1', '4.15.4' ] - cvc5: [ '1.3.2', '1.2.1' ] + z3: [ '4.15.4' ] + cvc5: [ '1.3.2' ] runs-on: ${{ matrix.os }} steps: @@ -111,6 +110,7 @@ jobs: **/build/reports/ !**/jacocoTestReport.xml + smt-tests: env: GH_TOKEN: ${{ github.token }} @@ -142,8 +142,8 @@ jobs: - name: Setup Gradle uses: gradle/actions/setup-gradle@v5 - - name: "Running tests: ${{ matrix.test }}" - run: ./gradlew --continue ${{ matrix.test }} + - name: "Running tests" + run: ./gradlew --continue --tests de.uka.ilkd.key.smt.* :key.core:test - name: Upload test results uses: actions/upload-artifact@v6 From ebdca3f4d52b80c527da132f2845c01c98cbb065 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Tue, 13 Jan 2026 23:42:23 +0100 Subject: [PATCH 4/4] fix order of cli --- .github/workflows/release-tests.yml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/.github/workflows/release-tests.yml b/.github/workflows/release-tests.yml index 785654b44c..3ddf50137a 100644 --- a/.github/workflows/release-tests.yml +++ b/.github/workflows/release-tests.yml @@ -3,13 +3,12 @@ name: Broad Release Tests on: workflow_dispatch: schedule: - - cron: '0 5 * * 1' # every monday morning + - cron: '0 5 5 * *' # every monday morning env: z3: '4.13.4' # default z3 version cvc5: '1.3.2' # default cvc5 version - jobs: unit-tests: strategy: @@ -143,7 +142,7 @@ jobs: uses: gradle/actions/setup-gradle@v5 - name: "Running tests" - run: ./gradlew --continue --tests de.uka.ilkd.key.smt.* :key.core:test + run: ./gradlew :key.core:test --continue --tests 'de.uka.ilkd.key.smt.*' - name: Upload test results uses: actions/upload-artifact@v6