Chierchia 2006: deduplicate fragment bridges, fix section headers and… #272
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: | | |
| # Build doc-gen4 executable | |
| 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" | |
| # Bib prepass (--none if no bib file) | |
| 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 | |
| # Generate docs for each Linglib module only (skip Mathlib/Init/Std/Lean) | |
| 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" "$SRC_URI/$f" || true | |
| done | |
| # Generate core docs for Init only (needed for basic type links) | |
| $DOCGEN genCore --build "$BUILD" Init || true | |
| # Build the search index | |
| $DOCGEN index --build "$BUILD" | |
| - 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 |