chore: move to v4.16.0-rc2 #55
Workflow file for this run
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 docs | |
| on: | |
| push: | |
| branches: | |
| - master | |
| pull_request: | |
| permissions: | |
| contents: read | |
| pages: write | |
| id-token: write | |
| jobs: | |
| build: | |
| name: build and deploy docs | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: clean up | |
| run: | | |
| rm -rf $HOME/.elan | |
| rm -rf $HOME/.cache/mathlib | |
| - name: Checkout repo | |
| uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 2 | |
| lfs: true | |
| - 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 | |
| run: | | |
| elan default $(cat lean-toolchain) | |
| - name: get cache | |
| run: lake exe cache get | |
| - name: build algorithm | |
| run: env LEAN_ABORT_ON_PANIC=1 lake build | |
| - name: build doc-gen4 | |
| run: | | |
| lake build doc-gen4 | |
| - name: build import graph | |
| run: | | |
| lake exe graph algorithm.html | |
| - name: generate docs | |
| run: | | |
| lake build Algorithm:docs | |
| lake build Algorithm:docsHeader | |
| - name: copy import graph | |
| run: | | |
| cp algorithm.html ./.lake/build/doc | |
| - name: Upload artifact | |
| uses: actions/upload-pages-artifact@v3 | |
| with: | |
| path: './.lake/build/doc' | |
| - name: Deploy to GitHub Pages | |
| if: github.ref == 'refs/heads/master' | |
| id: deployment | |
| uses: actions/deploy-pages@v4 | |
| - name: clean up | |
| run: | | |
| rm -rf $HOME/.elan | |
| rm -rf $HOME/.cache/mathlib |