Repository navigation
perf(FiveEighthsTheorem): reduce counting-proof elaboration #3783
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 | |
| # The build runs in one of three modes, decided per run by a cheap `plan` job | |
| # (scripts/ci/plan-build-shards.py) from the diff and the cache state: | |
| # | |
| # - `skip`: an exact README-only change. It still reports the | |
| # protected `Build project` check without spending hours rebuilding Lean. | |
| # - `single`: the classic one-job pipeline. This is the fast path for the | |
| # common case — a PR that adds or edits a project or three. | |
| # - `sharded`: for the runs that take hours serially (cold cache, | |
| # toolchain/manifest bump, refactors touching many projects), the dirty | |
| # projects are bin-packed into parallel `shard` build jobs. Pool projects | |
| # never import each other, so project-granular shards duplicate no work. | |
| # Each shard uploads only the files its build produced; `finalize` merges | |
| # them, builds the root library (also a safety net: anything a shard | |
| # missed is built here), and runs the whole-pool linters and quality | |
| # checks once. | |
| # | |
| # Shard assignment is computed from the tree at run time — there is no | |
| # static shard list to maintain as the pool grows. The `Build project` | |
| # gate job reports the overall verdict under the same check name the | |
| # single-job workflow used. | |
| on: | |
| push: | |
| branches: | |
| - main | |
| paths: | |
| - '**/*.lean' | |
| - 'lakefile.toml' | |
| - 'lean-toolchain' | |
| - 'lake-manifest.json' | |
| - 'LeanPool/projects.yml' | |
| - 'Challenge/challenges.yml' | |
| - 'python/lean_pool/challenge.py' | |
| - 'python/lean_pool/quality.py' | |
| - 'python/lean_pool/validation_cache.py' | |
| - 'python/lean_pool/ci_artifacts.py' | |
| - 'python/pyproject.toml' | |
| - 'python/uv.lock' | |
| - 'scripts/nolints-style.txt' | |
| - 'scripts/ci/**' | |
| - '.github/CODE_QUALITY.md' | |
| - '.github/workflows/lean_action_ci.yml' | |
| pull_request: | |
| branches: | |
| - main | |
| # Work stacks on the bump branch during a Lean/Mathlib migration, and | |
| # a contribution that never builds is a contribution nobody can judge: | |
| # PR #301 added a 210-file project onto `bump/v4.33.0-rc1` and got no | |
| # build, no linters, and no quality checks at all. | |
| - 'bump/**' | |
| paths: | |
| - 'README.md' | |
| # Attribution-only PRs must still produce the required checks. | |
| - 'NOTICE.extra.yml' | |
| - '**/*.lean' | |
| - 'lakefile.toml' | |
| - 'lean-toolchain' | |
| - 'lake-manifest.json' | |
| - 'LeanPool/projects.yml' | |
| - 'Challenge/challenges.yml' | |
| - 'python/lean_pool/challenge.py' | |
| - 'python/lean_pool/quality.py' | |
| - 'python/lean_pool/validation_cache.py' | |
| - 'python/lean_pool/ci_artifacts.py' | |
| - 'python/pyproject.toml' | |
| - 'python/uv.lock' | |
| - 'scripts/nolints-style.txt' | |
| - 'scripts/ci/**' | |
| - '.github/CODE_QUALITY.md' | |
| - '.github/workflows/notice.yml' | |
| - '.github/workflows/lean_action_ci.yml' | |
| workflow_dispatch: | |
| inputs: | |
| force_full: | |
| description: "Shard-build the whole pool even when a warm cache exists" | |
| required: false | |
| type: boolean | |
| default: false | |
| # Cancel superseded runs on the same branch / PR. | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| permissions: | |
| contents: read | |
| pages: write | |
| id-token: write | |
| jobs: | |
| plan: | |
| runs-on: ubuntu-latest | |
| name: Plan build | |
| outputs: | |
| mode: ${{ steps.plan.outputs.mode }} | |
| matrix: ${{ steps.plan.outputs.matrix }} | |
| steps: | |
| - name: Checkout project | |
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd | |
| with: | |
| fetch-depth: 0 | |
| # Only checks whether a warm build cache exists; a cold cache means a | |
| # whole-pool build, which is exactly when sharding pays off most. | |
| - name: Check for a warm build cache | |
| id: lake-cache | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| lookup-only: true | |
| path: .lake/build | |
| key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} | |
| restore-keys: | | |
| LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- | |
| - name: Plan the build | |
| id: plan | |
| env: | |
| EVENT_NAME: ${{ github.event_name }} | |
| BASE_SHA: ${{ github.event.pull_request.base.sha }} | |
| BEFORE_SHA: ${{ github.event.before }} | |
| FORCE_FULL: ${{ inputs.force_full }} | |
| CACHE_MATCHED: ${{ steps.lake-cache.outputs.cache-matched-key }} | |
| run: | | |
| set -euo pipefail | |
| diff_available=true | |
| # A file, not an environment variable: a large import's path list | |
| # exceeds the kernel's 128 KiB limit on a single environment string. | |
| changed_files="$RUNNER_TEMP/changed-files.txt" | |
| : > "$changed_files" | |
| case "$EVENT_NAME" in | |
| pull_request) | |
| git diff --name-only "$BASE_SHA"...HEAD > "$changed_files" | |
| ;; | |
| push) | |
| if [ -n "$BEFORE_SHA" ] \ | |
| && ! printf '%s' "$BEFORE_SHA" | grep -q '^0*$' \ | |
| && git cat-file -e "$BEFORE_SHA" 2>/dev/null; then | |
| git diff --name-only "$BEFORE_SHA"..HEAD > "$changed_files" | |
| else | |
| diff_available=false | |
| fi | |
| ;; | |
| workflow_dispatch) | |
| diff_available=false | |
| ;; | |
| esac | |
| cold=false | |
| if [ -z "$CACHE_MATCHED" ]; then cold=true; fi | |
| plan=$(CHANGED_FILES_PATH="$changed_files" DIFF_AVAILABLE="$diff_available" \ | |
| COLD="$cold" FORCE_FULL="$FORCE_FULL" \ | |
| python3 scripts/ci/plan-build-shards.py) | |
| echo "Plan: $plan" | |
| { | |
| echo "mode=$(echo "$plan" | python3 -c 'import json,sys; print(json.load(sys.stdin)["mode"])')" | |
| echo "matrix=$(echo "$plan" | python3 -c 'import json,sys; print(json.dumps(json.load(sys.stdin)["matrix"]))')" | |
| } >> "$GITHUB_OUTPUT" | |
| # The single-job pipeline is the fast path for ordinary PRs. | |
| build: | |
| needs: plan | |
| if: needs.plan.outputs.mode == 'single' | |
| runs-on: ubuntu-latest | |
| name: Build pool | |
| steps: | |
| - name: Checkout project | |
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd | |
| with: | |
| fetch-depth: 0 | |
| # Keep the large toolchain/Mathlib cache independent of per-commit builds. | |
| - name: Restore Lean dependencies | |
| id: dependency-cache | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: | | |
| ~/.elan | |
| .lake/packages | |
| key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} | |
| - name: Restore pool build | |
| id: cache | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: .lake/build | |
| key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} | |
| restore-keys: | | |
| LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- | |
| - name: Install Lean | |
| uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 | |
| with: | |
| auto-config: false | |
| use-github-cache: false | |
| use-mathlib-cache: false | |
| - name: Install uv | |
| uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff | |
| with: | |
| enable-cache: true | |
| - name: Install Mathlib cache | |
| id: mathlib-cache | |
| run: | | |
| if [ ! -d ".lake/packages/mathlib" ]; then | |
| ~/.elan/bin/lake exe cache get | |
| else | |
| echo "Mathlib already present from cache" | |
| fi | |
| - name: Check library indexes use the module system and are up to date | |
| run: | | |
| if ! ~/.elan/bin/lake exe mk_all --module --check; then | |
| echo "::error::Library indexes are out of date or missing module headers. Run 'lake exe mk_all --module' locally and commit the result." | |
| exit 1 | |
| fi | |
| - name: Build project | |
| run: | | |
| set -euo pipefail | |
| ~/.elan/bin/lake build LeanPool 2>&1 | tee lean-build.log | |
| if grep -nE '(^|: )warning:' lean-build.log; then | |
| echo "::error::Lean build emitted warnings; fix them before merging." | |
| exit 1 | |
| fi | |
| - name: Build challenges and solutions | |
| run: ./scripts/ci/build-challenges.sh | |
| # Publish once compilation succeeds, so docs can overlap the later | |
| # linters/quality checks without compiling the same PR a second time. | |
| - name: Package build for documentation | |
| if: github.event_name != 'pull_request' | |
| run: PYTHONPATH=python python3 -m lean_pool.ci_artifacts pack | |
| - name: Share build with documentation | |
| if: github.event_name != 'pull_request' | |
| uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 | |
| with: | |
| name: lean-pool-build | |
| path: lean-pool-build.tar.gz | |
| if-no-files-found: error | |
| compression-level: 0 | |
| retention-days: 1 | |
| # Actions scopes PR caches to refs/pull/<n>/merge: updates to the same | |
| # PR can reuse receipts, while main and other PRs cannot read them. | |
| - name: Restore project validation | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: .lake/validation-cache/v1 | |
| key: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} | |
| restore-keys: | | |
| LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- | |
| - name: Install validation dependencies | |
| run: cd python && uv sync --locked | |
| - name: Lint | |
| run: | | |
| cd python | |
| uv run python -m lean_pool.validation_cache lint --repo .. | |
| cd .. | |
| ~/.elan/bin/lake exe runLinter Challenge | |
| ~/.elan/bin/lake exe runLinter Solution | |
| - name: Text style lint | |
| run: | | |
| ~/.elan/bin/lake exe lint-style LeanPool | |
| ~/.elan/bin/lake exe lint-style Challenge | |
| ~/.elan/bin/lake exe lint-style Solution | |
| - name: Repository quality checks | |
| run: | | |
| cd python | |
| uv run python -m lean_pool.validation_cache quality --repo .. | |
| - name: Save project validation | |
| # Successful receipts are tiny; retain PR results across registry rebases. | |
| uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: .lake/validation-cache/v1 | |
| key: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} | |
| - name: Save Lean dependencies | |
| if: always() && github.ref == 'refs/heads/main' && steps.mathlib-cache.outcome == 'success' && steps.dependency-cache.outputs.cache-hit != 'true' | |
| uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: | | |
| ~/.elan | |
| .lake/packages | |
| key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} | |
| - name: Save pool build | |
| if: always() && github.ref == 'refs/heads/main' | |
| uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: .lake/build | |
| key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} | |
| shard: | |
| needs: plan | |
| if: needs.plan.outputs.mode == 'sharded' | |
| runs-on: ubuntu-latest | |
| name: Build shard ${{ matrix.shard }} | |
| strategy: | |
| # One shard failing must not cancel the rest: `finalize` rebuilds any | |
| # gap itself, so the run still yields a complete log — but the gate | |
| # job fails whenever a shard failed (a shard's warning gate must not | |
| # be bypassable by cache replay in `finalize`). | |
| fail-fast: false | |
| matrix: ${{ fromJSON(needs.plan.outputs.matrix) }} | |
| steps: | |
| - name: Checkout project | |
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd | |
| with: | |
| fetch-depth: 0 | |
| - name: Restore Lean dependencies | |
| id: dependency-cache | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: | | |
| ~/.elan | |
| .lake/packages | |
| key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} | |
| - name: Restore pool build | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: .lake/build | |
| key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} | |
| restore-keys: | | |
| LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- | |
| - name: Install Lean | |
| uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 | |
| with: | |
| auto-config: false | |
| use-github-cache: false | |
| use-mathlib-cache: false | |
| - name: Install Mathlib cache | |
| id: mathlib-cache | |
| run: | | |
| if [ ! -d ".lake/packages/mathlib" ]; then | |
| ~/.elan/bin/lake exe cache get | |
| else | |
| echo "Mathlib already present from cache" | |
| fi | |
| - name: Build this shard's projects | |
| env: | |
| PROJECTS: ${{ matrix.projects }} | |
| run: | | |
| set -euo pipefail | |
| touch "$RUNNER_TEMP/build-stamp" | |
| modules="" | |
| # shellcheck disable=SC2086 # word-split the project list on purpose | |
| for project in $PROJECTS; do | |
| project_modules=$(git ls-files -- "LeanPool/$project.lean" "LeanPool/$project/" \ | |
| | grep '\.lean$' \ | |
| | sed -e 's/\.lean$//' -e 's#/#.#g' \ | |
| | tr '\n' ' ') | |
| modules="$modules $project_modules" | |
| done | |
| # shellcheck disable=SC2086 # modules is a space-separated list on purpose | |
| ~/.elan/bin/lake build $modules 2>&1 | tee shard-build.log | |
| if grep -nE '(^|: )warning:' shard-build.log; then | |
| echo "::error::Lean build emitted warnings; fix them before merging." | |
| exit 1 | |
| fi | |
| # Ship only what this build produced; unchanged (cache-replayed) | |
| # files stay out, so `finalize` can layer the shard outputs onto the | |
| # same restored cache without clobbering anything fresher. | |
| - name: Package new build outputs | |
| env: | |
| SHARD: ${{ matrix.shard }} | |
| run: | | |
| set -euo pipefail | |
| find .lake/build -type f -newer "$RUNNER_TEMP/build-stamp" \ | |
| > "$RUNNER_TEMP/new-files.txt" | |
| echo "$(wc -l < "$RUNNER_TEMP/new-files.txt") new build files" | |
| if [ -s "$RUNNER_TEMP/new-files.txt" ]; then | |
| tar -czf "shard-oleans-$SHARD.tar.gz" -T "$RUNNER_TEMP/new-files.txt" | |
| fi | |
| - name: Upload build outputs | |
| uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 | |
| with: | |
| name: ci-oleans-${{ matrix.shard }} | |
| path: shard-oleans-*.tar.gz | |
| if-no-files-found: ignore | |
| retention-days: 1 | |
| finalize: | |
| needs: [plan, shard] | |
| # Run even when a shard failed: merging what succeeded and building the | |
| # rest here still produces a complete build log and lint report for | |
| # debugging. The gate job is what enforces that every shard was green. | |
| if: >- | |
| !cancelled() && needs.plan.result == 'success' && | |
| needs.plan.outputs.mode == 'sharded' | |
| runs-on: ubuntu-latest | |
| name: Assemble and lint | |
| steps: | |
| - name: Checkout project | |
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd | |
| with: | |
| fetch-depth: 0 | |
| - name: Restore Lean dependencies | |
| id: dependency-cache | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: | | |
| ~/.elan | |
| .lake/packages | |
| key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} | |
| - name: Restore pool build | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: .lake/build | |
| key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} | |
| restore-keys: | | |
| LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- | |
| - name: Install Lean | |
| uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 | |
| with: | |
| auto-config: false | |
| use-github-cache: false | |
| use-mathlib-cache: false | |
| - name: Install uv | |
| uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff | |
| with: | |
| enable-cache: true | |
| - name: Install Mathlib cache | |
| id: mathlib-cache | |
| run: | | |
| if [ ! -d ".lake/packages/mathlib" ]; then | |
| ~/.elan/bin/lake exe cache get | |
| else | |
| echo "Mathlib already present from cache" | |
| fi | |
| - name: Download shard build outputs | |
| uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093 | |
| with: | |
| pattern: ci-oleans-* | |
| merge-multiple: true | |
| - name: Merge shard build outputs | |
| run: | | |
| set -euo pipefail | |
| for archive in shard-oleans-*.tar.gz; do | |
| if [ -e "$archive" ]; then | |
| tar -xzf "$archive" | |
| rm "$archive" | |
| fi | |
| done | |
| - name: Check library indexes use the module system and are up to date | |
| run: | | |
| if ! ~/.elan/bin/lake exe mk_all --module --check; then | |
| echo "::error::Library indexes are out of date or missing module headers. Run 'lake exe mk_all --module' locally and commit the result." | |
| exit 1 | |
| fi | |
| # With the shard outputs in place this is mostly cache replay; it | |
| # builds the root module and anything a shard missed or failed to | |
| # deliver, so the assembled pool is complete regardless. | |
| - name: Build project | |
| run: | | |
| set -euo pipefail | |
| ~/.elan/bin/lake build LeanPool 2>&1 | tee lean-build.log | |
| if grep -nE '(^|: )warning:' lean-build.log; then | |
| echo "::error::Lean build emitted warnings; fix them before merging." | |
| exit 1 | |
| fi | |
| - name: Build challenges and solutions | |
| run: ./scripts/ci/build-challenges.sh | |
| # Publish once compilation succeeds, so docs can overlap the later | |
| # linters/quality checks without compiling the same PR a second time. | |
| - name: Package build for documentation | |
| if: github.event_name != 'pull_request' | |
| run: PYTHONPATH=python python3 -m lean_pool.ci_artifacts pack | |
| - name: Share build with documentation | |
| if: github.event_name != 'pull_request' | |
| uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 | |
| with: | |
| name: lean-pool-build | |
| path: lean-pool-build.tar.gz | |
| if-no-files-found: error | |
| compression-level: 0 | |
| retention-days: 1 | |
| # Actions scopes PR caches to refs/pull/<n>/merge: updates to the same | |
| # PR can reuse receipts, while main and other PRs cannot read them. | |
| - name: Restore project validation | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: .lake/validation-cache/v1 | |
| key: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} | |
| restore-keys: | | |
| LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- | |
| - name: Install validation dependencies | |
| run: cd python && uv sync --locked | |
| - name: Lint | |
| run: | | |
| cd python | |
| uv run python -m lean_pool.validation_cache lint --repo .. | |
| cd .. | |
| ~/.elan/bin/lake exe runLinter Challenge | |
| ~/.elan/bin/lake exe runLinter Solution | |
| - name: Text style lint | |
| run: | | |
| ~/.elan/bin/lake exe lint-style LeanPool | |
| ~/.elan/bin/lake exe lint-style Challenge | |
| ~/.elan/bin/lake exe lint-style Solution | |
| - name: Repository quality checks | |
| run: | | |
| cd python | |
| uv run python -m lean_pool.validation_cache quality --repo .. | |
| - name: Save project validation | |
| # Successful receipts are tiny; retain PR results across registry rebases. | |
| uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: .lake/validation-cache/v1 | |
| key: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} | |
| - name: Save Lean dependencies | |
| if: always() && github.ref == 'refs/heads/main' && steps.mathlib-cache.outcome == 'success' && steps.dependency-cache.outputs.cache-hit != 'true' | |
| uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: | | |
| ~/.elan | |
| .lake/packages | |
| key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} | |
| - name: Save pool build | |
| if: always() && github.ref == 'refs/heads/main' | |
| uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: .lake/build | |
| key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} | |
| # Single overall verdict under the check name the one-job workflow used, | |
| # so nothing watching "Build project" needs to change. | |
| gate: | |
| needs: [plan, build, shard, finalize] | |
| if: always() | |
| runs-on: ubuntu-latest | |
| name: Build project | |
| steps: | |
| - name: Check outcome | |
| env: | |
| MODE: ${{ needs.plan.outputs.mode }} | |
| PLAN_RESULT: ${{ needs.plan.result }} | |
| BUILD_RESULT: ${{ needs.build.result }} | |
| SHARD_RESULT: ${{ needs.shard.result }} | |
| FINALIZE_RESULT: ${{ needs.finalize.result }} | |
| run: | | |
| set -euo pipefail | |
| echo "plan=$PLAN_RESULT mode=$MODE build=$BUILD_RESULT shard=$SHARD_RESULT finalize=$FINALIZE_RESULT" | |
| if [ "$PLAN_RESULT" != "success" ]; then | |
| echo "::error::Build planning failed." | |
| exit 1 | |
| fi | |
| case "$MODE" in | |
| skip) | |
| echo "No Lean build inputs changed." | |
| ;; | |
| single) | |
| [ "$BUILD_RESULT" = "success" ] || { echo "::error::Build failed."; exit 1; } | |
| ;; | |
| sharded) | |
| [ "$SHARD_RESULT" = "success" ] || { echo "::error::A build shard failed."; exit 1; } | |
| [ "$FINALIZE_RESULT" = "success" ] || { echo "::error::Assembly or linting failed."; exit 1; } | |
| ;; | |
| *) | |
| echo "::error::Unknown build mode: $MODE" | |
| exit 1 | |
| ;; | |
| esac | |
| echo "CI passed in $MODE mode." |