Skip to content

Commit edbb84d

Browse files
Khatydeu
Kha
and
tydeu
authored
chore: CI: USE_LAKE secondary build job (leanprover#7505)
As preparation for the module system, and in hopes it will be faster than and replace the Nix CI. Secondary build jobs do not block merging. Also makes macOS aarch64 a secondary build job on the PR level, where it is the current bottleneck. --------- Co-authored-by: Mac Malone <[email protected]>
1 parent 756fd66 commit edbb84d

File tree

5 files changed

+306
-211
lines changed

5 files changed

+306
-211
lines changed

‎.github/workflows/build-template.yml

Lines changed: 234 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,234 @@
1+
name: build-template
2+
on:
3+
workflow_call:
4+
inputs:
5+
check-level:
6+
type: string
7+
required: true
8+
config:
9+
type: string
10+
required: true
11+
nightly:
12+
type: string
13+
required: true
14+
LEAN_VERSION_MAJOR:
15+
type: string
16+
required: true
17+
LEAN_VERSION_MINOR:
18+
type: string
19+
required: true
20+
LEAN_VERSION_PATCH:
21+
type: string
22+
required: true
23+
LEAN_SPECIAL_VERSION_DESC:
24+
type: string
25+
required: true
26+
RELEASE_TAG:
27+
type: string
28+
required: true
29+
30+
jobs:
31+
build:
32+
if: github.event_name != 'schedule' || github.repository == 'leanprover/lean4'
33+
strategy:
34+
matrix:
35+
include: ${{fromJson(inputs.config)}}
36+
# complete all jobs
37+
fail-fast: false
38+
runs-on: ${{ matrix.os }}
39+
defaults:
40+
run:
41+
shell: ${{ matrix.shell || 'nix develop -c bash -euxo pipefail {0}' }}
42+
name: ${{ matrix.name }}
43+
env:
44+
# must be inside workspace
45+
CCACHE_DIR: ${{ github.workspace }}/.ccache
46+
CCACHE_COMPRESS: true
47+
# current cache limit
48+
CCACHE_MAXSIZE: 200M
49+
# squelch error message about missing nixpkgs channel
50+
NIX_BUILD_SHELL: bash
51+
LSAN_OPTIONS: max_leaks=10
52+
# somehow MinGW clang64 (or cmake?) defaults to `g++` even though it doesn't exist
53+
CXX: c++
54+
MACOSX_DEPLOYMENT_TARGET: 10.15
55+
steps:
56+
- name: Install Nix
57+
uses: DeterminateSystems/nix-installer-action@main
58+
if: runner.os == 'Linux' && !matrix.cmultilib
59+
- name: Install MSYS2
60+
uses: msys2/setup-msys2@v2
61+
with:
62+
msystem: clang64
63+
# `:` means do not prefix with msystem
64+
pacboy: "make: python: cmake clang ccache gmp libuv git: zip: unzip: diffutils: binutils: tree: zstd tar:"
65+
if: runner.os == 'Windows'
66+
- name: Install Brew Packages
67+
run: |
68+
brew install ccache tree zstd coreutils gmp libuv
69+
if: runner.os == 'macOS'
70+
- name: Checkout
71+
uses: actions/checkout@v4
72+
with:
73+
# the default is to use a virtual merge commit between the PR and master: just use the PR
74+
ref: ${{ github.event.pull_request.head.sha }}
75+
# Do check out some CI-relevant files from virtual merge commit to accommodate CI changes on
76+
# master (as the workflow files themselves are always taken from the merge)
77+
# (needs to be after "Install *" to use the right shell)
78+
- name: CI Merge Checkout
79+
run: |
80+
git fetch --depth=1 origin ${{ github.sha }}
81+
git checkout FETCH_HEAD flake.nix flake.lock
82+
if: github.event_name == 'pull_request'
83+
# (needs to be after "Checkout" so files don't get overridden)
84+
- name: Setup emsdk
85+
uses: mymindstorm/setup-emsdk@v14
86+
with:
87+
version: 3.1.44
88+
actions-cache-folder: emsdk
89+
if: matrix.wasm
90+
- name: Install 32bit c libs
91+
run: |
92+
sudo dpkg --add-architecture i386
93+
sudo apt-get update
94+
sudo apt-get install -y gcc-multilib g++-multilib ccache libuv1-dev:i386 pkgconf:i386
95+
if: matrix.cmultilib
96+
- name: Cache
97+
if: matrix.name != 'Linux Lake'
98+
uses: actions/cache@v4
99+
with:
100+
path: |
101+
.ccache
102+
key: ${{ matrix.name }}-build-v3-${{ github.event.pull_request.head.sha }}
103+
# fall back to (latest) previous cache
104+
restore-keys: |
105+
${{ matrix.name }}-build-v3
106+
save-always: true
107+
- name: Cache
108+
if: matrix.name == 'Linux Lake'
109+
uses: actions/cache@v4
110+
with:
111+
path: |
112+
.ccache
113+
build/stage1/**/*.trace
114+
build/stage1/**/*.olean
115+
build/stage1/**/*.ilean
116+
build/stage1/**/*.c
117+
build/stage1/**/*.c.o*
118+
key: ${{ matrix.name }}-build-v3-${{ github.event.pull_request.head.sha }}
119+
# fall back to (latest) previous cache
120+
restore-keys: |
121+
${{ matrix.name }}-build-v3
122+
save-always: true
123+
# open nix-shell once for initial setup
124+
- name: Setup
125+
run: |
126+
ccache --zero-stats
127+
if: runner.os == 'Linux'
128+
- name: Set up NPROC
129+
run: |
130+
echo "NPROC=$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4)" >> $GITHUB_ENV
131+
- name: Build
132+
run: |
133+
[ -d build ] || mkdir build
134+
cd build
135+
# arguments passed to `cmake`
136+
# this also enables githash embedding into stage 1 library
137+
OPTIONS=(-DCHECK_OLEAN_VERSION=ON)
138+
OPTIONS+=(-DLEAN_EXTRA_MAKE_OPTS=-DwarningAsError=true)
139+
if [[ -n '${{ matrix.cross_target }}' ]]; then
140+
# used by `prepare-llvm`
141+
export EXTRA_FLAGS=--target=${{ matrix.cross_target }}
142+
OPTIONS+=(-DLEAN_PLATFORM_TARGET=${{ matrix.cross_target }})
143+
fi
144+
if [[ -n '${{ matrix.prepare-llvm }}' ]]; then
145+
wget -q ${{ matrix.llvm-url }}
146+
PREPARE="$(${{ matrix.prepare-llvm }})"
147+
eval "OPTIONS+=($PREPARE)"
148+
fi
149+
if [[ -n '${{ matrix.release }}' && -n '${{ inputs.nightly }}' ]]; then
150+
OPTIONS+=(-DLEAN_SPECIAL_VERSION_DESC=${{ inputs.nightly }})
151+
fi
152+
if [[ -n '${{ matrix.release }}' && -n '${{ inputs.RELEASE_TAG }}' ]]; then
153+
OPTIONS+=(-DLEAN_VERSION_MAJOR=${{ inputs.LEAN_VERSION_MAJOR }})
154+
OPTIONS+=(-DLEAN_VERSION_MINOR=${{ inputs.LEAN_VERSION_MINOR }})
155+
OPTIONS+=(-DLEAN_VERSION_PATCH=${{ inputs.LEAN_VERSION_PATCH }})
156+
OPTIONS+=(-DLEAN_VERSION_IS_RELEASE=1)
157+
OPTIONS+=(-DLEAN_SPECIAL_VERSION_DESC=${{ inputs.LEAN_SPECIAL_VERSION_DESC }})
158+
fi
159+
# contortion to support empty OPTIONS with old macOS bash
160+
cmake .. --preset ${{ matrix.CMAKE_PRESET || 'release' }} -B . ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/..
161+
time make -j$NPROC
162+
- name: Install
163+
run: |
164+
make -C build install
165+
- name: Check Binaries
166+
run: ${{ matrix.binary-check }} lean-*/bin/* || true
167+
- name: Count binary symbols
168+
run: |
169+
for f in lean-*/bin/*; do
170+
echo "$f: $(nm $f | grep " T " | wc -l) exported symbols"
171+
done
172+
if: matrix.name == 'Windows'
173+
- name: List Install Tree
174+
run: |
175+
# omit contents of Init/, ...
176+
tree --du -h lean-*-* | grep -E ' (Init|Lean|Lake|LICENSE|[a-z])'
177+
- name: Pack
178+
run: |
179+
dir=$(echo lean-*-*)
180+
mkdir pack
181+
# high-compression tar.zst + zip for release, fast tar.zst otherwise
182+
if [[ '${{ startsWith(github.ref, 'refs/tags/') && matrix.release }}' == true || -n '${{ inputs.nightly }}' || -n '${{ inputs.RELEASE_TAG }}' ]]; then
183+
${{ matrix.tar || 'tar' }} cf - $dir | zstd -T0 --no-progress -19 -o pack/$dir.tar.zst
184+
zip -rq pack/$dir.zip $dir
185+
else
186+
${{ matrix.tar || 'tar' }} cf - $dir | zstd -T0 --no-progress -o pack/$dir.tar.zst
187+
fi
188+
- uses: actions/upload-artifact@v4
189+
if: matrix.release
190+
with:
191+
name: build-${{ matrix.name }}
192+
path: pack/*
193+
- name: Lean stats
194+
run: |
195+
build/stage1/bin/lean --stats src/Lean.lean
196+
if: ${{ !matrix.cross }}
197+
- name: Test
198+
id: test
199+
run: |
200+
time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/stage1 -j$NPROC --output-junit test-results.xml ${{ matrix.CTEST_OPTIONS }}
201+
if: (matrix.wasm || !matrix.cross) && inputs.check-level >= 1
202+
- name: Test Summary
203+
uses: test-summary/action@v2
204+
with:
205+
paths: build/stage1/test-results.xml
206+
# prefix `if` above with `always` so it's run even if tests failed
207+
if: always() && steps.test.conclusion != 'skipped'
208+
- name: Check Test Binary
209+
run: ${{ matrix.binary-check }} tests/compiler/534.lean.out
210+
if: (!matrix.cross) && steps.test.conclusion != 'skipped'
211+
- name: Build Stage 2
212+
run: |
213+
make -C build -j$NPROC stage2
214+
if: matrix.test-speedcenter
215+
- name: Check Stage 3
216+
run: |
217+
make -C build -j$NPROC check-stage3
218+
if: matrix.test-speedcenter
219+
- name: Test Speedcenter Benchmarks
220+
run: |
221+
# Necessary for some timing metrics but does not work on Namespace runners
222+
# and we just want to test that the benchmarks run at all here
223+
#echo -1 | sudo tee /proc/sys/kernel/perf_event_paranoid
224+
export BUILD=$PWD/build PATH=$PWD/build/stage1/bin:$PATH
225+
cd tests/bench
226+
nix shell .#temci -c temci exec --config speedcenter.yaml --included_blocks fast --runs 1
227+
if: matrix.test-speedcenter
228+
- name: Check rebootstrap
229+
run: |
230+
# clean rebuild in case of Makefile changes
231+
make -C build update-stage0 && rm -rf build/stage* && make -C build -j$NPROC
232+
if: matrix.name == 'Linux' && inputs.check-level >= 1
233+
- name: CCache stats
234+
run: ccache -s

0 commit comments

Comments
 (0)