codelib: words32/slot32 twins + verified u32 copy loop (#68 phase 2c) #447
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: 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 | |
| use-mathlib-cache: true | |
| - name: Fail on build warnings | |
| working-directory: programs/lean | |
| run: | | |
| set -o pipefail | |
| # Rebuild (cached) and capture output. Warnings (e.g. `sorry`, | |
| # unused-variable lints) are re-emitted on every build but do not | |
| # change lake's exit code, so scan the log and fail if any appear. | |
| lake build 2>&1 | tee build.log | |
| if grep -E '(^|[[:space:]])warning:' build.log; then | |
| echo "::error::Build produced warnings; warnings are not allowed." | |
| exit 1 | |
| fi | |
| 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 |