Skip to content

refactor: port simple ground expr extraction from IR to LCNF#12705

Merged
hargoniX merged 1 commit intomasterfrom
hbv/port_simple_ground_expr
Feb 26, 2026
Merged

refactor: port simple ground expr extraction from IR to LCNF#12705
hargoniX merged 1 commit intomasterfrom
hbv/port_simple_ground_expr

Conversation

@hargoniX
Copy link
Copy Markdown
Contributor

This PR ports the simple ground expression extraction pass from IR to LCNF.

I locally confirmed that this produces no diff between stage1/stage2 at the C level (apart from the
changed compiler files) so this should essentially be binary equivalent.

@hargoniX hargoniX requested a review from leodemoura as a code owner February 26, 2026 13:42
@hargoniX
Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Feb 26, 2026

Benchmark results for 3f65b0d against 846420d are in! @hargoniX

  • 🟥 build//instructions: +619.7M (+0.00%)

Small changes (1✅)

  • build/module/Lean.Compiler.IR//instructions: -40.8M (-5.44%) (reduced significance based on *//lines)

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Feb 26, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 846420dabab15cec6d4c095069dc34d7a9ba4b59 --onto c595413fccaa47ebdc399d9b817c17425687fc26. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-26 15:05:58)

@leanprover-bot
Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 846420dabab15cec6d4c095069dc34d7a9ba4b59 --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-02-26 15:06:00)

@hargoniX hargoniX added the changelog-compiler Compiler, runtime, and FFI label Feb 26, 2026
@hargoniX hargoniX enabled auto-merge February 26, 2026 15:09
@hargoniX hargoniX added this pull request to the merge queue Feb 26, 2026
Merged via the queue into master with commit f83a8b4 Feb 26, 2026
23 checks passed
sgraf812 pushed a commit that referenced this pull request Feb 26, 2026
This PR ports the simple ground expression extraction pass from IR to
LCNF.

I locally confirmed that this produces no diff between stage1/stage2 at
the C level (apart from the
changed compiler files) so this should essentially be binary equivalent.
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

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants