Merge branch 'main' of https://github.com/teorth/analysis #13
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://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y | |
| - name: Get Mathlib cache | |
| run: ~/.elan/bin/lake exe cache get || true | |
| working-directory: ./analysis | |
| - name: Cache mathlib API docs | |
| uses: actions/cache@v4 | |
| with: | |
| path: | | |
| ./analysis/.lake/build/doc/Init | |
| ./analysis/.lake/build/doc/Lake | |
| ./analysis/.lake/build/doc/Lean | |
| ./analysis/.lake/build/doc/Std | |
| ./analysis/.lake/build/doc/Mathlib | |
| ./analysis/.lake/build/doc/declarations | |
| ./analysis/.lake/build/doc/find | |
| ./analysis/.lake/build/doc/*.* | |
| !./analysis/.lake/build/doc/declarations/declaration-data-Analysis* | |
| key: MathlibDoc-${{ hashFiles('lake-manifest.json') }} | |
| restore-keys: MathlibDoc- | |
| - name: Build doc-gen | |
| run: ~/.elan/bin/lake -R -Kenv=dev build Analysis:docs | |
| 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: 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 |