Conversation
This PR reduces allocation and copying overhead for bignum arithmetic and conversions by transferring temporary result storage into Lean objects. Reuse the existing GMP and built-in bignum move constructors while preserving copying lvalue calls, object layout, small-value normalization, and mimalloc header initialization. Add exact extern/reference comparisons, retained-input and retained-result tests, direct copy/move ownership checks, and an isolated runtime benchmark with allocation, retained-storage, and peak-storage measurements.
This PR bounds spare limb capacity retained by move-aware bignum allocation. Copy temporary results whose capacity exceeds twice the used limb count. Add independent arithmetic and capacity regression checks, align native test compilation with the runtime, and document guarded allocation benchmarks.
Collaborator
Author
|
!bench |
|
Benchmark results for 344f681 against dc34e5f are in. There are significant results. @kim-em
Large changes (1✅)
Medium changes (1✅)
Small changes (2✅, 1🟥)
|
This PR summarizes representative timings, the capacity policy, and benchmark invocation.
This PR keeps representative Int and Nat heap-result and heap-to-scalar checks, with a concise test description.
This PR describes the Int and Nat bignum results and heap-to-scalar normalization checked by the extern tests.
Use the test environment’s CXX and query leanc for public runtime flags, preserving sanitizer instrumentation without using the bundled C-only compiler setup.
Member
|
See also #14978. |
github-actions
Bot
added
the
toolchain-available
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
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 reduces allocation and copying overhead for bignum arithmetic and conversions.
Move owned temporary limb storage into Lean objects, falling back to copying when capacity exceeds twice the used limb count. Preserve copying lvalue calls, object layout, small-value normalization, and mimalloc header initialization. Add extern comparisons, compiled-caller tests, and a runtime benchmark documenting timings, allocations, and retained storage.
This change is independent of #15160, which retains the existing allocator.
🤖 prepared with codex