Fix coverage collection #388
Workflow file for this run
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: Build and test Lean backend | |
| on: [push, pull_request, workflow_dispatch] | |
| env: | |
| OPAMVERBOSE: 1 | |
| jobs: | |
| build: | |
| strategy: | |
| matrix: | |
| version: [5.2.1] | |
| os: [ubuntu-latest] | |
| runs-on: ${{ matrix.os }} | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: System dependencies (ubuntu) | |
| if: startsWith(matrix.os, 'ubuntu') | |
| run: | | |
| sudo apt install build-essential libgmp-dev z3 cvc4 opam | |
| - name: Restore cached opam | |
| id: cache-opam-restore | |
| uses: actions/cache/restore@v4 | |
| with: | |
| path: ~/.opam | |
| key: ${{ matrix.os }}-${{ matrix.version }} | |
| - name: Setup opam | |
| if: steps.cache-opam-restore.outputs.cache-hit != 'true' | |
| run: | | |
| opam init --yes --no-setup --shell=sh --compiler=${{ matrix.version }} | |
| opam install dune | |
| - name: Install Sail | |
| run: | | |
| git clone https://github.com/rems-project/sail.git | |
| eval $(opam env) | |
| (cd sail; opam install sail --deps-only --yes) | |
| (cd sail; make install) | |
| - name: Save cached opam | |
| id: cache-opam-save | |
| uses: actions/cache/save@v4 | |
| with: | |
| path: ~/.opam | |
| key: ${{ steps.cache-opam-restore.outputs.cache-primary-key }} | |
| - name: Install Lean | |
| run: | | |
| wget -q https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_debian.sh | |
| bash install_debian.sh ; rm -f install_debian.sh | |
| - name: Build the Sail RISCV Model for Lean | |
| run: | | |
| eval $(opam config env) | |
| cmake -S . -B build -DCMAKE_BUILD_TYPE=RelWithDebInfo -G Ninja | |
| cmake --build build/ --target generated_lean_rv64d generated_lean_executable_rv64d | |
| - name: Restore cached .lake directory | |
| id: cache-lake-restore | |
| uses: actions/cache/restore@v4 | |
| with: | |
| path: | | |
| build/model/Lean_RV64D/.lake | |
| build/model/Lean_RV64D_executable/.lake | |
| key: ${{ matrix.os }}-${{ matrix.version }} | |
| - name: Use Lean to build the model and report errors | |
| run: | | |
| source ~/.profile | |
| cd build/model/Lean_RV64D/ | |
| lake build | |
| - name: Save cached .lake directory | |
| id: cache-lake-save | |
| uses: actions/cache/save@v4 | |
| with: | |
| path: | | |
| build/model/Lean_RV64D/.lake | |
| build/model/Lean_RV64D_executable/.lake | |
| key: ${{ steps.cache-lake-restore.outputs.cache-primary-key }} |