Skip to content

feat: per-function termination hints#3040

Merged
Kha merged 3 commits intomasterfrom
joachim/per-function-hints
Jan 10, 2024
Merged

feat: per-function termination hints#3040
Kha merged 3 commits intomasterfrom
joachim/per-function-hints

Conversation

@nomeata
Copy link
Copy Markdown
Collaborator

@nomeata nomeata commented Dec 8, 2023 •
edited
Loading

This change

  • moves termination_by and decreasing_by next to the function they apply to
  • simplify the syntax of termination_by
  • apply the decreasing_by goal to all goals at once, for better interactive use.

See the section in RELEASES.md for more details and migration advise.

This is a hard breaking change, requiring developers to touch every termination_by in their code base. We decided to still do it as a hard-breaking change, because supporting both old and new syntax at the same time would be non-trivial, and not save that much. Moreover, this requires changes to some metaprograms that developers might have written, and supporting both syntaxes at the same time would make their migration harder.

Std and mathlib updates are prepared at

Fixes #2921 and #3081.

@nomeata nomeata changed the title joachim/per function hints feat: Per-function termination hints Dec 8, 2023
@nomeata nomeata changed the title feat: Per-function termination hints feat: per-function termination hints Dec 8, 2023
@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 Dec 8, 2023
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Dec 8, 2023
Update lean-toolchain for testing leanprover/lean4#3040
7badbe7
@ghost ghost added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Dec 8, 2023
@ghost
Copy link
Copy Markdown

ghost commented Dec 8, 2023 •
edited by ghost
Loading

ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Dec 8, 2023
Trigger CI for leanprover/lean4#3040
b5b35bb
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Dec 9, 2023
Trigger CI for leanprover/lean4#3040
7cce4c6
@nomeata nomeata force-pushed the joachim/per-function-hints branch from 6cd5349 to 31d5ba7 Compare December 11, 2023 11:57
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Dec 11, 2023
Trigger CI for leanprover/lean4#3040
31cc04c
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Dec 11, 2023
Trigger CI for leanprover/lean4#3040
73342bc
@nomeata nomeata mentioned this pull request Dec 11, 2023
Closed
kim-em
kim-em reviewed Dec 12, 2023
View reviewed changes
nomeata added a commit to nomeata/batteries that referenced this pull request Dec 13, 2023
@nomeata
refactor: Adjust to new termination_by syntax
1020a8d 
this makes the necessary changes to compile with the `termination_by`
syntax refactoring in leanprover/lean4#3040
This was referenced Dec 13, 2023
Closed
Closed
Open
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Dec 13, 2023
Trigger CI for leanprover/lean4#3040
a741948
@ghost ghost added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Dec 13, 2023
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Dec 13, 2023
Trigger CI for leanprover/lean4#3040
6137839
kim-em
kim-em reviewed Dec 14, 2023
View reviewed changes
nomeata added a commit that referenced this pull request Dec 15, 2023
@nomeata
refactor: move unpackArg etc. to WF.PackDomain/WF.PackMutual
cfb3d0d 
extracted from #3040 to keep the diff smaller
@nomeata nomeata mentioned this pull request Dec 15, 2023
Merged
nomeata
nomeata commented Dec 15, 2023
View reviewed changes
@nomeata nomeata mentioned this pull request Dec 16, 2023
Closed
github-merge-queue bot pushed a commit that referenced this pull request Dec 18, 2023
@nomeata
refactor: move unpackArg etc. to WF.PackDomain/WF.PackMutual (#3077)
7acbee8 
extracted from #3040 to keep the diff smaller
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Dec 20, 2023
Trigger CI for leanprover/lean4#3040
7685d03
@ghost ghost added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed builds-mathlib CI has verified that Mathlib builds against this PR labels Dec 20, 2023
@nomeata nomeata force-pushed the joachim/per-function-hints branch 2 times, most recently from c876e4b to d6b7201 Compare January 3, 2024 11:23
@nomeata
Copy link
Copy Markdown
Collaborator Author

nomeata commented Jan 3, 2024

Rebased this PR (against all my strongly held convictions) because it needs a stage0 update in the middle. Needs to be rebase-merged. This seems to be good to go, but I’ll wait for mathlib CI to work again, to make sure that the std and mathlib PRs are up-to-date, and check back with Scott about how to merge this with the least release complications.

@nomeata nomeata added full-ci will-merge-soon …unless someone speaks up labels Jan 3, 2024
@nomeata nomeata force-pushed the joachim/per-function-hints branch from d6b7201 to 800fe3d Compare January 5, 2024 10:00
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jan 5, 2024
Trigger CI for leanprover/lean4#3040
d5a365f
@ghost ghost added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed builds-mathlib CI has verified that Mathlib builds against this PR labels Jan 5, 2024
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 5, 2024 10:51 Inactive
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jan 5, 2024
Trigger CI for leanprover/lean4#3040
d706231
@ghost ghost added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Jan 5, 2024
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jan 5, 2024
Trigger CI for leanprover/lean4#3040
5aa8d57
leodemoura
leodemoura reviewed Jan 6, 2024
View reviewed changes
leodemoura
leodemoura reviewed Jan 6, 2024
View reviewed changes
leodemoura
leodemoura approved these changes Jan 6, 2024
View reviewed changes
@kim-em kim-em added awaiting-author Waiting for PR author to address issues and removed will-merge-soon …unless someone speaks up labels Jan 8, 2024
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jan 8, 2024
Trigger CI for leanprover/lean4#3040
dca6bb8
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 8, 2024 10:29 Inactive
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jan 8, 2024
Trigger CI for leanprover/lean4#3040
8f17464
@nomeata nomeata force-pushed the joachim/per-function-hints branch from 8278b00 to f2bc037 Compare January 8, 2024 11:30
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jan 8, 2024
Trigger CI for leanprover/lean4#3040
94946e3
@nomeata
feat: per-function termination hints
f92fdc0 
This change

 * moves `termination_by` and `decreasing_by` next to the function they
   apply to
 * simplify the syntax of `termination_by`
 * apply the `decreasing_by` goal to all goals at once, for better
   interactive use.

See the section in `RELEASES.md` for more details and migration advise.

This is a hard breaking change, requiring developers to touch every
`termination_by` in their code base. We decided to still do it as a
hard-breaking change, because supporting both old and new syntax at the
same time would be non-trivial, and not save that much. Moreover, this
requires changes to some metaprograms that developers might have
written, and supporting both syntaxes at the same time would make
_their_ migration harder.
@nomeata
chore: update stage0
e554131
@nomeata
refactor: termination_by changes in stdlib
b93cd98
This was referenced Jan 11, 2024
Merged
Merged
@kim-em kim-em mentioned this pull request Jan 13, 2024
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em kim-em left review comments

@digama0 digama0 digama0 left review comments

@david-christiansen david-christiansen david-christiansen approved these changes

@leodemoura leodemoura leodemoura approved these changes

@tydeu tydeu tydeu approved these changes

@Kha Kha Awaiting requested review from Kha

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 will-merge-soon …unless someone speaks up

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

RFC: Run decreasing_by tactic on all goals, not each goal

7 participants

@nomeata @Kha @david-christiansen @kim-em @digama0 @leodemoura @tydeu