Repository navigation
Reduce Erdos97ConvexOctagon peak compiler memory #6586
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: Documentation | |
| on: | |
| merge_group: | |
| types: [checks_requested] | |
| pull_request: | |
| branches: | |
| - main | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| permissions: | |
| contents: read | |
| actions: read | |
| jobs: | |
| scope: | |
| runs-on: ubuntu-latest | |
| outputs: | |
| applicable: ${{ steps.scope.outputs.applicable }} | |
| steps: | |
| - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd | |
| with: | |
| fetch-depth: 0 | |
| persist-credentials: false | |
| - id: scope | |
| env: | |
| EVENT: ${{ github.event_name }} | |
| BASE: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }} | |
| run: | | |
| set -euo pipefail | |
| applicable=true | |
| if [ "$EVENT" = merge_group ] || [ "$EVENT" = pull_request ]; then | |
| applicable=false | |
| if [ "$EVENT" = pull_request ]; then | |
| files=$(git diff --name-only --no-renames "$BASE"...HEAD) | |
| else | |
| files=$(git diff --name-only --no-renames "$BASE"..HEAD) | |
| fi | |
| # Git may quote names containing Unicode or control characters. | |
| if grep -Eq '^"?(docbuild/|lean-toolchain$|lakefile\.toml$|lake-manifest\.json$|python/lean_pool/(exposition/|documentation\.py$|indexes\.py$|quality\.py$|validation_cache\.py$|ci_artifacts\.py$|ci_cache\.py$|rebase_fastpath\.py$)|python/(pyproject\.toml|uv\.lock)$|scripts/exposition/|\.github/workflows/docs[^/]*\.yml$)' <<< "$files"; then | |
| applicable=true | |
| fi | |
| fi | |
| echo "applicable=$applicable" >> "$GITHUB_OUTPUT" | |
| # Cheap configuration/index checks remain independent of daily publication. | |
| preflight: | |
| needs: scope | |
| if: always() && (needs.scope.result != 'success' || needs.scope.outputs.applicable != 'false') | |
| runs-on: ubuntu-latest | |
| name: Documentation preflight | |
| outputs: | |
| build_revision: ${{ steps.build-identity.outputs.revision }} | |
| readme_only: ${{ steps.scope.outputs.readme_only }} | |
| rebase_only: ${{ steps.rebase.outputs.rebase_only }} | |
| steps: | |
| - name: Require successful change classification | |
| env: | |
| SCOPE_RESULT: ${{ needs.scope.result }} | |
| APPLICABLE: ${{ needs.scope.outputs.applicable }} | |
| run: | | |
| if [ "$SCOPE_RESULT" != success ] || [ "$APPLICABLE" != true ]; then | |
| echo "::error::Change classification failed; required validation cannot be skipped." | |
| exit 1 | |
| fi | |
| - name: Checkout project | |
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd | |
| with: | |
| fetch-depth: 0 | |
| - name: Install Python tooling runtime | |
| uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff | |
| with: | |
| enable-cache: true | |
| - name: Identify compiled Lean sources | |
| id: build-identity | |
| run: | | |
| set -euo pipefail | |
| revision=$(PYTHONPATH=python python3 -m lean_pool.ci_cache revision) | |
| echo "revision=$revision" >> "$GITHUB_OUTPUT" | |
| - name: Detect README-only change | |
| id: scope | |
| env: | |
| BASE_SHA: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }} | |
| EVENT_NAME: ${{ github.event_name }} | |
| HEAD_SHA: ${{ github.event.merge_group.head_sha || github.event.pull_request.head.sha }} | |
| run: | | |
| set -euo pipefail | |
| readme_only=false | |
| if [ "$EVENT_NAME" = "pull_request" ]; then | |
| files="$(git diff --name-only --no-renames "$BASE_SHA"..."$HEAD_SHA")" | |
| if [ "$files" = "README.md" ]; then | |
| readme_only=true | |
| fi | |
| fi | |
| echo "readme_only=$readme_only" >> "$GITHUB_OUTPUT" | |
| echo "README-only change: $readme_only" | |
| - name: Verify prior documentation preflight for a content-only rebase | |
| id: rebase | |
| if: github.event_name == 'pull_request' && steps.scope.outputs.readme_only != 'true' | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| REPOSITORY: ${{ github.repository }} | |
| PR_NUMBER: ${{ github.event.pull_request.number }} | |
| HEAD_SHA: ${{ github.event.merge_group.head_sha || github.event.pull_request.head.sha }} | |
| BASE_SHA: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }} | |
| run: | | |
| decision=$(PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath decide \ | |
| --workflow docs.yml --repository "$REPOSITORY" --number "$PR_NUMBER" \ | |
| --head "$HEAD_SHA" --base "$BASE_SHA") | |
| echo "rebase_only=$(echo "$decision" | python3 -c 'import json,sys; print(str(json.load(sys.stdin)["eligible"]).lower())')" >> "$GITHUB_OUTPUT" | |
| echo "$decision" | |
| # docbuild deliberately reuses the root workspace's compiled artifacts. | |
| # Fail before restoring anything if those workspaces ever diverge. | |
| - name: Check documentation workspace compatibility | |
| if: steps.scope.outputs.readme_only != 'true' | |
| run: | | |
| set -euo pipefail | |
| if ! cmp lean-toolchain docbuild/lean-toolchain; then | |
| echo "::error::Root and documentation workspaces use different Lean toolchains." | |
| exit 1 | |
| fi | |
| root_mathlib=$(jq -r '.packages[] | select(.name == "mathlib") | .rev' lake-manifest.json) | |
| docs_mathlib=$(jq -r '.packages[] | select(.name == "mathlib") | .rev' docbuild/lake-manifest.json) | |
| if [ -z "$root_mathlib" ] || [ "$root_mathlib" = "null" ]; then | |
| echo "::error::Root lake-manifest.json has no Mathlib revision." | |
| exit 1 | |
| fi | |
| if [ -z "$docs_mathlib" ] || [ "$docs_mathlib" = "null" ]; then | |
| echo "::error::docbuild/lake-manifest.json has no Mathlib revision." | |
| exit 1 | |
| fi | |
| if [ "$root_mathlib" != "$docs_mathlib" ]; then | |
| echo "::error::Root Mathlib revision $root_mathlib does not match docbuild ($docs_mathlib)." | |
| exit 1 | |
| fi | |
| # Preflight needs the toolchain and dependencies, not the pool build. | |
| # Stable dependencies are shared with CI without a new copy per commit. | |
| - name: Restore Lean dependencies | |
| id: dependency-cache | |
| if: steps.scope.outputs.readme_only != 'true' && steps.rebase.outputs.rebase_only != 'true' | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: | | |
| ~/.elan | |
| .lake/packages | |
| key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} | |
| - name: Install Lean | |
| if: steps.scope.outputs.readme_only != 'true' && steps.rebase.outputs.rebase_only != 'true' | |
| uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 | |
| with: | |
| auto-config: false | |
| use-github-cache: false | |
| use-mathlib-cache: false | |
| # A package directory from a restored cache does not prove that its | |
| # oleans match the current manifest. `cache get` is incremental, so run it | |
| # unconditionally and then verify the checkout revision. | |
| - name: Install and verify Mathlib cache | |
| if: steps.scope.outputs.readme_only != 'true' && steps.rebase.outputs.rebase_only != 'true' | |
| run: | | |
| set -euo pipefail | |
| ~/.elan/bin/lake exe cache get | |
| expected=$(jq -r '.packages[] | select(.name == "mathlib") | .rev' lake-manifest.json) | |
| actual=$(git -C .lake/packages/mathlib rev-parse HEAD) | |
| if [ "$actual" != "$expected" ]; then | |
| echo "::error::Mathlib checkout $actual does not match lake-manifest.json ($expected)." | |
| exit 1 | |
| fi | |
| - name: Check generated roots | |
| if: steps.scope.outputs.readme_only != 'true' && steps.rebase.outputs.rebase_only != 'true' | |
| run: ~/.elan/bin/lake exe mk_all --check | |
| - name: Check regenerated LeanPool root without Lean | |
| if: steps.rebase.outputs.rebase_only == 'true' | |
| run: PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath check-index |