claims only mode #114
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: Lean Action CI | |
| on: | |
| push: | |
| pull_request: | |
| workflow_dispatch: | |
| jobs: | |
| # The CI scripts behind the composite action, checked without a Lean toolchain: `gh`, `lake` and | |
| # `referee` are replaced by fakes, so this finishes in seconds and gates every pull request | |
| # separately from the (much slower) Lean build. | |
| # | |
| # Worth having as its own job rather than a step of the build: the shell this replaces lived in | |
| # consumer workflows where nothing could test it, and when `highlight` was removed from referee | |
| # the two copies of it kept calling a subcommand that no longer existed. `subcommands_exist` is | |
| # that regression, and it only helps if it runs on every change to either side. | |
| ci-scripts: | |
| name: CI script tests | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v5 | |
| # shellcheck is preinstalled on the GitHub-hosted Ubuntu images. | |
| - name: Lint | |
| run: shellcheck -x ci/*.sh ci/tests/*.sh | |
| - name: Test | |
| run: ./ci/tests/run-tests.sh | |
| build: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v5 | |
| - uses: leanprover/lean-action@v1 | |
| # `lake build` builds the default target, which is the `referee` executable alone. `Test` and | |
| # `Proofs` are separate Lake targets, so until this step existed neither the `#guard`s nor the | |
| # theorems were checked here — the build could go green with both broken. Both are checked at | |
| # elaboration time, so building them is running them. | |
| # | |
| # Placed before packaging so a failure stops the run rather than producing a binary from a | |
| # tree that does not pass its own checks. | |
| - name: Build tests and proofs | |
| run: lake build Test Proofs | |
| - name: Package referee binary | |
| run: ./scripts/package-referee-binary.sh |