build and deploy docs #16618
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 docs | |
| on: | |
| schedule: | |
| - cron: '0 */2 * * *' # every 2 hours | |
| push: | |
| pull_request: | |
| jobs: | |
| build: | |
| name: build and deploy docs | |
| runs-on: doc-gen | |
| steps: | |
| - name: Checkout repo | |
| uses: actions/checkout@v2 | |
| - name: Checkout mathlib | |
| run: git clone https://github.com/leanprover-community/mathlib | |
| - 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 | |
| cd mathlib | |
| ~/.elan/bin/lean --version | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| # - name: install Python | |
| # uses: actions/setup-python@v1 | |
| # with: | |
| # python-version: 3.8 | |
| - name: setup python venv | |
| run: | | |
| python3 -m venv .venv | |
| echo "$PWD/.venv/bin" >> $GITHUB_PATH | |
| - name: install Python dependencies | |
| run: | | |
| python -m pip install --upgrade pip | |
| pip install -r requirements.txt | |
| pip install pytest | |
| - name: run tests | |
| # note this runs tests against the pinned copy of mathlib, to make them less likely to break | |
| # the cronjob build. | |
| run: | | |
| leanproject get-mathlib-cache | |
| lean --make test | |
| pytest test/ | |
| - name: run leanproject | |
| run: | | |
| cd mathlib | |
| leanproject up | |
| - name: generate docs | |
| run: | | |
| if [ "$github_repo" = "leanprover-community/doc-gen" ] && [ "$github_ref" = "refs/heads/master" ]; then | |
| deploy="true" | |
| else | |
| deploy="false" | |
| fi | |
| ./deploy_docs.sh "mathlib" ".." "mathlib" "leanprover-community" "mathlib_docs" "$deploy" | |
| env: | |
| DEPLOY_GITHUB_TOKEN: ${{ secrets.DEPLOY_GITHUB_TOKEN }} | |
| github_repo: ${{ github.repository }} | |
| github_event: ${{ github.event_name }} | |
| github_ref: ${{ github.ref }} | |
| - name: Upload export.json | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| path: export.json | |
| - name: clean up working directory and elan | |
| if: always() | |
| run: rm -rf * $HOME/.elan $HOME/.mathlib |