lean4-htt/tests/compiler
Henrik Böving 334fa475b4
fix: use general allocator for closures (#10982)
This PR changes the closure allocator to use the general allocator
instead of the small object one.
This is because users may create closures with a gigantic amount of
closed variables which in turn
boost the size of the closure beyond the small object threshold.

This issue was uncovered by #10979. Detecting that the small object
threshold is at fault requires
building mimalloc in debug mode at which point it yields:
```
mimalloc: assertion failed: at "/home/henrik/lean4/build/debug/mimalloc/src/mimalloc/src/alloc.c":132, mi_heap_malloc_small_zero
  assertion: "size <= MI_SMALL_SIZE_MAX"
```
The generated code at fault here looks as follows:
```c
LEAN_EXPORT lean_object* l_initExec___at___00res_spec__0(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_2 = lean_alloc_closure((void*)(l_initializer_ext___at___00initExec___at___00res_spec__0_spec__0___lam__0___boxed), 3, 0);
x_3 = l_initExec___redArg___closed__0;
x_4 = l_initExec___redArg___closed__1;
x_5 = l_instMonadLiftNonDetT___closed__0;
x_6 = l_initExec___redArg___closed__2;
x_7 = l_initExec___at___00res_spec__0___closed__0;
lean_inc_ref(x_2);
x_8 = lean_alloc_closure((void*)(l_initExec___at___00res_spec__0___lam__29___boxed), 213, 212);
lean_closure_set(x_8, 0, x_3);
lean_closure_set(x_8, 1, x_2);
lean_closure_set(x_8, 2, x_4);
lean_closure_set(x_8, 3, x_3);
lean_closure_set(x_8, 4, x_4);
lean_closure_set(x_8, 5, x_3);
lean_closure_set(x_8, 6, x_4);
lean_closure_set(x_8, 7, x_3);
lean_closure_set(x_8, 8, x_4);
lean_closure_set(x_8, 9, x_3);
lean_closure_set(x_8, 10, x_4);
lean_closure_set(x_8, 11, x_3);
lean_closure_set(x_8, 12, x_4);
lean_closure_set(x_8, 13, x_3);
lean_closure_set(x_8, 14, x_4);
lean_closure_set(x_8, 15, x_5);
lean_closure_set(x_8, 16, x_6);
lean_closure_set(x_8, 17, x_5);
lean_closure_set(x_8, 18, x_5);
lean_closure_set(x_8, 19, x_5);
lean_closure_set(x_8, 20, x_5);
lean_closure_set(x_8, 21, x_5);
lean_closure_set(x_8, 22, x_5);
...
```
With the crash happening in `lean_alloc_closure` where we
unconditionally invoke the small allocator
which cannot cope with closures this large. Hopefully changing this to
the general purpose allocator
doesn't have too much of an impact on performance.

Closes: #10979
2025-10-27 10:16:59 +00:00
..
foreign chore: further split libleanshared on Windows to avoid symbol limit (#10136) 2025-08-26 16:01:57 +00:00
.gitignore chore: add .dSYM files (Mac debug symbols) to tests .gitignore files (#8771) 2025-06-13 15:27:46 +00:00
534.lean feat: cleanup of get and back functions on List/Array (#7059) 2025-02-17 01:43:45 +00:00
534.lean.expected.out
append.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
append.lean.expected.out chore(tests/compiler/append): add expected output 2019-02-09 20:02:26 +01:00
array.lean chore: rename Array.data to Array.toList 2024-09-10 15:24:23 +10:00
array.lean.expected.out fix: elim_array_cases 2021-01-04 16:10:49 -08:00
array_test.lean refactor: use Lists for Array reference implementation 2020-11-17 17:05:53 -08:00
array_test.lean.expected.out feat: add Subarray 2020-10-09 16:06:24 -07:00
array_test2.lean chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01:00
array_test2.lean.expected.out feat(library/init/data/array/basic): array helper functions 2019-04-28 10:10:24 -07:00
arrayMk.lean fix: Array.mk and Array.data externs 2020-12-13 11:10:01 -08:00
arrayMk.lean.expected.out fix: Array.mk and Array.data externs 2020-12-13 11:10:01 -08:00
bigctor.lean
bigctor.lean.expected.out
bytearray_bug.lean chore: remove >6 month old deprecations (#10446) 2025-09-22 12:47:11 +00:00
bytearray_bug.lean.expected.out
closure_bug1.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
closure_bug1.lean.expected.out
closure_bug2.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
closure_bug2.lean.expected.out test: news tests 2019-12-19 05:51:04 -08:00
closure_bug3.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
closure_bug3.lean.expected.out test: news tests 2019-12-19 05:51:04 -08:00
closure_bug4.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
closure_bug4.lean.expected.out
closure_bug5.lean
closure_bug5.lean.expected.out
closure_bug6.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
closure_bug6.lean.expected.out test: news tests 2019-12-19 05:51:04 -08:00
closure_bug7.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
closure_bug7.lean.expected.out
closure_bug8.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
closure_bug8.lean.expected.out
computedFieldsExtern.lean.no_interpreter feat: support extern computed fields 2022-07-11 12:26:53 -07:00
escape.lean chore: re-enable tests (#10923) 2025-10-23 08:38:57 +00:00
escape.lean.expected.out chore: re-enable tests (#10923) 2025-10-23 08:38:57 +00:00
expr.lean chore: re-enable tests (#10923) 2025-10-23 08:38:57 +00:00
expr.lean.expected.out chore: re-enable tests (#10923) 2025-10-23 08:38:57 +00:00
extractClosedMutualBlock.lean fix: do not extract closed terms containing constants being defined 2021-09-30 12:46:38 -07:00
extractClosedMutualBlock.lean.expected.out fix: do not extract closed terms containing constants being defined 2021-09-30 12:46:38 -07:00
float.lean fix: Inhabited Float produced a bogus run-time value (#6136) 2024-11-20 10:43:59 +00:00
float.lean.expected.out fix: Inhabited Float produced a bogus run-time value (#6136) 2024-11-20 10:43:59 +00:00
float_cases_bug.lean chore: HasToString => ToString 2020-10-27 16:11:48 -07:00
float_cases_bug.lean.expected.out fix(library/compiler/csimp): bug at float_cases_on 2019-08-05 13:23:27 -07:00
init.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
init.lean.expected.out
init.lean.no_interpreter
initUnboxed.lean fix: codegen initUnboxed correctly in LLVM backend (#2015) 2023-01-07 16:26:53 +01:00
initUnboxed.lean.expected.out fix: fixes #1998 2023-01-03 16:01:27 -08:00
initUnboxed.lean.no_interpreter fix: fixes #1998 2023-01-03 16:01:27 -08:00
large_closure_bug.lean fix: use general allocator for closures (#10982) 2025-10-27 10:16:59 +00:00
large_closure_bug.lean.expected.out fix: use general allocator for closures (#10982) 2025-10-27 10:16:59 +00:00
lazylist.lean feat: LLVM backend (#1837) 2022-12-30 12:45:30 +01:00
lazylist.lean.expected.out
lazylist.lean.no_interpreter
link_lake.lean fix: do not dllexport symbols in core static libraries (#3601) 2024-03-15 11:58:34 +00:00
link_lake.lean.expected.out fix: ship libLake.a 2023-07-21 09:19:19 +02:00
map_big.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
map_big.lean.expected.out
map_big.lean.no_interpreter
nat_shiftr.lean feat: optimize lean_nat_shiftr for scalars (#8268) 2025-05-11 01:39:59 +00:00
nat_shiftr.lean.expected.out feat: optimize lean_nat_shiftr for scalars (#8268) 2025-05-11 01:39:59 +00:00
overflow1.lean fix: panic in monadic polymorphic code 2021-09-28 17:46:19 -07:00
overflow1.lean.expected.out fix: panic in monadic polymorphic code 2021-09-28 17:46:19 -07:00
overflow2.lean fix: panic in monadic polymorphic code 2021-09-28 17:46:19 -07:00
overflow2.lean.expected.out fix: panic in monadic polymorphic code 2021-09-28 17:46:19 -07:00
overflow3.lean fix: panic in monadic polymorphic code 2021-09-28 17:46:19 -07:00
overflow3.lean.expected.out fix: panic in monadic polymorphic code 2021-09-28 17:46:19 -07:00
partial.lean refactor: make String.Pos opaque 2022-03-20 10:47:13 -07:00
partial.lean.expected.out feat(library/equations_compiler): add support for partial definitions 2019-03-27 11:09:32 -07:00
phashmap.lean chore: remove >6 month old deprecations (#10446) 2025-09-22 12:47:11 +00:00
phashmap.lean.expected.out chore: fix tests 2024-06-19 20:21:34 +02:00
phashmap2.lean chore: remove >6 month old deprecations (#9640) 2025-08-05 02:29:15 +00:00
phashmap2.lean.expected.out
phashmap3.lean chore: remove >6 month old deprecations (#10446) 2025-09-22 12:47:11 +00:00
phashmap3.lean.expected.out
print_error.lean chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01:00
print_error.lean.expected.out
print_error.lean.expected.ret
qsortBadLt.lean
qsortBadLt.lean.expected.out
rbmap_library.lean feat: Nat.(fold|foldRev|any|all)M? take a function which sees the upper bound (#6139) 2024-11-22 03:05:51 +00:00
rbmap_library.lean.expected.out
reusebug.lean chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01:00
reusebug.lean.expected.out
StackOverflow.lean chore: snake-case attributes (part 1) 2022-10-19 09:28:08 -07:00
StackOverflow.lean.expected.out feat: detect stack overflows on all platforms and threads 2020-05-04 11:11:11 +02:00
StackOverflow.lean.expected.ret feat: detect stack overflows on all platforms and threads 2020-05-04 11:11:11 +02:00
StackOverflow.lean.no_interpreter feat: detect stack overflows on all platforms and threads 2020-05-04 11:11:11 +02:00
StackOverflowTask.lean chore: snake-case attributes (part 1) 2022-10-19 09:28:08 -07:00
StackOverflowTask.lean.expected.out feat: detect stack overflows on all platforms and threads 2020-05-04 11:11:11 +02:00
StackOverflowTask.lean.expected.ret feat: detect stack overflows on all platforms and threads 2020-05-04 11:11:11 +02:00
StackOverflowTask.lean.no_interpreter feat: detect stack overflows on all platforms and threads 2020-05-04 11:11:11 +02:00
str.lean chore: re-enable tests (#10923) 2025-10-23 08:38:57 +00:00
str.lean.expected.out chore: re-enable tests (#10923) 2025-10-23 08:38:57 +00:00
strictAndOr.lean
strictAndOr.lean.expected.out
strictOrSimp.lean.expected.out
t1.lean
t1.lean.expected.out
t2.lean
t2.lean.expected.out
t4.lean
t4.lean.expected.out
test_single.sh feat: LLVM backend (#1837) 2022-12-30 12:45:30 +01:00
test_single_interpret.sh fix: unused variables linter review comments 2022-06-03 13:03:52 +02:00
thunk.lean
thunk.lean.expected.out
trie.lean chore: fix spelling mistakes in tests (#5439) 2024-09-24 03:22:53 +00:00
trie.lean.expected.out perf: Use flat ByteArrays in Trie (#2529) 2023-09-20 13:22:37 +02:00
trigraphs.lean test: C trigraph 2023-11-06 16:31:05 +01:00
trigraphs.lean.expected.out test: C trigraph 2023-11-06 16:31:05 +01:00
tuple.lean feat: allow trailing comma in tuples, lists, and tactics (#2643) 2023-11-17 13:31:41 +01:00
tuple.lean.expected.out feat: allow trailing comma in tuples, lists, and tactics (#2643) 2023-11-17 13:31:41 +01:00
typeFormerPolymorphism.lean fix: make lcAny-producing arrow types lower to tobj rather than obj (#9972) 2025-08-18 22:18:26 +00:00
typeFormerPolymorphism.lean.expected.out fix: make lcAny-producing arrow types lower to tobj rather than obj (#9972) 2025-08-18 22:18:26 +00:00
uint_fold.lean chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01:00
uint_fold.lean.expected.out
unreachable.lean feat: implement unreachable codegen for LLVM 2023-01-12 09:17:41 +01:00
unreachable.lean.expected.out feat: implement unreachable codegen for LLVM 2023-01-12 09:17:41 +01:00
uset.lean feat: Simp.Config.implicitDefEqProofs (#4595) 2024-11-29 22:29:27 +00:00
uset.lean.expected.out feat: implement uset for LLVM (#2025) 2023-01-09 12:25:37 +00:00
utf8Path.lean fix: Unicode path support for Lean Windows executables (#10133) 2025-08-27 11:28:55 +00:00
utf8Path.lean.expected.out fix: Unicode path support for Lean Windows executables (#10133) 2025-08-27 11:28:55 +00:00
wait_dedicated.lean feat: wait on dedicated tasks after main is finished (#7958) 2025-04-14 11:53:54 +00:00
wait_dedicated.lean.expected.out feat: wait on dedicated tasks after main is finished (#7958) 2025-04-14 11:53:54 +00:00