feat: unbox inductives in the compiler #11873
Open
+78,486
−46,278
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
Rob23oba
changed the title
github-actions
bot
added
the
release-ci
yes, I'm aware this is an ugly fix just you wait until I introduce the struct RC pass which must not happen before the interpreter runs the code (a compiled only pass!) anyways I hope there are no memory leaks
Contributor
Author
|
Great, seems to work! @hargoniX, could you !bench this? |
github-actions
bot
added
the
toolchain-available
Collaborator
|
Mathlib CI status (docs):
|
leanprover-bot
added a commit
to leanprover/reference-manual
that referenced
this pull request
Jan 2, 2026
Collaborator
|
Reference manual CI status:
|
leanprover-bot
added
the
breaks-manual
Contributor
Author
|
!bench |
|
Benchmark results for 7d9cc32 against 1ca4faa are in! @Rob23oba Runs (1🟥)
Large changes (1🟥)
Medium changes (21✅)
Small changes (2049✅, 26🟥)
|
Contributor
|
That's a nice first result. Though there does seem to be some (probabilistic?) segfault in the microbenchmarks here? I'm generally a little worried, given that most applications of I think there's also a couple of interesting open questions in the design space that are not obvious:
|
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Jan 6, 2026
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Jan 6, 2026
leanprover-bot
added a commit
to leanprover/reference-manual
that referenced
this pull request
Jan 6, 2026
Rob23oba
force-pushed
the
compiler-unbox-test
branch
from
e11f2d7 to
0e86c81
Compare
…lean4 into compiler-unbox-test
…piler-unbox-test
Rob23oba
force-pushed
the
compiler-unbox-test
branch
from
0e86c81 to
14717c3
Compare
Rob23oba
force-pushed
the
compiler-unbox-test
branch
from
14717c3 to
2634c96
Compare
Rob23oba
force-pushed
the
compiler-unbox-test
branch
from
2634c96 to
a9068e3
Compare
Rob23oba
force-pushed
the
compiler-unbox-test
branch
from
a9068e3 to
d1af1a8
Compare
Contributor
Author
|
!bench |
|
Benchmark results for 852e108 against 11e4e44 are in! @Rob23oba Large changes (74✅, 4🟥)Too many entries to display here. View the full report on radar instead. Medium changes (240✅, 2🟥)Too many entries to display here. View the full report on radar instead. Small changes (1847✅, 28🟥)Too many entries to display here. View the full report on radar instead. |
Rob23oba
force-pushed
the
compiler-unbox-test
branch
from
852e108 to
f2da84f
Compare
Contributor
Author
|
!bench mathlib |
|
Benchmark results for leanprover-community/mathlib4-nightly-testing@cf601f6 against leanprover-community/mathlib4-nightly-testing@c31e3a7 are in! @Rob23oba No significant changes detected. |
Contributor
Author
|
@Garmelon "No significant changes detected." feels weird considering almost every file has roughly -6% in instructions |
Contributor
|
Yeah, it's not great. Maybe I can re-use mathlib thresholds (based on historical data) for nightly-testing. More detailsRadar uses thresholds based on historical data, and nightly-testing's linearized history consists of all commits tagged If I use mathlib's thresholds, then I'll need to turn off (or at least scale by some factor) significance detection for the history, else most commits will turn out to be significant. |
Rob23oba
force-pushed
the
compiler-unbox-test
branch
from
f2da84f to
cad66e6
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
6 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 implements the
@[unbox]attribute: In compiled code, values from inductives tagged@[unbox]are stored asstructs on the stack rather than the heap.This takes a bit of different approach than previously outlined in the documentation, allowing unboxed structs to occur anywhere (including variables and parameters and not just return values). To make this work, the existing infrastructure for boxing/unboxing scalar types has been extended to work for
structtypes. Notable changes:IRType.structnow takesobjs : Array IRTypeandusize ssize : Natinstead of justArray IRType.objsis meant to mirror the projections from the regular constructor layout andusizeandssizecorrespond to the same fields in the constructor layoutIRType.uniontakes an array oftypes : Array IRTypethat now should all beIRType.structsExpr.unboxalso works forstruct/unionExpr.boxnow has two roles: boxing scalars and structs and "reshaping" structs (that is, translating between two unboxed struct/union types)FnBody.inc/FnBody.decon an unboxed struct corresponds to incrementing/decrementing every field.Expr.proj,Expr.uproj,Expr.sproj,Expr.usetandExpr.ssetnow take acidx : Natparameter to indicate which part of the union should be used.projandctor