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
| on: | |
| push: | |
| branches: | |
| - master | |
| # Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages | |
| permissions: | |
| contents: read | |
| pages: write | |
| id-token: write | |
| jobs: | |
| style_lint: | |
| name: Lint style | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Check for long lines | |
| if: always() | |
| run: | | |
| ! (find Clt -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://') | |
| - name: Don't 'import Mathlib', use precise imports | |
| if: always() | |
| run: | | |
| ! (find Clt -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Mathlib$') | |
| build_project: | |
| runs-on: ubuntu-latest | |
| name: Build project | |
| steps: | |
| - name: Checkout project | |
| uses: actions/checkout@v2 | |
| with: | |
| fetch-depth: 0 | |
| - name: Print files to upstream | |
| run: | | |
| grep -r --files-without-match 'import Clt' Clt | sort > 1.txt | |
| grep -r --files-with-match 'sorry' Clt | sort > 2.txt | |
| mkdir -p docs/_includes | |
| comm -23 1.txt 2.txt | sed -e 's/^\(.*\)$/- [`\1`](https:\/\/github.com\/RemyDegenne\/Clt\/blob\/master\/\1)/' > docs/_includes/files_to_upstream.md | |
| rm 1.txt 2.txt | |
| - name: Install elan | |
| run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.0.0 | |
| - name: Get cache | |
| run: ~/.elan/bin/lake -Kenv=dev exe cache get || true | |
| - name: Build project | |
| run: ~/.elan/bin/lake -Kenv=dev build Clt | |
| - name: Cache mathlib docs | |
| uses: actions/cache@v3 | |
| with: | |
| path: | | |
| .lake/build/doc/Init | |
| .lake/build/doc/Lake | |
| .lake/build/doc/Lean | |
| .lake/build/doc/Std | |
| .lake/build/doc/Mathlib | |
| .lake/build/doc/declarations | |
| key: MathlibDoc-${{ hashFiles('lake-manifest.json') }} | |
| restore-keys: | | |
| MathlibDoc- | |
| - name: Build documentation | |
| run: ~/.elan/bin/lake -Kenv=dev build Clt:docs | |
| - name: Copy documentation to `docs/docs` | |
| run: | | |
| mv .lake/build/doc docs/docs | |
| #- name: Upload docs & blueprint artifact | |
| # uses: actions/upload-pages-artifact@v1 | |
| # with: | |
| # path: docs/_site | |
| - name: Make sure the cache works | |
| run: | | |
| mv docs/docs .lake/build/doc |