update link to Isabelle 2022 #52
This file contains 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: Boogie Proof Generation CI | |
| on: | |
| push: | |
| branches: [ master, staging, trying ] | |
| pull_request: | |
| branches: [ master ] | |
| workflow_dispatch: | |
| env: | |
| Z3_VERSION: 4.8.8 | |
| jobs: | |
| build: | |
| strategy: | |
| matrix: | |
| os: [ ubuntu-latest ] | |
| fail-fast: false | |
| runs-on: ${{ matrix.os }} | |
| steps: | |
| - uses: actions/checkout@v3 | |
| with: | |
| submodules: 'true' | |
| - name: Setup dotnet | |
| uses: actions/setup-dotnet@v1 | |
| with: | |
| dotnet-version: '6.0.x' | |
| - name: Setup Python | |
| uses: actions/setup-python@v4 | |
| with: | |
| python-version: '3.10.6' | |
| - name: Get Z3 | |
| run: | | |
| wget --quiet https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-ubuntu-16.04.zip | |
| unzip z3-*.zip | |
| echo $(find $PWD/z3* -name bin -type d)>> $GITHUB_PATH | |
| - name: Compile Boogie proof generation | |
| run: | | |
| dotnet build -c Release Source/Boogie.sln | |
| - name: Generate external benchmark proofs | |
| run: | | |
| BOOGIE_EXE=$(find $PWD -type f -name "BoogieDriver") | |
| python3 etc/scripts/generate_proofs.py --inputdir ProofGenerationBenchmarks/external_benchmarks/modified --outputdir table_benchmarks_proofs --boogieproofExe $BOOGIE_EXE | |
| - name: Get Isabelle | |
| run: | | |
| wget --quiet https://isabelle.in.tum.de/website-Isabelle2022/dist/Isabelle2022_linux.tar.gz | |
| tar -xf Isabelle2022_linux.tar.gz | |
| rm Isabelle2022_linux.tar.gz | |
| mv Isabelle2022 isabelle_dir | |
| isabelle_dir/bin/isabelle version | |
| echo isabelle_dir/bin >> $GITHUB_PATH | |
| # add Boogie language session to ROOTS and create heap image (option -b) | |
| # for the session so that it does not have to rechecked every time | |
| - name: Set up Isabelle Boogie language session | |
| run: | | |
| echo "$PWD/foundational_boogie/BoogieLang" >> isabelle_dir/ROOTS | |
| isabelle_dir/bin/isabelle build -b -j4 -d $PWD/foundational_boogie/BoogieLang Boogie_Lang | |
| - name: Check external benchmark proofs | |
| run: | | |
| python3 etc/scripts/check_proofs.py --inputdir table_benchmarks_proofs --reps 1 | |
| - name: Generate Boogie benchmark proofs | |
| run: | | |
| BOOGIE_EXE=$(find $PWD -type f -name "BoogieDriver") | |
| python3 etc/scripts/generate_proofs.py --inputdir ProofGenerationBenchmarks/boogie_testsuite_benchmarks --outputdir boogie_benchmarks_proofs --boogieproofExe $BOOGIE_EXE | |
| - name: Check Boogie benchmark proofs | |
| run: | | |
| python3 etc/scripts/check_proofs.py --inputdir boogie_benchmarks_proofs --reps 1 |