Docgen test on nightly-testing #81
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: Docgen test on nightly-testing | |
| on: | |
| schedule: | |
| - cron: '37 1 * * *' # Run at 01:37 UTC every day (generated by fair dice roll) | |
| workflow_dispatch: | |
| jobs: | |
| build: | |
| name: build mathlib4-nightly-testing docs | |
| runs-on: doc-gen | |
| if: github.repository == 'leanprover-community/mathlib4-nightly-testing' | |
| steps: | |
| - name: clean up | |
| run: | | |
| rm -rf docbuild | |
| rm -rf "$HOME/.elan" | |
| rm -rf "$HOME/.cache/mathlib" | |
| - name: Checkout mathlib | |
| uses: actions/checkout@v6.0.1 | |
| with: | |
| repository: leanprover-community/mathlib4-nightly-testing | |
| ref: nightly-testing-green | |
| - name: Add upstream | |
| run: | | |
| # Add the nightly-testing remote if it does not exist already, otherwise `lake exe cache` gets confused. | |
| (git remote | grep -q '^nightly-testing$') || git remote add nightly-testing https://github.com/leanprover-community/mathlib4-nightly-testing.git | |
| - name: Build and lint the project. | |
| id: build-lean | |
| uses: leanprover/lean-action@434f25c2f80ded67bba02502ad3a86f25db50709 # v1.3.0 | |
| with: | |
| use-mathlib-cache: true | |
| # This is not quite the same as `docgen-action` does, since we do not actually want to upload the result. | |
| - name: create dummy docs project | |
| run: | | |
| # Build HTML documentation for the project | |
| # The output will be located in docbuild/docs | |
| # Create a temporary docbuild folder | |
| mkdir -p docbuild | |
| # Template lakefile.toml | |
| cat << EOF > docbuild/lakefile.toml | |
| name = "docbuild" | |
| reservoir = false | |
| version = "0.1.0" | |
| packagesDir = "../.lake/packages" | |
| [[require]] | |
| name = "mathlib" | |
| path = "../" | |
| [[require]] | |
| scope = "leanprover" | |
| name = "doc-gen4" | |
| rev = "nightly-testing" | |
| EOF | |
| # Initialise docbuild as a Lean project | |
| cd docbuild | |
| # No need to reinstall packages if we can just copy them from Mathlib. | |
| mkdir -p .lake/packages | |
| cp -r ../.lake/packages/* .lake/packages | |
| cp ../lean-toolchain . # Use Mathlib's (nightly) toolchain. | |
| # Disable an error message due to a non-blocking bug. See Zulip | |
| MATHLIB_NO_CACHE_ON_UPDATE=1 lake update "$NAME" | |
| # Copy references.bib over while doc-gen lacks support for subproject references.bib | |
| mkdir docs/ | |
| cp ../docs/references.bib docs/references.bib | |
| - name: build doc-gen4 | |
| working-directory: docbuild | |
| run: | | |
| env DISABLE_EQUATIONS=1 lake build doc-gen4 | |
| - name: build import graph | |
| working-directory: . | |
| run: | | |
| lake exe graph mathlib.html | |
| - name: generate docs | |
| working-directory: docbuild | |
| run: | | |
| lake build Batteries:docs Qq:docs Aesop:docs ProofWidgets:docs Mathlib:docs Archive:docs Counterexamples:docs docs:docs | |
| lake build Mathlib:docsHeader | |
| - name: clean up | |
| if: always() | |
| run: | | |
| rm -rf docbuild | |
| rm -rf "$HOME/.elan" | |
| rm -rf "$HOME/.cache/mathlib" | |
| - name: Send success message on Zulip | |
| uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2 | |
| if: success() | |
| with: | |
| api-key: ${{ secrets.ZULIP_API_KEY }} | |
| email: 'github-mathlib4-bot@leanprover.zulipchat.com' | |
| organization-url: 'https://leanprover.zulipchat.com' | |
| to: 'nightly-testing' | |
| type: 'stream' | |
| topic: 'Docgen status updates' | |
| content: | | |
| ✅ The docgen run for Mathlib's [nightly-testing branch](https://github.com/leanprover-community/mathlib4-nightly-testing/tree/nightly-testing) has [succeeded](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) ([${{ github.sha }}](https://github.com/${{ github.repository }}/commit/${{ github.sha }})). | |
| - name: Send failure message on Zulip | |
| uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2 | |
| if: failure() | |
| with: | |
| api-key: ${{ secrets.ZULIP_API_KEY }} | |
| email: 'github-mathlib4-bot@leanprover.zulipchat.com' | |
| organization-url: 'https://leanprover.zulipchat.com' | |
| to: 'nightly-testing' | |
| type: 'stream' | |
| topic: 'Docgen status updates' | |
| content: | | |
| ❌ The docgen run for Mathlib's [nightly-testing branch](https://github.com/leanprover-community/mathlib4-nightly-testing/tree/nightly-testing) has [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) ([${{ github.sha }}](https://github.com/${{ github.repository }}/commit/${{ github.sha }})). | |
| This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4. |