Skip to content

Conversation

@hargoniX
Copy link
Contributor

@hargoniX hargoniX commented Sep 30, 2025

This PR reduces the aggressiveness of the dead let eliminator from lambda RC.

The motivation for this is that all other passes in lambda RC respect impurity but the dead let eliminator still operates under the assumption of purity. There is a couple of motivations for the elim dead let elaborator:

  • unused projections introduced by the ToIR translation
  • the elim dead branch pass introducing new opportunities
  • closed term extraction introducing new opportunities

@hargoniX hargoniX added the changelog-compiler Compiler, runtime, and FFI label Sep 30, 2025
@hargoniX hargoniX changed the title refactor: remove dead let eliminator from lambda RC refactor: tame down dead let eliminator in lambda RC Sep 30, 2025
@hargoniX
Copy link
Contributor Author

!bench

@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 Sep 30, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase dfd3d185300df044fa087d3fa166cb6fb3bd8269 --onto 7d55c033e1f0ad8cb7c2b9ab72e5db40ce192222. You can force Mathlib CI using the force-mathlib-ci label. (2025-09-30 18:43:33)

@leanprover-bot
Copy link
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 dfd3d185300df044fa087d3fa166cb6fb3bd8269 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-09-30 18:43:34)

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 545fff9.
There were significant changes against commit dfd3d18:

  Benchmark   Metric           Change
  ============================================
- stdlib      grind linarith    19.1% (26.0 σ)

@hargoniX hargoniX added this pull request to the merge queue Sep 30, 2025
Merged via the queue into master with commit d88e417 Sep 30, 2025
16 checks passed
@hargoniX hargoniX deleted the hbv/ir_impure branch September 30, 2025 20:40
arthur-adjedj pushed a commit to arthur-adjedj/lean4 that referenced this pull request Oct 6, 2025
This PR reduces the aggressiveness of the dead let eliminator from
lambda RC.

The motivation for this is that all other passes in lambda RC respect
impurity but the dead let eliminator still operates under the assumption
of purity. There is a couple of motivations for the elim dead let
elaborator:
- unused projections introduced by the ToIR translation
- the elim dead branch pass introducing new opportunities
- closed term extraction introducing new opportunities
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.

5 participants