Skip to content

perf: widen more in ElimDeadBranches #10856

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.

Sign up for GitHub

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

Jump to bottom
Merged
hargoniX merged 1 commit into from
Oct 27, 2025
Merged

perf: widen more in ElimDeadBranches #10856

hargoniX merged 1 commit into from
Oct 27, 2025

Conversation

@hargoniX
Copy link
Contributor

@hargoniX hargoniX commented Oct 20, 2025 •
edited
Loading

This PR performs more widening in ElimDeadBranches in an attempt to improve performance in situations with a lot of local precision.

While this is not enough to make the compilation instant it pushes compilation time from 12s to 3s for the example in #10857 and barely introduces regressions so it seems like a good first step in this direction.

Closes: #10857

@hargoniX
Copy link
Contributor Author

hargoniX commented Oct 20, 2025

!radar

@leanprover-radar
Copy link

leanprover-radar commented Oct 20, 2025 •
edited
Loading

Benchmark results for 6910b6e against e3a5369 are in! @hargoniX

@hargoniX
Copy link
Contributor Author

hargoniX commented Oct 20, 2025

!radar

@leanprover-radar
Copy link

leanprover-radar commented Oct 20, 2025 •
edited
Loading

Benchmark results for 673935e against e3a5369 are in! @hargoniX

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

leanprover-community-bot commented Oct 20, 2025 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e3a5369bd7705e732d571319a7d3513ba9a70a63 --onto 135e7e7bd3908515354137c952f0d40945fff757. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-20 19:33:04)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 3a42ee0c3060e2a8365927d205ead5990366053d --onto 97d63db52cd2fc3353f8a75f48209de0011f1bd3. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-27 09:31:15)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Oct 20, 2025 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase e3a5369bd7705e732d571319a7d3513ba9a70a63 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-20 19:33:06)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 3a42ee0c3060e2a8365927d205ead5990366053d --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-27 09:31:16)

@hargoniX hargoniX added the changelog-compiler Compiler, runtime, and FFI label Oct 27, 2025
@hargoniX hargoniX changed the title perf: widen more perf: widen more in ElimDeadBranches Oct 27, 2025
@hargoniX hargoniX marked this pull request as ready for review October 27, 2025 08:44
@hargoniX hargoniX requested a review from leodemoura as a code owner October 27, 2025 08:44
@hargoniX
Copy link
Contributor Author

hargoniX commented Oct 27, 2025

!radar

@leanprover-radar
Copy link

leanprover-radar commented Oct 27, 2025 •
edited
Loading

Benchmark results for 5d8e5aa against 3a42ee0 are in! @hargoniX

Minor changes (1)
  • riscv-ast.lean//instructions changed by +0.7% (🟥).

@hargoniX hargoniX added this pull request to the merge queue Oct 27, 2025
Merged via the queue into master with commit 7e1be20 Oct 27, 2025
17 checks passed
@hargoniX hargoniX deleted the hbv/elim_dead_perf branch October 27, 2025 09:42
wkrozowski pushed a commit to wkrozowski/lean4 that referenced this pull request Oct 27, 2025
@hargoniX @wkrozowski
perf: widen more in ElimDeadBranches (leanprover#10856)
0b4d490 
This PR performs more widening in ElimDeadBranches in an attempt to
improve performance in situations with a lot of local precision.

While this is not enough to make the compilation instant it pushes
compilation time from 12s to 3s for the example in leanprover#10857 and barely
introduces regressions so it seems like a good first step in this
direction.

Closes: leanprover#10857
@nomeata nomeata mentioned this pull request Oct 29, 2025
Merged
@iamrecursion iamrecursion mentioned this pull request Nov 17, 2025
Open
4 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

Assignees

No one assigned

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

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Compiler regression on compiling deeply nested lambdas

5 participants

@hargoniX @leanprover-radar @leanprover-community-bot @leanprover-bot