Integrate Iris small-step Wasm semantics #485
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: | |
| codelib: | |
| name: Build CodeLib proofs | |
| runs-on: macos-latest | |
| steps: | |
| - uses: actions/checkout@v5 | |
| - uses: actions/cache@v5 | |
| 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: codelib | |
| build-args: "--wfail" | |
| use-mathlib-cache: true | |
| programs: | |
| name: Build program proofs | |
| runs-on: macos-latest | |
| steps: | |
| - uses: actions/checkout@v5 | |
| - uses: actions/cache@v5 | |
| 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-args: "Project --wfail" | |
| use-mathlib-cache: true | |
| test: | |
| name: Smoke test | |
| runs-on: ubuntu-latest | |
| needs: [codelib, programs] | |
| steps: | |
| - uses: actions/checkout@v5 | |
| - uses: actions/cache@v5 | |
| 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 |