build and deploy mathlib4 docs #220
This file contains 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 mathlib4 docs | |
| on: | |
| workflow_dispatch: | |
| schedule: | |
| - cron: '0 */8 * * *' # every 8 hours | |
| # Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages | |
| permissions: | |
| contents: read | |
| pages: write | |
| id-token: write | |
| jobs: | |
| build: | |
| name: build and deploy mathlib4 docs | |
| runs-on: doc-gen | |
| steps: | |
| - name: clean up | |
| run: | | |
| rm -rf mathlib4 | |
| rm -rf workaround | |
| rm -rf $HOME/.elan | |
| rm -rf $HOME/.cache/mathlib | |
| - name: Checkout repo | |
| uses: actions/checkout@v3 | |
| with: | |
| repository: leanprover-community/mathlib4 | |
| path: mathlib4 | |
| - name: install elan | |
| run: | | |
| set -o pipefail | |
| curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| - name: get cache | |
| working-directory: mathlib4 | |
| run: lake exe cache get | |
| - name: build mathlib | |
| working-directory: mathlib4 | |
| run: env LEAN_ABORT_ON_PANIC=1 lake build | |
| - name: create dummy docs project | |
| run: | | |
| # Workaround for the lake issue | |
| elan default leanprover/lean4:nightly | |
| lake new workaround | |
| cd workaround | |
| cp -f ../mathlib4/lean-toolchain . | |
| echo 'require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"' >> lakefile.lean | |
| echo 'require «mathlib» from ".." / "mathlib4"' >> lakefile.lean | |
| # doc-gen4 expects to work on github repos with at least one commit | |
| git add . | |
| git commit -m "workaround" | |
| git remote add origin "https://github.com/leanprover/workaround" | |
| mkdir lake-packages | |
| cp -r ../mathlib4/lake-packages/* lake-packages/ | |
| lake update | |
| - name: build doc-gen4 | |
| working-directory: workaround | |
| run: | | |
| lake build doc-gen4 | |
| - name: generate docs | |
| working-directory: workaround | |
| run: | | |
| lake build Std:docs Qq:docs Aesop:docs ProofWidgets:docs Mathlib:docs Archive:docs Counterexamples:docs docs:docs | |
| - name: copy extra files | |
| run: | | |
| cp mathlib4/docs/{100.yaml,overview.yaml,undergrad.yaml} workaround/build/doc | |
| - name: Upload artifact | |
| uses: actions/upload-pages-artifact@v1 | |
| with: | |
| path: 'workaround/build/doc' | |
| - name: Deploy to GitHub Pages | |
| id: deployment | |
| uses: actions/deploy-pages@v1 | |
| - name: clean up | |
| if: always() | |
| run: | | |
| rm -rf mathlib4 | |
| rm -rf workaround | |
| rm -rf $HOME/.elan | |
| rm -rf $HOME/.cache/mathlib |