0.230.538 — ChannelCapacity gibbs_inequality deleted, entropy_le_log_… #315
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. The Lake `:docs` facet cascades | |
| # docInfo jobs into Mathlib (~2700+ targets for any Linglib | |
| # module that imports mathlib), which OOMs the runner. The | |
| # CLI's `single` only writes docs for the named module — its | |
| # imports are loaded into memory but not documented. | |
| 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 | |
| export BUILD DOCGEN SRC_URI DB | |
| # Remove stale DB — schema changes across doc-gen4 versions | |
| # cause "no such table" errors if an old DB is reused. | |
| 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 in parallel (-P 4 cores). | |
| # Each invocation writes to a shared SQLite db with WAL + | |
| # 24h busy timeout (see doc-gen4/Main.lean:walCheckpoint), | |
| # and updateModuleDb uses immediate transactions per | |
| # 100-module batch, so concurrent writers are safe. | |
| # Memory: each `single` peaks ~3-4 GB (mathlib import closure); | |
| # 4 in parallel ≈ 12-16 GB on a 16 GB runner. If we OOM, | |
| # drop -P to 2. | |
| find Linglib -name '*.lean' | sort | \ | |
| xargs -I{} -P 4 sh -c ' | |
| f="$1" | |
| mod=$(echo "$f" | sed "s|/|.|g; s|\.lean$||") | |
| echo " doc: $mod" | |
| $DOCGEN single --build "$BUILD" "$mod" "$DB" "$SRC_URI/$f" || true | |
| ' _ {} | |
| # 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 |