max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: CI: build everything with Lake (#13721)

Browse source
This commit is contained in:
Sebastian Ullrich 2026-05-16 19:11:25 +02:00 • committed by GitHub
parent d64eaf4597
commit ef2dc0f66a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 0 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
.github/workflows/ci.yml vendored
View file

@ -421,12 +421,6 @@ jobs:
// "CTEST_OPTIONS": "-R \"leantest_1007\\.lean|leantest_Format\\.lean|leanruntest\\_1037.lean|leanruntest_ac_rfl\\.lean|leanruntest_tempfile.lean\\.|leanruntest_libuv\\.lean\""
// }
];
for (const job of matrix) {
if (job["prepare-llvm"]) {
// `USE_LAKE` is not compatible with `prepare-llvm` currently
job["CMAKE_OPTIONS"] = (job["CMAKE_OPTIONS"] ? job["CMAKE_OPTIONS"] + " " : "") + "-DUSE_LAKE=OFF";
}
}
if (lakeCi) {
for (const job of matrix) {
job["CMAKE_OPTIONS"] = (job["CMAKE_OPTIONS"] ? job["CMAKE_OPTIONS"] + " " : "") + "-DLAKE_CI=ON";