Integrate Iris small-step Wasm semantics #482
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] | |
| pull_request: | |
| workflow_dispatch: | |
| jobs: | |
| build: | |
| name: Build & verify proofs | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: actions/cache@v4 | |
| with: | |
| path: .lake/packages | |
| key: lake-pkgs-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('interpreter/lake-manifest.json') }} | |
| restore-keys: | | |
| lake-pkgs-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}- | |
| - uses: leanprover/lean-action@v1 | |
| with: | |
| lake-package-directory: programs/lean | |
| # Build every CodeLib module (including its verified examples) as a | |
| # separate target. Keeping examples out of the downstream umbrella | |
| # avoids loading their large proof environments into every Project | |
| # module in parallel on the hosted runner. | |
| build-args: "@CodeLib Project --wfail" | |
| use-mathlib-cache: true | |
| test: | |
| name: Smoke test | |
| runs-on: ubuntu-latest | |
| needs: build | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: actions/cache@v4 | |
| with: | |
| path: .lake/packages | |
| key: lake-pkgs-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('interpreter/lake-manifest.json') }} | |
| restore-keys: | | |
| lake-pkgs-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}- | |
| - uses: leanprover/lean-action@v1 | |
| with: | |
| lake-package-directory: interpreter | |
| # Build the `Interpreter` library (not just the `runner` exe) so the | |
| # worked examples under Interpreter/Wasm/Examples/ — which the main | |
| # `programs/lean` build does not reach — are compiled and their | |
| # `native_decide` checks run, keeping an example from silently | |
| # rotting. Coverage is only as complete as Examples/Basic.lean's | |
| # umbrella import: this build reaches an example iff Basic.lean | |
| # imports it, so every example file must be listed there. | |
| build-args: Interpreter runner | |
| use-mathlib-cache: true | |
| - name: Install just | |
| uses: taiki-e/install-action@just | |
| - name: Runner smoke test | |
| run: just runner-smoke |