diff --git a/.github/old_workflows/deletecache.yml b/.github/old_workflows/deletecache.yml deleted file mode 100644 index 8376a396fc9..00000000000 --- 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 41134d5a18f..00000000000 --- 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 93a3b2f001d..00000000000 --- 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 4fc333c65f9..00000000000 --- 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 1b7e1c7dc30..00000000000 --- a/.github/qodana.starter.full.xml +++ /dev/null @@ -1,7016 +0,0 @@ - - - - \ No newline at end of file diff --git a/.github/workflows/opttest.yml b/.github/workflows/opttest.yml index 768a3663e41..26528e5f9dc 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/ diff --git a/.github/workflows/release-tests.yml b/.github/workflows/release-tests.yml new file mode 100644 index 00000000000..3ddf50137a7 --- /dev/null +++ b/.github/workflows/release-tests.yml @@ -0,0 +1,157 @@ +name: Broad Release Tests + +on: + workflow_dispatch: + schedule: + - 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: + 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 ] + os: [ macos-latest, ubuntu-latest, windows-latest ] + java: [ 21, 25 ] + z3: [ '4.15.4' ] + cvc5: [ '1.3.2' ] + + 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" + run: ./gradlew :key.core:test --continue --tests 'de.uka.ilkd.key.smt.*' + + - 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 e861d23b238..00000000000 --- 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 51910bfe924..0dbf0b6dd3b 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 497019b40e9..00000000000 --- 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 -