generated from pitmonticone/LeanProject
-
Notifications
You must be signed in to change notification settings - Fork 50
206 lines (179 loc) · 7.75 KB
/
blueprint.yml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
name: Compile blueprint
on:
push:
branches:
- main
paths:
- '**/*.lean'
- '**/blueprint.yml'
- 'blueprint/**'
- 'commentary/**'
- 'home_page/**'
- '**/generate_dashboard.py'
- '**/generate_equation_implication_js.py'
- '**/generate_graphiti_data.rb'
- 'lean-toolchain'
- 'lakefile.toml'
- 'lake-manifest.json'
pull_request:
branches:
- main
paths:
- '**/*.lean'
- '**/blueprint.yml'
- 'blueprint/**'
- 'commentary/**'
- 'home_page/**'
- '**/generate_dashboard.py'
- '**/generate_equation_implication_js.py'
- '**/generate_graphiti_data.rb'
- '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:
build_project:
runs-on: ubuntu-latest
name: Build project
steps:
- name: Add 'awaiting-CI' label
if: >
github.event_name == 'pull_request'
run: |
curl --request POST \
--url https://github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels \
--header 'authorization: Bearer ${{ secrets.PAT_TOKEN }}' \
--header 'Content-Type: application/json' \
--data '["awaiting-CI"]'
- 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: Cache build artifacts and Mathlib API docs
uses: actions/cache@v4
with:
path: |
.lake/build
!.lake/build/doc-data
!.lake/build/doc/declarations/declaration-data-equational_theories*
key: LakeBuild-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
restore-keys: LakeBuild-
- name: Build project
run: ~/.elan/bin/lake build equational_theories
- name: check environment with lean4checker
run: |
: Check Environment with lean4checker
chmod +x ./scripts/lean4_checker/run_lean4checker.sh
./scripts/lean4_checker/run_lean4checker.sh
shell: bash
- name: Build project API documentation
run: ~/.elan/bin/lake -R -Kenv=dev build equational_theories:docs
- name: Check for `home_page` folder
id: check_home_page
run: |
if [ -d home_page ]; then
echo "The 'home_page' folder exists in the repository."
echo "HOME_PAGE_EXISTS=true" >> $GITHUB_ENV
else
echo "The 'home_page' folder does not exist in the repository."
echo "HOME_PAGE_EXISTS=false" >> $GITHUB_ENV
fi
- name: Build blueprint and copy to `home_page/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 home_page
cp blueprint/print/print.pdf home_page/blueprint.pdf
leanblueprint web
cp -r blueprint/web home_page/blueprint
- name: Check declarations mentioned in the blueprint exist in Lean code
run: |
~/.elan/bin/lake exe checkdecls blueprint/lean_decls
- name: Check with lean4lean
run: |
python scripts/lean4lean_checker/main.py
- name: Copy API documentation to `home_page/docs`
run: cp -r .lake/build/doc home_page/docs
- name: Remove unnecessary lake files from documentation in `home_page/docs`
run: |
find home_page/docs -name "*.trace" -delete
find home_page/docs -name "*.hash" -delete
- name: Generate home_page/dashboard.md
run: |
pip install pillow
python scripts/generate_dashboard.py
- name: Generate home_page/implications/implications.js
run: |
~/.elan/bin/lake exe extract_implications outcomes > /tmp/out.json
pip install markdown
python scripts/generate_equation_implication_js.py /tmp/out.json
- name: Generate the Finite Magma Explorer website
run: |
mkdir -p home_page/fme
cp -r tools/fme/dist/* home_page/fme
~/.elan/bin/lake exe extract_implications unknowns > home_page/fme/unknowns.json
COMMIT_HASH=$(git rev-parse --short HEAD)
sed -i "s/UNKNOWN_VERSION/$COMMIT_HASH/g" home_page/fme/index.html
- name: Bundle dependencies
if: github.event_name == 'push'
uses: ruby/setup-ruby@v1
with:
working-directory: home_page
ruby-version: "3.0" # Specify Ruby version
bundler-cache: true # Enable caching for bundler
- name: Generate home_page/graphiti/graph.json
run: |
~/.elan/bin/lake exe extract_implications --json > /tmp/implications.json
~/.elan/bin/lake exe extract_implications unknowns > /tmp/unknowns.json
ruby scripts/generate_graphiti_data.rb /tmp/implications.json /tmp/unknowns.json data/duals.json > home_page/graphiti/graph.json
- name: Build website using Jekyll
if: github.event_name == 'push' && env.HOME_PAGE_EXISTS == 'true'
working-directory: home_page
run: JEKYLL_ENV=production bundle exec jekyll build # Note this will also copy the blueprint and API doc into home_page/_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.HOME_PAGE_EXISTS == 'true' && 'home_page/_site' || 'home_page/' }}
- name: Deploy to GitHub Pages
if: github.event_name == 'push'
id: deployment
uses: actions/deploy-pages@v4
# - name: Make sure the API documentation cache works
# run: mv home_page/docs .lake/build/doc
- name: Remove 'awaiting-CI' label
if: >
always() &&
github.event_name == 'pull_request'
run: |
curl --request DELETE \
--url https://github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels/awaiting-CI \
--header 'authorization: Bearer ${{ secrets.PAT_TOKEN }}' \
--header 'Content-Type: application/json'