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
Draft
wants to merge 16 commits into
base: master
Choose a base branch
from
Draft

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

wants to merge 16 commits into from
+8,364 −6,641

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

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)

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%)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@hargoniX hargoniX Awaiting requested review from hargoniX hargoniX will be requested when the pull request is marked ready for review hargoniX is a code owner

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura will be requested when the pull request is marked ready for review leodemoura is a code owner

Assignees

No one assigned

Labels

breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changes-stage0 Contains stage0 changes, merge manually using rebase 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