Skip to content

Commit a3ddb16

Browse files
KhaKha
committed
restore CI, always run fsanitize on large on all tests
1 parent adb9c2d commit a3ddb16

File tree

1 file changed

+145
-9
lines changed

1 file changed

+145
-9
lines changed

‎.github/workflows/ci.yml‎

Lines changed: 145 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -153,7 +153,7 @@ jobs:
153153
# 0: PRs without special label
154154
# 1: PRs with `merge-ci` label, merge queue checks, master commits
155155
# 2: nightlies
156-
# 2: PRs with `release-ci` label, full releases
156+
# 3: PRs with `release-ci` label, full releases
157157
- name: Set check level
158158
id: set-level
159159
# We do not use github.event.pull_request.labels.*.name here because
@@ -199,18 +199,154 @@ jobs:
199199
const isPr = "${{ github.event_name }}" == "pull_request";
200200
const isPushToMaster = "${{ github.event_name }}" == "push" && "${{ github.ref_name }}" == "master";
201201
let matrix = [
202+
/* TODO: to be updated to new LLVM
202203
{
203-
"name": "Linux fsanitize",
204+
"name": "Linux LLVM",
205+
"os": "ubuntu-latest",
206+
"release": false,
207+
"enabled": level >= 2,
208+
"test": true,
209+
"shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
210+
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst",
211+
"prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
212+
"binary-check": "ldd -v",
213+
// foreign code may be linked against more recent glibc
214+
// reverse-ffi needs to be updated to link to LLVM libraries
215+
"CTEST_OPTIONS": "-E 'foreign|leanlaketest_reverse-ffi'",
216+
"CMAKE_OPTIONS": "-DLLVM=ON -DLLVM_CONFIG=${GITHUB_WORKSPACE}/build/llvm-host/bin/llvm-config"
217+
}, */
218+
{
219+
// portable release build: use channel with older glibc (2.26)
220+
"name": "Linux release",
221+
// usually not a bottleneck so make exclusive to `fast-ci`
204222
"os": large && fast ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
205-
"enabled": true, //level >= 2,
206-
// do not have nightly release wait for this
207-
//"secondary": level <= 2,
223+
"release": true,
224+
// Special handling for release jobs. We want:
225+
// 1. To run it in PRs so developers get PR toolchains (so secondary without tests is sufficient)
226+
// 2. To skip it in merge queues as it takes longer than the
227+
// Linux lake build and adds little value in the merge queue
228+
// 3. To run it in release (obviously)
229+
// 4. To run it for pushes to master so that pushes to master have a Linux toolchain
230+
// available as an artifact for Grove to use.
231+
"enabled": isPr || level != 1 || isPushToMaster,
232+
"test": level >= 1,
233+
"secondary": level == 0,
234+
"shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
235+
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst",
236+
"prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
237+
"binary-check": "ldd -v",
238+
// foreign code may be linked against more recent glibc
239+
"CTEST_OPTIONS": "-E 'foreign'",
240+
},
241+
{
242+
"name": "Linux Lake",
243+
"os": large ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
244+
"enabled": true,
245+
"check-rebootstrap": level >= 1,
246+
"check-stage3": level >= 2,
247+
"test": true,
248+
// NOTE: `test-speedcenter` currently seems to be broken on `ubuntu-latest`
249+
"test-speedcenter": large && level >= 2,
250+
// We are not warning-free yet on all platforms, start here
251+
"CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror",
252+
},
253+
{
254+
"name": "Linux Reldebug",
255+
"os": "ubuntu-latest",
256+
"enabled": level >= 2,
257+
"test": true,
258+
"CMAKE_PRESET": "reldebug",
259+
},
260+
{
261+
"name": "Linux fsanitize",
262+
// Always run on large if available, more reliable regarding timeouts
263+
"os": large ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
264+
"enabled": level >= 2,
208265
"test": true,
209266
// turn off custom allocator & symbolic functions to make LSAN do its magic
210-
"CMAKE_PRESET": "sanitize"
211-
// exclude seriously slow/problematic tests (laketests crash, async_base_functions timeouts)
212-
//"CTEST_OPTIONS": "-E '(interactive|pkg|lake|bench)/|treemap|StackOverflow|async_base_functions'"
213-
}
267+
"CMAKE_PRESET": "sanitize",
268+
// `StackOverflow*` correctly triggers ubsan
269+
// `reverse-ffi` fails to link in sanitizers
270+
"CTEST_OPTIONS": "-E 'StackOverflow|reverse-ffi'"
271+
},
272+
{
273+
"name": "macOS",
274+
"os": "macos-15-intel",
275+
"release": true,
276+
"test": false, // Tier 2 platform
277+
"enabled": level >= 2,
278+
"shell": "bash -euxo pipefail {0}",
279+
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-apple-darwin.tar.zst",
280+
"prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
281+
"binary-check": "otool -L",
282+
"tar": "gtar", // https://github.com/actions/runner-images/issues/2619
283+
"CTEST_OPTIONS": "-E 'leanlaketest_hello'", // started failing from unpack
284+
},
285+
{
286+
"name": "macOS aarch64",
287+
// standard GH runner only comes with 7GB so use large runner if possible when running tests
288+
"os": large && (fast || level >= 1) ? "nscloud-macos-sequoia-arm64-6x14" : "macos-15",
289+
"CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-darwin_aarch64",
290+
"release": true,
291+
"shell": "bash -euxo pipefail {0}",
292+
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-aarch64-apple-darwin.tar.zst",
293+
"prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
294+
"binary-check": "otool -L",
295+
"tar": "gtar", // https://github.com/actions/runner-images/issues/2619
296+
// See "Linux release" for release job levels; Grove is not a concern here
297+
"enabled": isPr || level != 1,
298+
"test": level >= 1,
299+
"secondary": level == 0,
300+
},
301+
{
302+
"name": "Windows",
303+
"os": large && (fast || level >= 2) ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
304+
"release": true,
305+
"enabled": level >= 2,
306+
"test": true,
307+
"shell": "msys2 {0}",
308+
"CMAKE_OPTIONS": "-G \"Unix Makefiles\"",
309+
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
310+
"prepare-llvm": "../script/prepare-llvm-mingw.sh lean-llvm*",
311+
"binary-check": "ldd",
312+
},
313+
{
314+
"name": "Linux aarch64",
315+
"os": "nscloud-ubuntu-22.04-arm64-4x16",
316+
"CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-linux_aarch64",
317+
"release": true,
318+
"enabled": level >= 2,
319+
"test": true,
320+
"shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}",
321+
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-aarch64-linux-gnu.tar.zst",
322+
"prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
323+
},
324+
// Started running out of memory building expensive modules, a 2GB heap is just not that much even before fragmentation
325+
//{
326+
// "name": "Linux 32bit",
327+
// "os": "ubuntu-latest",
328+
// // Use 32bit on stage0 and stage1 to keep oleans compatible
329+
// "CMAKE_OPTIONS": "-DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_MMAP=OFF -DUSE_GMP=OFF -DLEAN_EXTRA_CXX_FLAGS='-m32' -DLEANC_OPTS='-m32' -DMMAP=OFF -DLEAN_INSTALL_SUFFIX=-linux_x86 -DCMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DSTAGE0_CMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DPKG_CONFIG_EXECUTABLE=/usr/bin/i386-linux-gnu-pkg-config",
330+
// "cmultilib": true,
331+
// "release": true,
332+
// "enabled": level >= 2,
333+
// "cross": true,
334+
// "shell": "bash -euxo pipefail {0}"
335+
//}
336+
// {
337+
// "name": "Web Assembly",
338+
// "os": "ubuntu-latest",
339+
// // Build a native 32bit binary in stage0 and use it to compile the oleans and the wasm build
340+
// "CMAKE_OPTIONS": "-DCMAKE_C_COMPILER_WORKS=1 -DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_CMAKE_CXX_COMPILER=clang++ -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_EXECUTABLE_SUFFIX=\"\" -DUSE_GMP=OFF -DMMAP=OFF -DSTAGE0_MMAP=OFF -DCMAKE_AR=../emsdk/emsdk-main/upstream/emscripten/emar -DCMAKE_TOOLCHAIN_FILE=../emsdk/emsdk-main/upstream/emscripten/cmake/Modules/Platform/Emscripten.cmake -DLEAN_INSTALL_SUFFIX=-linux_wasm32 -DSTAGE0_CMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/",
341+
// "wasm": true,
342+
// "cmultilib": true,
343+
// "release": true,
344+
// "enabled": level >= 2,
345+
// "cross": true,
346+
// "shell": "bash -euxo pipefail {0}",
347+
// // Just a few selected tests because wasm is slow
348+
// "CTEST_OPTIONS": "-R \"leantest_1007\\.lean|leantest_Format\\.lean|leanruntest\\_1037.lean|leanruntest_ac_rfl\\.lean|leanruntest_tempfile.lean\\.|leanruntest_libuv\\.lean\""
349+
// }
214350
];
215351
for (const job of matrix) {
216352
if (job["prepare-llvm"]) {

0 commit comments

Comments
 (0)