build and deploy mathlib4 docs #3017
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 mathlib4 docs | |
| on: | |
| push: | |
| branches: | |
| - main | |
| pull_request: | |
| 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@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1 | |
| with: | |
| repository: leanprover-community/mathlib4_docs | |
| path: mathlib4_docs | |
| - name: Checkout mathlib | |
| uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1 | |
| 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 "mathlib4_docs@leanprover-community.github.io" | |
| 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@7b1f4a764d45c48632c6b24a0339c27f5614fb0b # v4.0.0 | |
| with: | |
| path: 'workaround/.lake/build/doc' | |
| - name: Deploy to GitHub Pages | |
| if: github.ref == 'refs/heads/main' | |
| id: deployment | |
| uses: actions/deploy-pages@d6db90164ac5ed86f2b6aed7e0febac5b3c0c03e # v4.0.5 | |
| - 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 | |
| notify_if_failed: | |
| runs-on: ubuntu-latest | |
| needs: build | |
| if: always() | |
| steps: | |
| - name: Checkout repository | |
| uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1 | |
| - name: Get job status and URLs | |
| id: get-status | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| run: | | |
| JOB_NAME="build and deploy mathlib4 docs" | |
| # Get URL and conclusion for the specific job | |
| JOB_DATA=$(gh run view ${{ github.run_id }} --json jobs --jq \ | |
| ".jobs[] | select(.name == \"$JOB_NAME\")") | |
| JOB_URL=$(echo "$JOB_DATA" | jq -r '.url') | |
| JOB_CONCLUSION=$(echo "$JOB_DATA" | jq -r '.conclusion') | |
| echo "job_url=${JOB_URL}" | tee -a "$GITHUB_OUTPUT" | |
| echo "job_conclusion=${JOB_CONCLUSION}" | tee -a "$GITHUB_OUTPUT" | |
| - name: Post failure / cancelled message for mathlib_test_executable on Zulip | |
| if: steps.get-status.outputs.job_conclusion != 'success' | |
| uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2 | |
| with: | |
| api-key: ${{ secrets.ZULIP_API_KEY }} | |
| email: 'leanprover-community-monitor-runners-bot@leanprover.zulipchat.com' | |
| organization-url: 'https://leanprover.zulipchat.com' | |
| to: 'nightly-testing' | |
| type: 'stream' | |
| topic: 'mathlib4_docs failure' | |
| content: | | |
| ❌ mathlib4_docs [${{ steps.get-status.outputs.job_conclusion }}](${{ steps.get-status.outputs.job_url }}) on ${{ github.sha }} | |
| workflow-keepalive: | |
| if: github.event_name == 'schedule' | |
| runs-on: ubuntu-latest | |
| permissions: | |
| actions: write | |
| steps: | |
| - uses: liskin/gh-workflow-keepalive@f72ff1a1336129f29bf0166c0fd0ca6cf1bcb38c # v1.2.1 |