-
Notifications
You must be signed in to change notification settings - Fork 715
fix: use general allocator for closures #10982
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Contributor
Author
|
!radar |
|
Benchmark results for 167c9c9 against 3a42ee0 are in! @hargoniX |
3 tasks
Contributor
Author
|
No instruction regression in sight! Let's go for it. |
Collaborator
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
wkrozowski
pushed a commit
to wkrozowski/lean4
that referenced
this pull request
Oct 27, 2025
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 leanprover#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: leanprover#10979
github-merge-queue bot
pushed a commit
that referenced
this pull request
Nov 17, 2025
This PR fixes fallout of the closure allocator changes in #10982. As far as we know this bug only meaningfully manifests in non default build configurations without mimalloc such as: `cmake --preset release -DUSE_MIMALLOC=OFF` The issue is that I forgot to update the deallocation functions for closures. However, this only seems to matter if we disable mimalloc which is why this slipped through testing.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Labels
changelog-compiler
Compiler, runtime, and FFI
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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:
The generated code at fault here looks as follows:
With the crash happening in
lean_alloc_closurewhere we unconditionally invoke the small allocatorwhich 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