Skip to content

perf: de-fuel some recursive definitions in Core #11416

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
nomeata merged 22 commits into from
Dec 5, 2025
Merged

perf: de-fuel some recursive definitions in Core #11416

nomeata merged 22 commits into from
Dec 5, 2025

Conversation

@nomeata
Copy link
Collaborator

@nomeata nomeata commented Nov 28, 2025

This PR follows up on #7965 and avoids manual fuel constructions in some recursive definitions.

nomeata added 15 commits April 14, 2025 21:40
@nomeata
feat: dedicated fix operator for well-founded recursion on Nat
c2e2396 
This PR lets recursive functions defined by well-founded recursion use a
different `fix` function when the termination measure is of type `Nat`.
This fix-point operator use structural recursion on “fuel”, initialized
by the given measure, and is thus reasonable to reduce, e.g. in `by
decide` proofs.
@nomeata
Merge branch 'nightly-with-mathlib' of https://github.com/leanprover/…
45a43c7 
…lean4 into joachim/nat-fix
@nomeata
Merge branch 'master' of https://github.com/leanprover/lean4 into joa…
b2c8896 
…chim/nat-fix
@nomeata
Merge branch 'nightly-with-mathlib' of https://github.com/leanprover/…
02637a0 
…lean4 into joachim/nat-fix
@nomeata
Add test for #11181
926dfc0
@nomeata
Require stage0 update
119a0ad
@nomeata
move
ba51f29
@nomeata
fix tests
912a28c
@nomeata
Add test for #2021 (not fixed)
80775ca
@nomeata
Merge branch 'nightly-with-mathlib' of https://github.com/leanprover/…
24dd7fc 
…lean4 into joachim/nat-fix
@nomeata
Update wfirred test
dc23022
@nomeata
Disable special attribute handling for Nat recursion (ugly, sorry for…
d08c0de 
… that)
@nomeata
Prevent accidential reduction of open fuel
1a3901a
@nomeata
More tests
e1506cd
@nomeata
chore: update stage0
5e5421d
@nomeata
Copy link
Collaborator Author

nomeata commented Nov 28, 2025

!radar

@leanprover-radar
Copy link

leanprover-radar commented Nov 28, 2025 •
edited
Loading

Benchmark results for e09c73e against a4f9a79 are in! @nomeata

Major changes (2)
  • 🟥 build//instructions: +176.5G (+1.4%)
  • ✅ mut_rec_wf//instructions: -769.2M (-2.5%)
Minor changes (2)
  • ✅ lake config import//instructions: -8.5M (-0.5%)
  • ✅ lake env//instructions: -15.7M (-1.0%)

@github-actions github-actions bot added the changes-stage0 Contains stage0 changes, merge manually using rebase label Nov 28, 2025
@nomeata
Copy link
Collaborator Author

nomeata commented Nov 28, 2025

!radar

@leanprover-radar
Copy link

leanprover-radar commented Nov 28, 2025 •
edited
Loading

Benchmark results for 5ee79ed against a4f9a79 are in! @nomeata

Major changes (4)
  • 🟥 build//instructions: +178.2G (+1.4%)
  • 🟥 grind_ring_5.lean//instructions: +1.1G (+12.2%)
  • ✅ lake env//instructions: -16.9M (-1.0%)
  • ✅ mut_rec_wf//instructions: -770.3M (-2.5%)
Minor changes (1)
  • ✅ size/init/.olean//bytes: -221kiB (-0.2%)

@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 Nov 28, 2025
@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Nov 28, 2025 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-11-27 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-11-28 12:09:11)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-12-05 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-12-05 15:07:11)

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 28, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#11416
2c0779d
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Nov 28, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#11416
d6c0374
@leanprover-community-bot leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Nov 28, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Nov 28, 2025

Mathlib CI status (docs):

@nomeata
Copy link
Collaborator Author

nomeata commented Nov 28, 2025

!radar

@leanprover-radar
Copy link

leanprover-radar commented Nov 28, 2025 •
edited
Loading

Benchmark results for 5e5421d against a4f9a79 are in! @nomeata

Runs (2)
  • 🟥 build exited with code 2
  • 🟥 other exited with code 2

@nomeata
Copy link
Collaborator Author

nomeata commented Nov 28, 2025

!radar

@leanprover-radar
Copy link

leanprover-radar commented Nov 28, 2025 •
edited
Loading

Benchmark results for c49d679 against a4f9a79 are in! @nomeata

Major changes (3)
  • 🟥 build//instructions: +173.5G (+1.4%)
  • ✅ lake env//instructions: -16.4M (-1.0%)
  • ✅ mut_rec_wf//instructions: -771.2M (-2.5%)

@nomeata
Copy link
Collaborator Author

nomeata commented Dec 5, 2025

!radar

@leanprover-radar
Copy link

leanprover-radar commented Dec 5, 2025 •
edited
Loading

Benchmark results for 74c7bab against 455fd0b are in! @nomeata

Minor changes (1)
  • ✅ size/init/.olean//bytes: -197kiB (-0.2%)

@github-actions github-actions bot removed the changes-stage0 Contains stage0 changes, merge manually using rebase label Dec 5, 2025
@nomeata
Copy link
Collaborator Author

nomeata commented Dec 5, 2025

!radar

@leanprover-radar
Copy link

leanprover-radar commented Dec 5, 2025 •
edited
Loading

Benchmark results for 22e91fa against 455fd0b are in! @nomeata

Minor changes (1)
  • ✅ size/init/.olean//bytes: -197kiB (-0.2%)

@nomeata nomeata marked this pull request as ready for review December 5, 2025 14:29
@nomeata nomeata requested a review from kim-em as a code owner December 5, 2025 14:29
@nomeata nomeata added awaiting-mathlib We should not merge this until we have a successful Mathlib build and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Dec 5, 2025
@nomeata nomeata enabled auto-merge December 5, 2025 14:30
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Dec 5, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#11416
d9077f3
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Dec 5, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#11416
6b93a8b
@leanprover-community-bot leanprover-community-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed awaiting-mathlib We should not merge this until we have a successful Mathlib build labels Dec 5, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Dec 5, 2025

@nomeata nomeata added this pull request to the merge queue Dec 5, 2025
Merged via the queue into master with commit d4c832e Dec 5, 2025
32 of 34 checks passed
algebraic-dev pushed a commit that referenced this pull request Dec 8, 2025
@nomeata @algebraic-dev
perf: de-fuel some recursive definitions in Core (#11416)
e84a2af 
This PR follows up on #7965 and avoids manual fuel constructions in some
recursive definitions.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees

No one assigned

Labels

builds-mathlib CI has verified that Mathlib builds against this PR 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.

5 participants

@nomeata @leanprover-radar @leanprover-bot @leanprover-community-bot