feat: per-function termination hints #3040

nomeata · 2023-12-08T10:41:45Z

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.

leanprover-community-mathlib4-bot · 2023-12-08T19:01:34Z

💥 Mathlib branch lean-pr-testing-3040 build failed against this PR. (2023-12-08 19:01:32) View Log
💥 Mathlib branch lean-pr-testing-3040 build failed against this PR. (2023-12-08 19:25:36) View Log
💥 Mathlib branch lean-pr-testing-3040 build failed against this PR. (2023-12-09 11:24:01) View Log
💥 Mathlib branch lean-pr-testing-3040 build failed against this PR. (2023-12-11 12:21:46) View Log
💥 Mathlib branch lean-pr-testing-3040 build failed against this PR. (2023-12-11 14:38:15) View Log
❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-12-11 21:33:23)
💥 Mathlib branch lean-pr-testing-3040 build failed against this PR. (2023-12-13 14:24:49) View Log
🟡 Mathlib branch lean-pr-testing-3040 build against this PR was cancelled. (2023-12-13 14:55:04) View Log
🟡 Mathlib branch lean-pr-testing-3040 build against this PR was cancelled. (2023-12-13 14:59:44) View Log
🟡 Mathlib branch lean-pr-testing-3040 build against this PR was cancelled. (2023-12-13 15:23:30) View Log
❌ Mathlib branch lean-pr-testing-3040 built against this PR, but linting failed. (2023-12-13 16:09:53) View Log
✅ Mathlib branch lean-pr-testing-3040 has successfully built against this PR. (2023-12-13 18:18:45) View Log
✅ Mathlib branch lean-pr-testing-3040 has successfully built against this PR. (2023-12-13 18:56:14) View Log
💥 Mathlib branch lean-pr-testing-3040 build failed against this PR. (2023-12-20 14:38:59) View Log
💥 Mathlib branch lean-pr-testing-3040 build failed against this PR. (2023-12-20 14:44:33) View Log
🟡 Mathlib branch lean-pr-testing-3040 build this PR didn't complete normally. (2023-12-20 14:58:23) View Log
💥 Mathlib branch lean-pr-testing-3040 build failed against this PR. (2023-12-20 15:12:27) View Log
💥 Mathlib branch lean-pr-testing-3040 build failed against this PR. (2023-12-20 15:49:38) View Log
💥 Mathlib branch lean-pr-testing-3040 build failed against this PR. (2023-12-20 16:04:10) View Log
🟡 Mathlib branch lean-pr-testing-3040 build against this PR was cancelled. (2023-12-20 16:24:25) View Log
✅ Mathlib branch lean-pr-testing-3040 has successfully built against this PR. (2023-12-20 16:56:45) View Log
✅ Mathlib branch lean-pr-testing-3040 has successfully built against this PR. (2023-12-20 18:09:55) View Log
❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-2023-12-21' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow. (2023-12-21 09:25:07)
🟡 Mathlib branch lean-pr-testing-3040 build this PR didn't complete normally. (2023-12-21 10:35:29) View Log
💥 Mathlib branch lean-pr-testing-3040 build failed against this PR. (2023-12-21 11:09:55) View Log
💥 Mathlib branch lean-pr-testing-3040 build failed against this PR. (2023-12-21 11:31:41) View Log
💥 Mathlib branch lean-pr-testing-3040 build failed against this PR. (2023-12-21 17:14:40) View Log
💥 Mathlib branch lean-pr-testing-3040 build failed against this PR. (2023-12-21 17:35:37) View Log
💥 Mathlib branch lean-pr-testing-3040 build failed against this PR. (2023-12-21 22:11:40) View Log
💥 Mathlib branch lean-pr-testing-3040 build failed against this PR. (2023-12-22 13:06:42) View Log
💥 Mathlib branch lean-pr-testing-3040 build failed against this PR. (2023-12-22 14:00:18) View Log
💥 Mathlib branch lean-pr-testing-3040 build failed against this PR. (2023-12-22 15:34:36) View Log
💥 Mathlib branch lean-pr-testing-3040 build failed against this PR. (2023-12-22 15:58:10) View Log
✅ Mathlib branch lean-pr-testing-3040 has successfully built against this PR. (2023-12-23 11:56:22) View Log
✅ Mathlib branch lean-pr-testing-3040 has successfully built against this PR. (2023-12-23 12:37:43) View Log
🟡 Mathlib branch lean-pr-testing-3040 build this PR didn't complete normally. (2024-01-02 11:31:53) View Log
🟡 Mathlib branch lean-pr-testing-3040 build this PR didn't complete normally. (2024-01-02 12:51:31) View Log
🟡 Mathlib branch lean-pr-testing-3040 build this PR didn't complete normally. (2024-01-02 15:20:13) View Log
🟡 Mathlib branch lean-pr-testing-3040 build this PR didn't complete normally. (2024-01-02 17:05:00) View Log
❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-2023-12-31' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow. (2024-01-03 13:19:24)
💥 Mathlib branch lean-pr-testing-3040 build failed against this PR. (2024-01-05 10:49:33) View Log
💥 Mathlib branch lean-pr-testing-3040 build failed against this PR. (2024-01-05 12:13:01) View Log
💥 Mathlib branch lean-pr-testing-3040 build failed against this PR. (2024-01-05 12:22:56) View Log
✅ Mathlib branch lean-pr-testing-3040 has successfully built against this PR. (2024-01-05 13:34:04) View Log
✅ Mathlib branch lean-pr-testing-3040 has successfully built against this PR. (2024-01-05 14:37:35) View Log
✅ Mathlib branch lean-pr-testing-3040 has successfully built against this PR. (2024-01-08 07:48:40) View Log
🟡 Mathlib branch lean-pr-testing-3040 build against this PR was cancelled. (2024-01-08 12:13:10) View Log
✅ Mathlib branch lean-pr-testing-3040 has successfully built against this PR. (2024-01-08 13:30:26) View Log
✅ Mathlib branch lean-pr-testing-3040 has successfully built against this PR. (2024-01-08 17:22:01) View Log
❗ Mathlib CI will not be attempted unless your PR branches off the 'nightly-with-mathlib' branch. (2024-01-09 10:34:08)

