Inheritance/ mathlib-PR cleanup quick wins (0.230.57): pop Prototype … #301
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: Build and Deploy Docs | |
| on: | |
| push: | |
| branches: [main] | |
| workflow_dispatch: | |
| env: | |
| ELAN_NO_OVERRIDE_NOTICE: 1 | |
| permissions: | |
| contents: read | |
| pages: write | |
| id-token: write | |
| concurrency: | |
| group: "pages" | |
| cancel-in-progress: true | |
| jobs: | |
| build: | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 120 | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| with: | |
| submodules: true | |
| - name: Install elan | |
| run: | | |
| curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| - name: Install and activate toolchain | |
| run: | | |
| elan toolchain install $(cat lean-toolchain) | |
| elan override set $(cat lean-toolchain) | |
| lake --version | |
| - name: Cache .lake | |
| uses: actions/cache@v4 | |
| with: | |
| path: .lake | |
| key: lake-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-docs-${{ hashFiles('Linglib/**/*.lean', 'Linglib.lean') }} | |
| restore-keys: | | |
| lake-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-docs- | |
| lake-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}- | |
| - name: Get Mathlib cache | |
| run: lake exe cache get | |
| - name: Build project | |
| run: lake build | |
| - name: Build documentation (Linglib only, skip Mathlib) | |
| run: | | |
| # Use doc-gen4 CLI directly to avoid Lake facet processing ALL | |
| # transitive deps (Mathlib/Lean core), which OOMs the runner. | |
| lake build doc-gen4 | |
| BUILD=.lake/build | |
| DOCGEN="lake exe doc-gen4" | |
| REPO_URL="https://github.com/${{ github.repository }}" | |
| COMMIT="${{ github.sha }}" | |
| SRC_URI="$REPO_URL/blob/$COMMIT" | |
| DB=api-docs.db | |
| # Remove stale DB — schema changes across doc-gen4 versions | |
| # cause "no such table" errors if an old DB is reused. | |
| # Delete both possible locations (build dir and repo root). | |
| rm -f "$BUILD/$DB" "$DB" | |
| # Bibliography prepass | |
| if [ -f docs/references.bib ]; then | |
| $DOCGEN bibPrepass --build "$BUILD" docs/references.bib | |
| elif [ -f docs/references.json ]; then | |
| $DOCGEN bibPrepass --build "$BUILD" --json docs/references.json | |
| else | |
| $DOCGEN bibPrepass --build "$BUILD" --none | |
| fi | |
| # Document root module (may fail if Linglib.olean missing — non-fatal) | |
| $DOCGEN single --build "$BUILD" Linglib "$DB" "$SRC_URI/Linglib.lean" || true | |
| # Document all Linglib submodules | |
| find Linglib -name '*.lean' | sort | while read -r f; do | |
| mod=$(echo "$f" | sed 's|/|.|g; s|\.lean$||') | |
| echo " doc: $mod" | |
| $DOCGEN single --build "$BUILD" "$mod" "$DB" "$SRC_URI/$f" || true | |
| done | |
| # Generate HTML + search index from database | |
| # NOTE: fromDb treats the db arg as a literal path (not relative | |
| # to --build), unlike single/genCore which prepend --build. | |
| $DOCGEN fromDb --build "$BUILD" "$BUILD/$DB" | |
| - name: Install Hugo | |
| uses: peaceiris/actions-hugo@v3 | |
| with: | |
| hugo-version: 'latest' | |
| extended: true | |
| - name: Build blog | |
| working-directory: blog | |
| run: hugo --minify | |
| - name: Compose site | |
| run: | | |
| mkdir -p .lake/build/doc-site | |
| # Hugo output → site root | |
| cp -r blog/public/* .lake/build/doc-site/ | |
| # doc-gen4 output → /docs/ subdirectory | |
| mkdir -p .lake/build/doc-site/docs | |
| cp -r .lake/build/doc/* .lake/build/doc-site/docs/ | |
| - name: Setup Pages | |
| uses: actions/configure-pages@v4 | |
| - name: Upload artifact | |
| uses: actions/upload-pages-artifact@v3 | |
| with: | |
| path: '.lake/build/doc-site' | |
| deploy: | |
| environment: | |
| name: github-pages | |
| url: ${{ steps.deployment.outputs.page_url }} | |
| runs-on: ubuntu-latest | |
| needs: build | |
| steps: | |
| - name: Deploy to GitHub Pages | |
| id: deployment | |
| uses: actions/deploy-pages@v4 |