-
Notifications
You must be signed in to change notification settings - Fork 3
209 lines (180 loc) · 7.1 KB
/
build.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
207
208
209
# This file is based on mathlib's `build.yml.in` but we don't use mathlib's `mk_build_yml.sh` so
# you can edit this file directly.
# In fact we took this from the LTE version, so credit is due to @bentoner
on:
push:
branches-ignore:
# ignore tmp branches used by bors
- 'staging.tmp*'
- 'trying.tmp*'
- 'staging*.tmp'
- 'nolints'
# do not build lean-x.y.z branch used by leanpkg
- 'lean-3.*'
# ignore staging branch used by bors, this is handled by bors.yml
- 'staging'
name: continuous integration
jobs:
# When you push to a branch, we cancel previous runs of jobs in this file on that branch.
cancel:
name: 'Cancel previous runs on branch'
# if: github.ref != 'refs/heads/master'
runs-on: ubuntu-latest
# timeout-minutes: 3
steps:
- uses: styfle/cancel-workflow-action@0.9.0
with:
all_but_latest: true
access_token: ${{ github.token }}
build:
name: Build flt-regular
runs-on: ubuntu-latest
env:
# number of commits to check for olean cache
GIT_HISTORY_DEPTH: 20
outputs:
artifact_name: ${{ steps.setup_precompiled.outputs.artifact_name }}
steps:
- uses: actions/checkout@v3
with:
fetch-depth: ${{ env.GIT_HISTORY_DEPTH }}
- name: install elan
run: |
set -o pipefail
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
~/.elan/bin/lean --version
echo "$HOME/.elan/bin" >> $GITHUB_PATH
echo "short_lean_version=$(~/.elan/bin/lean --run scripts/lean_version.lean)" >> $GITHUB_ENV
- name: install Python
if: ${{ ! 0 }}
uses: actions/setup-python@v1
with:
python-version: 3.8
- name: install mathlibtools
run: python -m pip install --upgrade pip mathlibtools
- name: leanpkg configure
run: leanpkg configure
- name: get mathlib cache
run: leanproject get-mathlib-cache || true
- name: try to find olean cache
continue-on-error: true
run: ./scripts/fetch_olean_cache.sh
- name: leanpkg build
id: build
run: |
echo "::set-output name=started::true"
lean --json --make src | python scripts/detect_errors.py
lean --json --make src | python scripts/detect_errors.py
- name: push release to azure
if: always() && (github.repository == 'leanprover-community/flt-regular') && steps.build.outputs.started == 'true' && github.ref == 'refs/heads/master'
continue-on-error: true
run: |
archive_name="$(git rev-parse HEAD).tar.xz"
find src/ -name "*.olean" -o -name ".noisy_files" | tar cJf "$archive_name" -T -
azcopy copy "$archive_name" "https://oleanstorage.blob.core.windows.net/mathlib/flt-regular/$archive_name${{ secrets.AZURE_SAS_TOKEN }}" --block-size-mb 99 --overwrite false
- name: setup precompiled zip file
if: always() && steps.build.outputs.started == 'true'
id: setup_precompiled
run: |
touch workspace.tar
tar -cf workspace.tar --exclude=*.tar* .
git_hash="$(git log -1 --pretty=format:%h)"
echo "::set-output name=artifact_name::precompiled-flt-regular-$short_lean_version-$git_hash"
- name: upload precompiled flt-regular zip file
if: always() && steps.build.outputs.started == 'true'
uses: actions/upload-artifact@v2
with:
name: ${{ steps.setup_precompiled.outputs.artifact_name }}
path: workspace.tar
lint:
name: Lint flt-regular
runs-on: ubuntu-latest
needs: build
steps:
- name: retrieve build
uses: actions/download-artifact@v2
with:
name: ${{ needs.build.outputs.artifact_name }}
- name: untar build
run: tar -xf workspace.tar
- name: install elan
run: |
set -o pipefail
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
~/.elan/bin/lean --version
echo "$HOME/.elan/bin" >> $GITHUB_PATH
- name: lint
# Uncomment the following line to make the build succeed even if there are linting errors
# continue-on-error: true
run: |
./scripts/mk_all.sh
lean --run scripts/lint_project.lean
stats:
name: Stats for flt-regular
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v3
- name: install ripgrep
run: sudo apt install -y ripgrep
- name: count lines in src
run: |
shopt -s globstar
wc -l src/**/*.lean
- name: count sorries
run: |
rg --count-matches sorry src | awk -F ':' 'BEGIN {sum = 0} {sum += $2} {print $2 " " $1} END {print sum " total"}'
update-branch:
# This should be configured so that failure (which is likely whenever there is a force-push to
# master) doesn't cause the rest of the build to fail, e.g., by putting it in its own job.
name: Update lean-3.3x branch
runs-on: ubuntu-latest
needs: build
steps:
- uses: actions/checkout@v2
with:
fetch-depth: 0
- name: update lean-3.3x branch
if: github.ref == 'refs/heads/master'
uses: leanprover-contrib/update-versions-action@master
deploy:
runs-on: ubuntu-latest
needs: build
steps:
- name: Checkout
uses: actions/checkout@v3
with:
submodules: true
- name: Setup Python
uses: actions/setup-python@v2
with:
python-version: '3.8'
- name: Install elan
run: |
set -o pipefail
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -v -y
sudo ln -s $HOME/.elan/bin/* /usr/local/bin;
- name: Install python Lean dependencies
run: python -m pip install --upgrade pip requests markdown2 toml mathlibtools toposort invoke
- name: Link and fetch mathlib
run: |
leanproject get-m
inv decls
# name: Install Leanblueprint and generate web in tex env
# uses: xu-cheng/texlive-action/full@v1
# with:
# run: |
# apk update
# apk add --update make py3-pip git
# git config --global --add safe.directory $GITHUB_WORKSPACE
# git config --global --add safe.directory `pwd`
# python3 -m pip install --upgrade pip requests wheel
# apk add pkgconfig graphviz graphviz-dev gcc musl-dev && \
# python3 -m pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/"
# python3 -m pip install invoke git+https://github.com/plastex/plastex.git git+https://github.com/PatrickMassot/leanblueprint.git
# inv pdf; cp print/blueprint.bbl doc/web.bbl; inv qweb
# cp print/blueprint.pdf web/
# name: deploy
# uses: peaceiris/actions-gh-pages@v3
# with:
# github_token: ${{ secrets.github_token }}
# publish_dir: ./web