Pierre Castéran (Oct 01 2022 at 09:18): Pierre Castéran (Oct 01 2022 at 09:18):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.
Théo Zimmermann (Oct 01 2022 at 09:29):auto has indeed recently become more powerful
Théo Zimmermann (Oct 01 2022 at 09:30):A way of fixing this which is backward compatible is to do some explicit goal management (avoid ; auto and ; trivial).
Karl Palmskog (Oct 01 2022 at 11:00):@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.
Pierre Castéran (Oct 01 2022 at 12:14):Ok, It will take some time ...
Karl Palmskog (Oct 01 2022 at 12:15):OK, then I'll merge this one in the meantime: https://github.com/coq-community/goedel/pull/15
Pierre Castéran (Oct 01 2022 at 13:30):It represents days (weeks?) of work. This, plus the 8.16 changes. Discouraging ...
Théo Zimmermann (Oct 01 2022 at 13:36):Fixing the auto problems?
Pierre Castéran (Oct 01 2022 at 13:45):yes :sad:
> grep auto theories/ordinals/*/*.v | wc -l
5018
> grep trivial theories/ordinals/*/*.v | wc -l
1071
Let me try. Which branch should I use? master?
Pierre Castéran (Oct 01 2022 at 15:12):Yes, it’s on master. For the time being, I just looked at 3 files: Addition, Iterates and partially AP. I believe the autos at the end of a bullet are OK. There were also issues with several … too.
Karl Palmskog (Oct 01 2022 at 15:14):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)
Théo Zimmermann (Oct 01 2022 at 15:16):Hum, this is weird. I did a single fix and the whole of hydra-battles compiles:
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?
Pierre Castéran (Oct 01 2022 at 15:22):Thanks!
Perhaps I was discouraged too early :grinning:
Théo Zimmermann (Oct 01 2022 at 15:23):Should I push this fix?
Pierre Castéran (Oct 01 2022 at 15:24):yes, let’s try.
Karl Palmskog (Oct 01 2022 at 15:24):can confirm at least hydra-battles part works on coq.dev with this change
Pierre Castéran (Oct 01 2022 at 15:26):Is this the only contrib which has been broken with this change?
Théo Zimmermann (Oct 01 2022 at 15:26):No, far from it!
Karl Palmskog (Oct 01 2022 at 15:27):probably, most of them are broken at this point
Théo Zimmermann (Oct 01 2022 at 15:27):See the long list of links to PRs from https://github.com/coq/coq/pull/16293
Théo Zimmermann (Oct 01 2022 at 15:28):The changelog also contains some warnings about these recent auto changes: https://coq.github.io/doc/master/refman/changes.html#tactics
Pierre Castéran (Oct 01 2022 at 15:30):Could it have been possible to give the users a choice between some old_auto tactic and the new one? Or between auto and smart_auto ?
Karl Palmskog (Oct 01 2022 at 15:32):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)
Théo Zimmermann (Oct 01 2022 at 15:33):@Pierre Castéran Sure, this kind of thing is typically achieved by providing a compatibility flag.
Théo Zimmermann (Oct 01 2022 at 15:33):@Karl Palmskog ; auto is a fragile pattern, that's all.
Karl Palmskog (Oct 01 2022 at 15:34):sure, this was auto in isolation, but recently also intuition. broke
Théo Zimmermann (Oct 01 2022 at 15:35):It broke or it raised a warning (saying that it would stop using auto with * by default)?
Karl Palmskog (Oct 01 2022 at 15:37):ah, didn't we get the warning in 8.16 and then it broke on master? I don't remember exactly.
Théo Zimmermann (Oct 01 2022 at 15:37):No, the warning is in master only.
Théo Zimmermann (Oct 01 2022 at 15:38):According to https://coq.github.io/doc/master/refman/changes.html#tactics
Théo Zimmermann (Oct 01 2022 at 15:38):Anyway, that's a change you have been asking, isn't it?
Karl Palmskog (Oct 01 2022 at 15:39):I don't know, I guess it's one solution, if I could choose I'd probably make the whole of intuition deprecated
Karl Palmskog (Oct 01 2022 at 15:43):anyway, one problem is of course that tactic proofs are almost never organized well from the beginning, with solve or by and bulleting, and chaining only when it makes sense
Théo Zimmermann (Oct 01 2022 at 15:45):Well, but isn't such a breaking change an opportunity to make things more robust?
Théo Zimmermann (Oct 01 2022 at 15:48):FTR, addition-chains works fine with Coq dev ;-)
Pierre Castéran (Oct 01 2022 at 15:52):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.
Karl Palmskog (Oct 01 2022 at 15:53):=> // will use done under the hood, which was to my understanding designed by Georges as the-most-stable-tactic-possible-that-discharges-simple-goals
Théo Zimmermann (Oct 01 2022 at 15:55):gaia-hydras also works :tada:
Théo Zimmermann (Oct 01 2022 at 15:55):The most surprising thing to me that Gaia works fine.
Théo Zimmermann (Oct 01 2022 at 15:55):But I guess I shouldn't be surprised, since it's written in SSReflect :wink:
Last updated: Apr 19 2024 at 05:01 UTC