Craig's trick #1737
This file contains hidden or 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: CI | |
| on: | |
| push: | |
| branches: | |
| - "master" | |
| pull_request: | |
| merge_group: | |
| workflow_dispatch: | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| permissions: | |
| contents: read | |
| pages: write | |
| id-token: write | |
| jobs: | |
| build: | |
| name: Build project | |
| runs-on: ubuntu-latest | |
| steps: | |
| # We don't use https://github.com/leanprover/lean-action. | |
| # Because caching strategy is not suitable for our project. | |
| - uses: actions/checkout@v4 | |
| - name: Setup elan | |
| run: | | |
| curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none | |
| echo "$HOME/.elan/bin" >> "$GITHUB_PATH" | |
| - name: Setup graphviz | |
| uses: ts-graphviz/setup-graphviz@v2 | |
| - name: Setup typst | |
| uses: typst-community/setup-typst@v4 | |
| - name: Setup mdbook | |
| uses: baptiste0928/cargo-install@v3 | |
| with: | |
| crate: mdbook | |
| version: "0.4.51" | |
| - name: Setup mdbook-katex | |
| uses: baptiste0928/cargo-install@v3 | |
| with: | |
| crate: mdbook-katex | |
| version: "0.9.4" | |
| - name: Print tools version | |
| run: | | |
| lake --version | |
| dot -V | |
| typst --version | |
| mdbook --version | |
| mdbook-katex --version | |
| # Restore project cache | |
| - name: Restore cache | |
| id: cache-restore | |
| uses: actions/cache/restore@v4 | |
| with: | |
| path: .lake | |
| key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} | |
| restore-keys: | | |
| lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }} | |
| # Build project | |
| - name: Get Mathlib cache | |
| run: lake exe cache get | |
| - name: Build project | |
| run: lake build --keep-toolchain | |
| # Build import-graph | |
| - name: Generate import graph | |
| run: | | |
| lake exe graph ./import_graph.png | |
| lake exe graph ./import_graph.pdf | |
| lake exe graph ./import_graph.html | |
| - name: Copy import graph to pages | |
| run: | | |
| cp ./import_graph.png ./pages/src/assets | |
| cp ./import_graph.pdf ./pages/src/assets | |
| cp ./import_graph.html ./pages/src/assets | |
| - name: Generate Propositional Zoo | |
| run: | | |
| lake exe generate_propositional_zoo | |
| typst compile ./Zoo/propositional.typ ./pages/src/assets/propositional_zoo.png | |
| - name: Generate Modal Zoo | |
| run: | | |
| lake exe generate_modal_zoo | |
| typst compile ./Zoo/modal.typ ./pages/src/assets/modal_zoo.png | |
| - name: Generate Arith Zoo | |
| run: | | |
| lake exe generate_arith_zoo | |
| typst compile ./Zoo/arith.typ ./pages/src/assets/arith_zoo.png | |
| # Build doc | |
| - name: Build docs | |
| run: lake build Foundation:docs | |
| - name: Copy docs to pages | |
| run: cp -r .lake/build/doc ./pages/_output/doc | |
| # Save project cache | |
| - name: Save project cache | |
| id: cache-save | |
| uses: actions/cache/save@v4 | |
| with: | |
| path: .lake | |
| key: ${{ steps.cache-restore.outputs.cache-primary-key }} | |
| # Build book | |
| - name: Build book | |
| run: mdbook build | |
| working-directory: pages | |
| # Upload pages artifact | |
| - uses: actions/upload-pages-artifact@v3 | |
| with: | |
| path: pages/_output | |
| deploy: | |
| runs-on: ubuntu-latest | |
| needs: build | |
| if: github.ref == 'refs/heads/master' | |
| environment: | |
| name: github-pages | |
| url: ${{ steps.deployment.outputs.page_url }} | |
| steps: | |
| - id: deployment | |
| uses: actions/deploy-pages@v4 |