danabra.mov
My solutions to Tao's Analysis I, formalized in Lean
1name: Build book
2
3on:
4 push:
5 branches:
6 - main
7 - solutions
8 pull_request:
9 workflow_dispatch:
10
11concurrency:
12 group: ${{ github.ref }} # Group runs by the ref (branch or PR)
13 cancel-in-progress: true # Cancel any ongoing runs in the same group
14
15defaults:
16 run:
17 working-directory: ./book
18
19jobs:
20 build:
21 runs-on: ubuntu-latest
22 steps:
23 - uses: actions/checkout@v4
24 - name: Install elan
25 run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
26 - name: Restore cache if available
27 uses: actions/cache/restore@v4
28 with:
29 path: |
30 ./analysis/.lake
31 ./book/.lake
32 key: lake-${{ runner.os }}-${{ runner.arch}}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
33 restore-keys: lake-${{ runner.os }}-${{ runner.arch}}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
34 # Getting the mathlib cache is only useful when mathlib gets updated, but will save a lot of time in that case.
35 - name: Get Mathlib cache
36 run: ~/.elan/bin/lake exe cache get || true
37 working-directory: ./analysis
38 - name: Build doc-gen
39 run: ~/.elan/bin/lake -R -Kenv=dev build Analysis:docs
40 working-directory: ./analysis
41 - name: Build metadata of project
42 run: ~/.elan/bin/lake build
43 working-directory: ./analysis
44 - name: Build book
45 run: |
46 ~/.elan/bin/lake exe analysis-book
47 - name: Copy docs to analysis-book
48 run: |
49 cp -r ../analysis/.lake/build/doc _site/docs
50 - name: Remove unnecessary lake files from documentation in `_site/docs`
51 run: |
52 find _site/docs -name "*.trace" -delete
53 find _site/docs -name "*.hash" -delete
54 - name: Save cache
55 uses: actions/cache/save@v4
56 with:
57 path: |
58 ./analysis/.lake
59 ./book/.lake
60 key: lake-${{ runner.os }}-${{ runner.arch}}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
61 - name: Upload website
62 uses: actions/upload-pages-artifact@v3
63 with:
64 path: './book/_site'
65 deploy:
66 # Add a dependency to the build job
67 needs: build
68
69 # Grant GITHUB_TOKEN the permissions required to make a Pages deployment
70 permissions:
71 pages: write # to deploy to Pages
72 id-token: write # to verify the deployment originates from an appropriate source
73
74 # Deploy to the github-pages environment
75 environment:
76 name: github-pages
77 url: ${{ steps.deployment.outputs.page_url }}
78
79 # Specify runner + deployment step
80 runs-on: ubuntu-latest
81 if: github.ref == 'refs/heads/main'
82 steps:
83 - name: Deploy to GitHub Pages
84 id: deployment
85 uses: actions/deploy-pages@v4