refactor: post-stage0 fixes to #3040 #3110
Conversation
until around 7fe6881 the way to define well-founded recursions was to specify a `WellFoundedRelation` on the argument explicitly. This was rather low-level, for example one had to predict the packing of multiple arguments into `PProd`s, the packing of mutual functions into `PSum`s, and the cliques that were calculated. Then the current `termination_by` syntax was introduced, where you sepecify the termination argument at a higher level (one clause per functions, unpacked arguments), and the `WellFoundedRelation` is found using type class resolution. The old syntax was kept around as `termination_by'`. But at the time of writing, this is not used anywhere in the lean, std, mathlib or the theroem-proving-in-lean repositories. Also, should be possible to express anything that the old syntax supported also with the new one, possibly requiring a helper type with a suitable instance, or a very generic wrapper like ``` inductive WithWFRel {a : Type _} {rel : a → a → Prop} (h : WellFounded rel) where | mk : a -> WithWFRel h instance : WellFoundedRelation (WithWFRel h) := invImage (fun x => match x with | .mk x => x) ⟨_, h⟩ ``` Since the old syntax is unused, has an unhelpful name and relies on internals, this removes the support. Now is a good time before the refactoring that's planned in #2921. The test suite was updated without particular surprises. The parametric `terminationHint` parser is gone, which means we can match on syntax more easily now, in `expandDecreasingBy?`.
…termination_by_core
…termination_by_core
but I am a bit stuck/confused in `src/lake/Lake/DSL/DeclUtil.lean`
|
Normally I do this kind of thing using a single PR which has a |
|
I'm creating this mostly to test what would happen. Maybe we should enable CI for branches to not have to create PRa just to run CI. (Additionally I think it's preferable to use the automatic stage0 update on master, no need to worry if the stage0 code was created cleanly.) Ah, but maybe this doesn't work here, because library changes will have to be included in this PR. |
|
The point is not to use the update stage0 commit when it is actually merged, in fact it usually has to be recreated on each rebase. The point is so that the tests pass and the PR is all in one place; handling dependent PRs is more complicated, maintenance-wise, than just replacing the update-stage0 commit when bumping such a PR. |
|
Mario, the point is that in this case the stage 0 update is not necessary as part of the original PR. I agree with Joachim that a follow-up PR is easier in this case. |
|
In any case I should be better at marking PRs (besides marking them as Draft) that are just me trying something on the side, which may or may not turn in to real PRs :-) I was hoping I can proceed by merging #3040, then automatic stage0 update on master, then clean-up-PR (like with #2964 and then #3105), but that may not be possible in this case, where updating stage0 will break CI until broken library code is updated. |
|
I think a PR which fails the stage2 build should not be merged, any stage0 update and other post-stage0 fixes should be done on the same PR. If that's not the situation here, then feel free to ignore, but it sounds like #3040 still has issues of this form. |
|
It probably has, which I am just discovering. I agree that in that case we have to go back to the multiple-rebased-commits-including-stage0-on-one-PR workflow. |
nomeata
force-pushed
the
joachim/per-function-hints-stage0
branch
from
bae229f to
30c17cb
Compare
github-actions
bot
added
the
toolchain-available
leanprover-community-mathlib4-bot
added
the
breaks-mathlib
|
leanprover-community-mathlib4-bot
added
builds-mathlib
nomeata
force-pushed
the
joachim/per-function-hints
branch
7 times, most recently
from
44db469 to
6818314
Compare
This pull request is only opened to run CI on stuff I may do once #3040 is
merged and stage0 updated.