Merge pull request #5 from ImperialCollegeLondon/faster-ci #11
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: | |
| - main | |
| # 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 FLT -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 FLT -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: Install elan | |
| run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none | |
| - name: Get cache | |
| run: ~/.elan/bin/lake -Kenv=dev exe cache get || true | |
| - name: Build project | |
| run: ~/.elan/bin/lake -Kenv=dev build FLT | |
| - 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 | |
| key: DocGen4-${{ hashFiles('lake-manifest.json') }} | |
| restore-keys: | | |
| DocGen4- | |
| - name: Build documentation | |
| run: ~/.elan/bin/lake -Kenv=dev build FLT:docs | |
| - name: Install Python | |
| uses: actions/setup-python@v4 | |
| with: | |
| python-version: '3.9' | |
| cache: 'pip' # caching pip dependencies | |
| - name: Install blueprint apt deps with cache | |
| uses: awalsh128/cache-apt-pkgs-action@latest | |
| with: | |
| # texlive-binaries is for kpsewhich, which is a dependency of plastex/blueprint | |
| packages: graphviz libgraphviz-dev pdf2svg dvisvgm texlive-binaries | |
| version: 1.0 | |
| - name: Install blueprint dependencies | |
| run: | | |
| pip install -r blueprint/requirements.txt | |
| - name: Build blueprint PDF | |
| uses: xu-cheng/texlive-action@v2 | |
| with: | |
| scheme: full | |
| run: | | |
| apk update | |
| apk add --update make py3-pip git | |
| git config --global --add safe.directory $GITHUB_WORKSPACE | |
| git config --global --add safe.directory `pwd` | |
| python3 -m pip install --upgrade pip requests wheel | |
| python3 -m pip install invoke | |
| inv bp | |
| - name: Build blueprint website and copy blueprint to `docs/blueprint` | |
| run: | | |
| inv web | |
| inv copy | |
| - name: Copy Lean documentation to `docs/docs` | |
| run: | | |
| mv .lake/build/doc docs/docs | |
| - name: Bundle dependencies | |
| uses: ruby/setup-ruby@v1 | |
| with: | |
| working-directory: docs | |
| ruby-version: "3.0" # Not needed with a .ruby-version file | |
| bundler-cache: true # runs 'bundle install' and caches installed gems automatically | |
| - name: Bundle website | |
| working-directory: docs | |
| run: JEKYLL_ENV=production bundle exec jekyll build | |
| - name: Upload docs & blueprint artifact | |
| uses: actions/upload-pages-artifact@v1 | |
| with: | |
| path: docs/_site | |
| - name: Deploy to GitHub Pages | |
| id: deployment | |
| uses: actions/deploy-pages@v1 | |
| - name: Make sure the cache works | |
| run: | | |
| mv docs/docs .lake/build/doc |