|
| 1 | +name: Docgen test on nightly-testing |
| 2 | + |
| 3 | +on: |
| 4 | + schedule: |
| 5 | + - cron: '37 1 * * *' # Run at 01:37 UTC every day (generated by fair dice roll) |
| 6 | + workflow_dispatch: |
| 7 | + |
| 8 | +jobs: |
| 9 | + build: |
| 10 | + name: build mathlib4-nightly-testing docs |
| 11 | + runs-on: doc-gen |
| 12 | + if: github.repository == 'leanprover-community/mathlib4-nightly-testing' |
| 13 | + steps: |
| 14 | + - name: clean up |
| 15 | + run: | |
| 16 | + rm -rf docbuild |
| 17 | + rm -rf "$HOME/.elan" |
| 18 | + rm -rf "$HOME/.cache/mathlib" |
| 19 | +
|
| 20 | + - name: Checkout mathlib |
| 21 | + uses: actions/checkout@v4 |
| 22 | + with: |
| 23 | + repository: leanprover-community/mathlib4-nightly-testing |
| 24 | + ref: nightly-testing-green |
| 25 | + |
| 26 | + - name: Add upstream |
| 27 | + run: | |
| 28 | + # Add the nightly-testing remote if it does not exist already, otherwise `lake exe cache` gets confused. |
| 29 | + (git remote | grep -q '^nightly-testing$') || git remote add nightly-testing https://github.com/leanprover-community/mathlib4-nightly-testing.git |
| 30 | +
|
| 31 | + - name: Build and lint the project. |
| 32 | + id: build-lean |
| 33 | + uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # v1.2.0 |
| 34 | + with: |
| 35 | + use-mathlib-cache: true |
| 36 | + |
| 37 | + # This is not quite the same as `docgen-action` does, since we do not actually want to upload the result. |
| 38 | + - name: create dummy docs project |
| 39 | + run: | |
| 40 | + # Build HTML documentation for the project |
| 41 | + # The output will be located in docbuild/docs |
| 42 | +
|
| 43 | + # Create a temporary docbuild folder |
| 44 | + mkdir -p docbuild |
| 45 | +
|
| 46 | + # Template lakefile.toml |
| 47 | + cat << EOF > docbuild/lakefile.toml |
| 48 | + name = "docbuild" |
| 49 | + reservoir = false |
| 50 | + version = "0.1.0" |
| 51 | + packagesDir = "../.lake/packages" |
| 52 | +
|
| 53 | + [[require]] |
| 54 | + name = "mathlib" |
| 55 | + path = "../" |
| 56 | +
|
| 57 | + [[require]] |
| 58 | + scope = "leanprover" |
| 59 | + name = "doc-gen4" |
| 60 | + rev = "main" |
| 61 | + EOF |
| 62 | +
|
| 63 | + # Initialise docbuild as a Lean project |
| 64 | + cd docbuild |
| 65 | +
|
| 66 | + # No need to reinstall packages if we can just copy them from Mathlib. |
| 67 | + mkdir -p .lake/packages |
| 68 | + cp -r ../.lake/packages/* .lake/packages |
| 69 | + cp ../lean-toolchain . # Use Mathlib's (nightly) toolchain. |
| 70 | +
|
| 71 | + # Disable an error message due to a non-blocking bug. See Zulip |
| 72 | + MATHLIB_NO_CACHE_ON_UPDATE=1 lake update "$NAME" |
| 73 | +
|
| 74 | + # Copy references.bib over while doc-gen lacks support for subproject references.bib |
| 75 | + mkdir docs/ |
| 76 | + cp ../docs/references.bib docs/references.bib |
| 77 | +
|
| 78 | + - name: build doc-gen4 |
| 79 | + working-directory: docbuild |
| 80 | + run: | |
| 81 | + env DISABLE_EQUATIONS=1 lake build doc-gen4 |
| 82 | +
|
| 83 | + - name: build import graph |
| 84 | + working-directory: . |
| 85 | + run: | |
| 86 | + lake exe graph mathlib.html |
| 87 | +
|
| 88 | + - name: generate docs |
| 89 | + working-directory: docbuild |
| 90 | + run: | |
| 91 | + lake build Batteries:docs Qq:docs Aesop:docs ProofWidgets:docs Mathlib:docs Archive:docs Counterexamples:docs docs:docs |
| 92 | + lake build Mathlib:docsHeader |
| 93 | +
|
| 94 | + - name: clean up |
| 95 | + if: always() |
| 96 | + run: | |
| 97 | + rm -rf docbuild |
| 98 | + rm -rf "$HOME/.elan" |
| 99 | + rm -rf "$HOME/.cache/mathlib" |
| 100 | +
|
| 101 | + - name: Send success message on Zulip |
| 102 | + uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2 |
| 103 | + if: success() |
| 104 | + with: |
| 105 | + api-key: ${{ secrets.ZULIP_API_KEY }} |
| 106 | + email: 'github-mathlib4-bot@leanprover.zulipchat.com' |
| 107 | + organization-url: 'https://leanprover.zulipchat.com' |
| 108 | + to: 'nightly-testing' |
| 109 | + type: 'stream' |
| 110 | + topic: 'Docgen status updates' |
| 111 | + content: | |
| 112 | + ✅ 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 }})). |
| 113 | +
|
| 114 | + - name: Send failure message on Zulip |
| 115 | + uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2 |
| 116 | + if: failure() |
| 117 | + with: |
| 118 | + api-key: ${{ secrets.ZULIP_API_KEY }} |
| 119 | + email: 'github-mathlib4-bot@leanprover.zulipchat.com' |
| 120 | + organization-url: 'https://leanprover.zulipchat.com' |
| 121 | + to: 'nightly-testing' |
| 122 | + type: 'stream' |
| 123 | + topic: 'Docgen status updates' |
| 124 | + content: | |
| 125 | + ❌ 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 }})). |
| 126 | + This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4. |
0 commit comments