Update README.md #5
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 | |
| on: | |
| push: | |
| branches: [main, master] | |
| pull_request: | |
| branches: [main, master] | |
| workflow_dispatch: | |
| jobs: | |
| test: | |
| strategy: | |
| matrix: | |
| os: [ubuntu-22.04, macos-14] | |
| lean-version: [leanprover/lean4:v4.21.0] | |
| runs-on: ${{ matrix.os }} | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| - name: Setup Lean | |
| uses: leanprover/lean-action@v1 | |
| - name: Install Rust | |
| uses: actions-rs/toolchain@v1 | |
| with: | |
| toolchain: stable | |
| override: true | |
| - name: Build | |
| run: lake build | |
| - name: Test | |
| run: lake test | |
| - name: Extract smoke test | |
| run: | | |
| # Placeholder for extraction smoke test | |
| echo "Extraction smoke test - TODO: implement lake exe extract" | |
| # lake exe extract smoke | |
| - name: Check for sorry | |
| run: | | |
| if grep -r "sorry" LeanToolchain/; then | |
| echo "Found 'sorry' statements - these should be replaced with proofs" | |
| exit 1 | |
| fi |