build and deploy mathlib4 docs #1593
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_docs | |
| rm -rf mathlib4 | |
| rm -rf workaround | |
| rm -rf $HOME/.elan | |
| rm -rf $HOME/.cache/mathlib | |
| - name: Checkout repo | |
| uses: actions/checkout@v4 | |
| with: | |
| repository: leanprover-community/mathlib4_docs | |
| path: mathlib4_docs | |
| - name: Checkout mathlib | |
| uses: actions/checkout@v4 | |
| 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: set default toolchain | |
| working-directory: mathlib4 | |
| run: | | |
| elan default $(cat lean-toolchain) | |
| - 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: | | |
| lake new workaround lib | |
| cd workaround | |
| cp -f ../mathlib4/lean-toolchain . | |
| cp -f ../mathlib4_docs/lakefile.toml . | |
| # doc-gen4 expects to work on github repos with at least one commit | |
| git config user.email "[email protected]" | |
| git config user.name "mathlib4_docs CI" | |
| git add . | |
| git commit -m "workaround" | |
| git remote add origin "https://github.com/leanprover-community/workaround" | |
| mkdir -p .lake/packages | |
| cp -r ../mathlib4/.lake/packages/* .lake/packages | |
| lake update | |
| # Copy references.bib over while doc-gen lacks support for subproject references.bib | |
| mkdir docs/ | |
| cp ../mathlib4/docs/references.bib docs/references.bib | |
| - name: build doc-gen4 | |
| working-directory: workaround | |
| run: | | |
| lake build doc-gen4 | |
| - name: build import graph | |
| working-directory: mathlib4 | |
| run: | | |
| lake exe graph mathlib.html | |
| - name: generate docs | |
| working-directory: workaround | |
| run: | | |
| lake build Batteries:docs Qq:docs Aesop:docs ProofWidgets:docs Mathlib:docs Archive:docs Counterexamples:docs docs:docs | |
| lake build Mathlib:docsHeader | |
| - name: copy extra files | |
| run: | | |
| cp mathlib4/docs/{100.yaml,1000.yaml,overview.yaml,undergrad.yaml} workaround/.lake/build/doc | |
| - name: copy import graph | |
| run: | | |
| cp mathlib4/mathlib.html workaround/.lake/build/doc | |
| - name: Upload artifact | |
| uses: actions/upload-pages-artifact@v3 | |
| with: | |
| path: 'workaround/.lake/build/doc' | |
| - name: Deploy to GitHub Pages | |
| id: deployment | |
| uses: actions/deploy-pages@v4 | |
| - name: clean up | |
| if: always() | |
| run: | | |
| rm -rf mathlib4_docs | |
| rm -rf mathlib4 | |
| rm -rf workaround | |
| rm -rf $HOME/.elan | |
| rm -rf $HOME/.cache/mathlib |