Add useful comments #85
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
| on: | |
| push: | |
| branches: | |
| - master | |
| - gh-actions | |
| # 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: | |
| # Check for long lines in .lean files and report if any lines exceed 100 characters | |
| - name: Check for long lines | |
| if: always() | |
| run: | | |
| ! (find BonnAnalysis -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://') | |
| 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 leanprover/lean4:4.0.0 | |
| - name: Update docgen4 | |
| run: ~/.elan/bin/lake -R -Kenv=dev update doc-gen4 | |
| - name: Get cache | |
| run: ~/.elan/bin/lake -Kenv=dev exe cache get || true | |
| - name: Build project | |
| run: ~/.elan/bin/lake -Kenv=dev build BonnAnalysis | |
| # Cache the documentation for Mathlib to save rebuild time | |
| - 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 | |
| !.lake/build/doc/declarations/declaration-data-BonnAnalysis* | |
| key: MathlibDoc-${{ hashFiles('lake-manifest.json') }} | |
| restore-keys: | | |
| MathlibDoc- | |
| - name: Build documentation | |
| run: ~/.elan/bin/lake -Kenv=dev build BonnAnalysis:docs | |
| - name: Install Python | |
| uses: actions/setup-python@v4 | |
| with: | |
| python-version: '3.9' | |
| cache: 'pip' | |
| # Install required apt packages for blueprint | |
| - name: Install blueprint apt dependencies | |
| run: | | |
| sudo apt-get update -qq | |
| sudo apt-get install -y --no-install-recommends graphviz libgraphviz-dev pdf2svg dvisvgm texlive-latex-base texlive-latex-extra texlive-fonts-recommended texlive-fonts-extra texlive-xetex | |
| - name: Install blueprint dependencies | |
| run: | | |
| cd blueprint && pip install -r requirements.txt | |
| - name: Build blueprint and copy to `docs/blueprint` | |
| run: inv all | |
| - name: Remove lake files from documentation | |
| run: | | |
| find .lake/build/doc -name "*.trace" -delete | |
| find .lake/build/doc -name "*.hash" -delete | |
| - name: Copy documentation to `docs/docs` | |
| run: | | |
| sudo chown -R runner docs | |
| cp -r .lake/build/doc docs/docs | |
| - name: Bundle dependencies | |
| uses: ruby/setup-ruby@v1 | |
| with: | |
| working-directory: docs | |
| ruby-version: "3.0" | |
| bundler-cache: true | |
| - 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 |