adjust cache, only upload website from main branch #768
Workflow file for this run
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
| # based on https://github.com/leanprover-community/lean-liquid/blob/master/.github/workflow/build.yml | |
| # with additions from https://github.com/PatrickMassot/leanblueprint | |
| on: | |
| push: | |
| name: CI | |
| # Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages | |
| permissions: | |
| contents: read # Read access to repository contents | |
| pages: write # Write access to GitHub Pages | |
| id-token: write # Write access to ID tokens | |
| jobs: | |
| build: | |
| name: Build PDL | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout project | |
| uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: ${{ env.GIT_HISTORY_DEPTH }} | |
| - 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 | |
| ~/.elan/bin/lean --version | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| - name: make pdl | |
| run: make pdl | |
| - name: Cache both .lake/build folders | |
| uses: actions/cache@v4 | |
| with: | |
| path: | | |
| .lake/build | |
| docbuild/.lake/build | |
| key: lakeBuild-${{ hashFiles('lake-manifest.json') }} | |
| restore-keys: lakeBuild- | |
| - name: Build documentation | |
| run: make doc | |
| - name: Copy documentation to `home_page/docs` | |
| if: github.ref == 'ref/head/main' | |
| run: | | |
| mkdir -p home_page | |
| cp -r docbuild/.lake/build/doc home_page/docs | |
| - name: Remove unnecessary lake files from documentation in `home_page/docs` | |
| if: github.ref == 'ref/head/main' | |
| run: | | |
| find home_page/docs -name "*.trace" -delete | |
| find home_page/docs -name "*.hash" -delete | |
| - name: Upload website | |
| if: github.ref == 'ref/head/main' | |
| uses: actions/upload-pages-artifact@v3 | |
| with: | |
| path: 'home_page/' | |
| - name: Deploy to GitHub Pages | |
| if: github.ref == 'ref/head/main' | |
| id: deployment | |
| uses: actions/deploy-pages@v4 | |
| bml: | |
| name: Build BML | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: ${{ env.GIT_HISTORY_DEPTH }} | |
| - 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 | |
| ~/.elan/bin/lean --version | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| - name: make bml | |
| run: make bml | |
| stats: | |
| name: Stats | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: install ripgrep | |
| run: sudo apt install -y ripgrep | |
| - name: PDL count lines in src | |
| run: | | |
| shopt -s globstar | |
| wc -l Pdl/**/*.lean | |
| - name: PDL count sorries | |
| run: | | |
| rg --count-matches sorry Pdl | awk -F ':' 'BEGIN {sum = 0} {sum += $2} {print $2 " " $1} END {print sum " sorries in total"}' | |
| - name: BML count lines in src | |
| run: | | |
| shopt -s globstar | |
| wc -l Bml/**/*.lean | |
| - name: BML count sorries | |
| run: | | |
| rg --count-matches sorry Bml | awk -F ':' 'BEGIN {sum = 0} {sum += $2} {print $2 " " $1} END {print sum " sorries in total"}' |