Fix soundness bug: correct quantifier structure in functional extensi… #151
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: ci-linux | |
| permissions: | |
| contents: read | |
| on: | |
| pull_request: | |
| push: | |
| branches: [ staging, main ] | |
| concurrency: | |
| group: ${{ github.ref }} | |
| cancel-in-progress: true | |
| env: | |
| LEAN_VERSION: "4.24.0" | |
| Z3_VERSION: "4.15.2" | |
| GLIBC_Z3: "2.39" | |
| jobs: | |
| build: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Setup Lean | |
| run: | | |
| curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y | |
| echo "/home/runner/.elan/bin" >> $GITHUB_PATH | |
| chmod +x /home/runner/.elan/bin/* | |
| - name: Fix Elan version | |
| run: | | |
| elan toolchain install ${{ env.LEAN_VERSION }} | |
| elan default ${{ env.LEAN_VERSION }} | |
| - name: Install Z3 | |
| run: | | |
| cd /home/runner/ | |
| wget -q https://github.com/Z3Prover/z3/releases/download/z3-${{ env.Z3_VERSION }}/z3-${{ env.Z3_VERSION }}-x64-glibc-${{ env.GLIBC_Z3 }}.zip | |
| unzip -q z3-${{ env.Z3_VERSION }}-x64-glibc-${{ env.GLIBC_Z3 }}.zip | |
| chmod +x z3-${{ env.Z3_VERSION }}-x64-glibc-${{ env.GLIBC_Z3 }}.zip | |
| echo "/home/runner/z3-${{ env.Z3_VERSION }}-x64-glibc-${{ env.GLIBC_Z3 }}/bin" >> $GITHUB_PATH | |
| - name: Tools version | |
| run: | | |
| elan --version | |
| lake --version | |
| lean --version | |
| z3 --version | |
| - name: Checkout repository | |
| uses: actions/checkout@v4 | |
| - name: Build and Validate Blaster | |
| run: make check_blaster | |
| - name: Upload Blaster build log | |
| if: failure() | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: blaster-build | |
| path: ./Blaster/build.log | |
| - name: Execute and Validate Tests | |
| run: LEAN_NUM_THREADS=5 ./scripts/check_lean_project_compilation.sh Tests | |
| - name: Upload Tests log | |
| if: failure() | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: tests-build | |
| path: ./Tests/build.log |