It seems that failures in the compilation of hydra-battles (hence goedel) on dev come from a recent change in
auto 's behaviour.
The error which appears is
no such goal. I'm starting to fix that.
auto has indeed recently become more powerful
A way of fixing this which is backward compatible is to do some explicit goal management (avoid
; auto and
@Pierre Castéran please flag up when you have hydra-battles working on
coq.dev, then I can enable CI for
coq.dev for goedel.
Ok, It will take some time ...
OK, then I'll merge this one in the meantime: https://github.com/coq-community/goedel/pull/15
It represents days (weeks?) of work. This, plus the 8.16 changes. Discouraging ...
Fixing the auto problems?
> grep auto theories/ordinals/*/*.v | wc -l 5018 > grep trivial theories/ordinals/*/*.v | wc -l 1071
Let me try. Which branch should I use?
Yes, it’s on master. For the time being, I just looked at 3 files:
Iterates and partially
AP. I believe the
autos at the end of a bullet are OK. There were also issues with several
based on this case, we could consider adding at least hydra-battles part to Coq CI (so it at least builds when tactic behavior gets updated)
Hum, this is weird. I did a single fix and the whole of
diff --git a/theories/ordinals/Schutte/AP.v b/theories/ordinals/Schutte/AP.v index 267c2fe..7b67616 100644 --- a/theories/ordinals/Schutte/AP.v +++ b/theories/ordinals/Schutte/AP.v @@ -633,7 +633,7 @@ Proof. - intro H0; case (@lt_irrefl zero). apply lt_le_trans with alpha;auto. rewrite <- H0; pattern phi0; apply phi0_elim. - intros f H1; eapply ordering_le;eauto. + intros f H1; eapply ordering_le; [ eauto |]. split. - intro H0; destruct H0 as [x H0]. generalize (@AP_phi0 alpha).
Oh, but I see that you had already pushed a few such fixes. So maybe there was just this one remaining?
Perhaps I was discouraged too early :grinning:
Should I push this fix?
yes, let’s try.
can confirm at least hydra-battles part works on
coq.dev with this change
Is this the only contrib which has been broken with this change?
No, far from it!
probably, most of them are broken at this point
See the long list of links to PRs from https://github.com/coq/coq/pull/16293
The changelog also contains some warnings about these recent
auto changes: https://coq.github.io/doc/master/refman/changes.html#tactics
Could it have been possible to give the users a choice between some
old_auto tactic and the new one? Or between
a more realistic message for projects where breaking tactics is a problem: anyone who wants stable tactic behavior is encouraged to migrate to ssreflect (+ maybe itauto)
@Pierre Castéran Sure, this kind of thing is typically achieved by providing a compatibility flag.
; auto is a fragile pattern, that's all.
sure, this was auto in isolation, but recently also
It broke or it raised a warning (saying that it would stop using
auto with * by default)?
ah, didn't we get the warning in 8.16 and then it broke on master? I don't remember exactly.
No, the warning is in master only.
According to https://coq.github.io/doc/master/refman/changes.html#tactics
Anyway, that's a change you have been asking, isn't it?
I don't know, I guess it's one solution, if I could choose I'd probably make the whole of
anyway, one problem is of course that tactic proofs are almost never organized well from the beginning, with
by and bulleting, and chaining only when it makes sense
Well, but isn't such a breaking change an opportunity to make things more robust?
FTR, addition-chains works fine with Coq dev ;-)
Btw, is ssreflect’s
=> // pattern stable?
Many of the issues I met come from the use of the patten
apply foo; auto where the application of
foo generates a bunch of sub-goals.
=> // will use
done under the hood, which was to my understanding designed by Georges as the-most-stable-tactic-possible-that-discharges-simple-goals
gaia-hydras also works :tada:
The most surprising thing to me that Gaia works fine.
But I guess I shouldn't be surprised, since it's written in SSReflect :wink:
Last updated: Jun 11 2023 at 00:30 UTC