key/.github/workflows/release-tests.yml at main · KeYProject/key · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
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: false
      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: Assemble
        run: ./gradlew --parallel assemble

      - 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: false
      matrix:
        test: [ testProveRules, testRunAllFunProofs, testRunAllInfProofs, testRunAllWdProofs, 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: false
      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