tests/lean/termination_by_where.lean

this makes the necessary changes to compile with the `termination_by` syntax refactoring in leanprover/lean4#3040

src/Lean/Elab/PreDefinition/WF/PackMutual.lean

extracted from #3040 to keep the diff smaller

src/Lean/Elab/DefView.lean

extracted from #3040 to keep the diff smaller

src/Lean/Elab/PreDefinition/WF/GuessLex.lean

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.

…hints) (#95)

nomeata changed the title ~~joachim/per function hints~~ feat: Per-function termination hints Dec 8, 2023

nomeata changed the title ~~feat: Per-function termination hints~~ feat: per-function termination hints Dec 8, 2023

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

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 8, 2023

Update lean-toolchain for testing leanprover/lean4#3040

7badbe7

leanprover-community-mathlib4-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Dec 8, 2023

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 8, 2023

Trigger CI for leanprover/lean4#3040

b5b35bb

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 9, 2023

Trigger CI for leanprover/lean4#3040

7cce4c6

nomeata force-pushed the joachim/per-function-hints branch from 6cd5349 to 31d5ba7 Compare December 11, 2023 11:57

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 11, 2023

Trigger CI for leanprover/lean4#3040

31cc04c

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 11, 2023

Trigger CI for leanprover/lean4#3040

73342bc

nomeata mentioned this pull request Dec 11, 2023

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

Closed

kim-em reviewed Dec 12, 2023

View reviewed changes

tests/lean/termination_by_where.lean Outdated Show resolved Hide resolved

nomeata added a commit to nomeata/batteries that referenced this pull request Dec 13, 2023

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

refactor: Adjust to new termination_by syntax leanprover-community/batteries#446

Closed

refactor: Adjust to new termination_by syntax leanprover-community/mathlib4#9019

Closed

WF.Fix: Does not deduplicate goals when lambdas are duplicated #3062

Open

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 13, 2023

Trigger CI for leanprover/lean4#3040

a741948

leanprover-community-mathlib4-bot 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

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 13, 2023

Trigger CI for leanprover/lean4#3040

6137839

kim-em reviewed Dec 14, 2023

View reviewed changes

src/Lean/Elab/PreDefinition/WF/PackMutual.lean Outdated Show resolved Hide resolved

nomeata added a commit that referenced this pull request Dec 15, 2023

refactor: move unpackArg etc. to WF.PackDomain/WF.PackMutual

cfb3d0d

extracted from #3040 to keep the diff smaller

nomeata mentioned this pull request Dec 15, 2023

refactor: move unpackArg etc. to WF.PackDomain/WF.PackMutual #3077

Merged

nomeata commented Dec 15, 2023

View reviewed changes

src/Lean/Elab/DefView.lean Outdated Show resolved Hide resolved

nomeata mentioned this pull request Dec 16, 2023

RFC: termination_by syntax: less wiggle-room with variables #3081

Closed

github-merge-queue bot pushed a commit that referenced this pull request Dec 18, 2023

refactor: move unpackArg etc. to WF.PackDomain/WF.PackMutual (#3077)

7acbee8

extracted from #3040 to keep the diff smaller

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 20, 2023

Trigger CI for leanprover/lean4#3040

7685d03

leanprover-community-mathlib4-bot 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

leodemoura approved these changes Jan 6, 2024

View reviewed changes

src/Lean/Elab/PreDefinition/WF/GuessLex.lean Outdated Show resolved Hide resolved

src/Lean/Elab/PreDefinition/WF/GuessLex.lean Show resolved Hide resolved

src/Lean/Elab/PreDefinition/WF/GuessLex.lean Show resolved Hide resolved

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

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 8, 2024

Trigger CI for leanprover/lean4#3040

dca6bb8

github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 8, 2024 10:29 Inactive

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 8, 2024

Trigger CI for leanprover/lean4#3040

8f17464

nomeata force-pushed the joachim/per-function-hints branch from 8278b00 to f2bc037 Compare January 8, 2024 11:30

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 8, 2024

Trigger CI for leanprover/lean4#3040

94946e3

github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 8, 2024 12:22 Inactive

nomeata added will-merge-soon …unless someone speaks up and removed awaiting-author Waiting for PR author to address issues labels Jan 8, 2024

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 8, 2024

Trigger CI for leanprover/lean4#3040

e55e250

nomeata force-pushed the joachim/per-function-hints branch from f2bc037 to 77da1f2 Compare January 9, 2024 09:46

github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 9, 2024 10:30 Inactive

nomeata force-pushed the joachim/per-function-hints branch 2 times, most recently from 44db469 to 6818314 Compare January 9, 2024 14:48

github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 9, 2024 15:31 Inactive

nomeata force-pushed the joachim/per-function-hints branch from 6818314 to 1e4eefb Compare January 10, 2024 14:58

nomeata added 3 commits January 10, 2024 15:59

chore: update stage0

e554131

refactor: termination_by changes in stdlib

b93cd98

nomeata force-pushed the joachim/per-function-hints branch from 1e4eefb to b93cd98 Compare January 10, 2024 14:59

github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 10, 2024 15:40 Inactive

Kha merged commit 368ead5 into master Jan 10, 2024
20 checks passed

nomeata deleted the joachim/per-function-hints branch January 10, 2024 16:28

This was referenced Jan 11, 2024

chore: adaptions for nightly-2023-01-11 leanprover-community/batteries#524

Merged

chore: use termination_by in Nat.gcd #3164

Merged

kim-em added a commit to leanprover-community/aesop that referenced this pull request Jan 13, 2024

chore: adaptations for leanprover/lean4#3040

7b18a25

kim-em mentioned this pull request Jan 13, 2024

chore: adaptations for leanprover/lean4#3040 (changes to termination hints) leanprover-community/aesop#95

Merged

kim-em added a commit to leanprover-community/aesop that referenced this pull request Jan 13, 2024

chore: adaptations for leanprover/lean4#3040 (changes to termination …

60de6c7

…hints) (#95)

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: per-function termination hints #3040

feat: per-function termination hints #3040

nomeata commented Dec 8, 2023 •

edited

Loading

leanprover-community-mathlib4-bot commented Dec 8, 2023 •

edited

Loading

feat: per-function termination hints #3040

feat: per-function termination hints #3040

Conversation

nomeata commented Dec 8, 2023 • edited Loading

leanprover-community-mathlib4-bot commented Dec 8, 2023 • edited Loading

nomeata commented Dec 8, 2023 •

edited

Loading

leanprover-community-mathlib4-bot commented Dec 8, 2023 •

edited

Loading