Task #241 (#282) #96
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
| name: Compile blueprint | |
| on: | |
| push: | |
| branches: | |
| - main | |
| paths: | |
| - '**/*.lean' | |
| - '**/blueprint.yml' | |
| - 'blueprint/**' | |
| - 'docs/**' | |
| - 'lean-toolchain' | |
| - 'lakefile.toml' | |
| - 'lake-manifest.json' | |
| pull_request: | |
| branches: | |
| - main | |
| paths: | |
| - '**/*.lean' | |
| - '**/blueprint.yml' | |
| - 'blueprint/**' | |
| - 'docs/**' | |
| - 'lean-toolchain' | |
| - 'lakefile.toml' | |
| - 'lake-manifest.json' | |
| workflow_dispatch: # Allow manual triggering of the workflow from the GitHub Actions interface | |
| # Cancel previous runs if a new commit is pushed to the same PR or branch | |
| concurrency: | |
| group: ${{ github.ref }} # Group runs by the ref (branch or PR) | |
| cancel-in-progress: true # Cancel any ongoing runs in the same group | |
| # Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages and modify PR labels | |
| permissions: | |
| contents: read # Read access to repository contents | |
| pages: write # Write access to GitHub Pages | |
| id-token: write # Write access to ID tokens | |
| issues: write # Write access to issues | |
| pull-requests: write # Write access to pull requests | |
| 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@v4 | |
| with: | |
| fetch-depth: 0 # Fetch all history for all branches and tags | |
| - 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 | |
| - name: Build project | |
| run: ~/.elan/bin/lake build FLT | |
| - name: Cache Mathlib docs | |
| uses: actions/cache@v4 | |
| with: | |
| path: | | |
| .lake/build/doc | |
| key: MathlibDoc-${{ hashFiles('lake-manifest.json') }} | |
| restore-keys: | | |
| MathlibDoc- | |
| - name: Build project API documentation | |
| run: ~/.elan/bin/lake -R -Kenv=dev build FLT:docs | |
| - name: Check for `docs` folder # this is meant to detect a Jekyll-based website | |
| id: check_docs | |
| run: | | |
| if [ -d docs ]; then | |
| echo "The 'docs' folder exists in the repository." | |
| echo "DOCS_EXISTS=true" >> $GITHUB_ENV | |
| else | |
| echo "The 'docs' folder does not exist in the repository." | |
| echo "DOCS_EXISTS=false" >> $GITHUB_ENV | |
| fi | |
| - name: Build blueprint and copy to `docs/blueprint` | |
| uses: xu-cheng/texlive-action@v2 | |
| with: | |
| docker_image: ghcr.io/xu-cheng/texlive-full:20231201 | |
| run: | | |
| # Install necessary dependencies and build the blueprint | |
| apk update | |
| apk add --update make py3-pip git pkgconfig graphviz graphviz-dev gcc musl-dev | |
| git config --global --add safe.directory $GITHUB_WORKSPACE | |
| git config --global --add safe.directory `pwd` | |
| python3 -m venv env | |
| source env/bin/activate | |
| pip install --upgrade pip requests wheel | |
| pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/" | |
| pip install leanblueprint | |
| leanblueprint pdf | |
| mkdir -p docs | |
| cp blueprint/print/print.pdf docs/blueprint.pdf | |
| leanblueprint web | |
| cp -r blueprint/web docs/blueprint | |
| - name: Check declarations mentioned in the blueprint exist in Lean code | |
| run: | | |
| ~/.elan/bin/lake exe checkdecls blueprint/lean_decls | |
| - name: Copy API documentation to `docs/docs` | |
| run: cp -r .lake/build/doc docs/docs | |
| - name: Bundle dependencies | |
| if: github.event_name == 'push' | |
| uses: ruby/setup-ruby@v1 | |
| with: | |
| working-directory: docs | |
| ruby-version: "3.0" # Specify Ruby version | |
| bundler-cache: true # Enable caching for bundler | |
| - name: Build website using Jekyll | |
| if: github.event_name == 'push' && env.DOCS_EXISTS == 'true' | |
| working-directory: docs | |
| run: JEKYLL_ENV=production bundle exec jekyll build # Note this will also copy the blueprint and API doc into docs/_site | |
| - name: "Upload website (API documentation, blueprint and any home page)" | |
| if: github.event_name == 'push' | |
| uses: actions/upload-pages-artifact@v3 | |
| with: | |
| path: ${{ env.DOCS_EXISTS == 'true' && 'docs/_site' || 'docs/' }} | |
| - name: Deploy to GitHub Pages | |
| if: github.event_name == 'push' | |
| id: deployment | |
| uses: actions/deploy-pages@v4 |