Emilio Jesús Gallego Arias (Apr 22 2021 at 20:31): Emilio Jesús Gallego Arias (Apr 22 2021 at 20:31):By the way @Jason Gross @Théo Zimmermann you need to refine coqbot otherwise it will collapse with the current criterion; I rarely break the test suite, however I intend to break CI often.
Jason Gross (Apr 22 2021 at 20:37):@Emilio Jesús Gallego Arias I'm assuming you're talking about the criterion we're using to invoke the minimizer on CI failures (still a work in progress, but nearly finished). I hope that dune migration will not cause new errors in .v files? We currently only invoke the minimizer if:
File "...", line ..., characters ...:\nError:) and furthermore the filename ends in .vAnything that meets all of these criteria seems like it is almost by definition a good candidate for inclusion into the test-suite, no?
Emilio Jesús Gallego Arias (Apr 22 2021 at 20:38):I just mean I don't want the minimizer in most of my PRs, and the criterion still triggers it.
Emilio Jesús Gallego Arias (Apr 22 2021 at 20:39):The criteria doesn't work for most of my work which is actually on the infrastructure itself
Emilio Jesús Gallego Arias (Apr 22 2021 at 20:40):and destroy coqbot by adding a huge load to it
Emilio Jesús Gallego Arias (Apr 22 2021 at 20:41):Example can be seen in the Dune PR, I did a typo on some env variable, making all the CI fail [not the test suite]
Emilio Jesús Gallego Arias (Apr 22 2021 at 20:41):For gitlab that's fine, I cancel the pipeline as soon as I realize, but with this setup coqbot will be DOS by me in no time I'm afraid.
Emilio Jesús Gallego Arias (Apr 22 2021 at 20:42):Quick fix: update the criteria so the minimizer doesn't run on kind: infrastructure tags.
Gaëtan Gilbert (Apr 22 2021 at 20:42):I guess it should add "some library: job succeeded"
Gaëtan Gilbert (Apr 22 2021 at 20:43):also it would be nice if it linked the failing log it's looking at
Emilio Jesús Gallego Arias (Apr 22 2021 at 20:43):I guess I prefer having some control with tags, libraries may use different build setup so still work on infra could produce a lot of spam.
Emilio Jesús Gallego Arias (Apr 22 2021 at 20:54):For now the spam seems just too much (100s of messages per day per PR are predicted), so I'd suggest you disable this feature until the check is refined, please.
Jason Gross (Apr 22 2021 at 20:54):Is it already triggering? And can you link to the dune PR?
Jason Gross (Apr 22 2021 at 20:56):I'm still a bit confused. Are you saying that with some env var typo, coqc will fail on all CI .v files with an error message in the .v file, even though it works fine on the test-suite file? (Can you give a short example to help me understand?)
Jason Gross (Apr 22 2021 at 20:57):Quick fix: update the criteria so the minimizer doesn't run on
kind: infrastructuretags.
Sure, this seems fine to me. I'm inclined to let @Théo Zimmermann implement this, since I'm not sure how to query tags.
Jason Gross (Apr 22 2021 at 21:06):Huh, I'm confused how it's working, as when we tested things, it wasn't working.
Jason Gross (Apr 22 2021 at 21:07):Also, I unfortunately haven't figured out how to deploy new code to coqbot, and I'm not sure which is the correct state to role back to, so I think we'll have to wait for @Théo Zimmermann, unfortunately. Sorry about the spam
Emilio Jesús Gallego Arias (Apr 22 2021 at 21:35):@Jason Gross there are many ways to break CI in ways that the CI still passes and hard to test, current setup with coq_makefile is hard to test exhaustively, this is where tools like dune do better as they have a much restricted set of features to try and you get full coverage on Dune's own test suite [so then it becomes much harder to break than our current mess of spaguetti and glue]
Emilio Jesús Gallego Arias (Apr 22 2021 at 21:35):Dune PR is this one, https://github.com/coq/coq/pull/13617 , and indeed, the bot minimization triggered and caused pas mal de spam
Emilio Jesús Gallego Arias (Apr 22 2021 at 21:35):So I dunno, but I'd suggest to pause the deploy of this and make it an opt-in first
Emilio Jesús Gallego Arias (Apr 22 2021 at 21:37):Yet another example, I did set the wrong url in an overlay, this triggers the bot
Jason Gross (Apr 22 2021 at 21:38):Okay, I've rolled coqbot back to where it was yesterday, since I don't recall which of the many versions we tried today works well.
Jason Gross (Apr 22 2021 at 21:40):I'd also be fine with making it opt-in for a bit; I'll try to write up some code to make it respond to @coqbot ci minimize rather than to the checks completion, for now.
Emilio Jesús Gallego Arias (Apr 22 2021 at 22:04):Sounds great, thanks @Jason Gross ; I'll try to add some thoughts to the current criteria to see if we can automate it.
Jason Gross (Apr 22 2021 at 22:04):Awesome, thanks!
Emilio Jesús Gallego Arias (Apr 22 2021 at 22:43):Sorry for the spam by the way @Théo Zimmermann , I need to improve my chat etiquette a big deal and for example open a new topic.
Going back on topic for this thread, the PR seems to be looking very good to me (famous last words), it was a bit painful due to all the changes needed but at each iteration code seems to become more clear so I'm reasonably happy for a merge.
Notification Bot (Apr 23 2021 at 09:41):This topic was moved here from #Coq devs & plugin devs > Dune Migration by Théo Zimmermann
Théo Zimmermann (Apr 23 2021 at 09:54):Very sorry about all of this, folks. Indeed, how could I forget that infrastructure PRs should not trigger CI minimization. Thanks, Jason, for rolling back. I've rolled back to the version that was deployed from the master branch so that everything that we've fixed is there, just the new minimization feature isn't.
Emilio Jesús Gallego Arias (Apr 23 2021 at 12:03):Oh nothing to be sorry about, that's a cool but pretty complex feature it is normal we got some hiccups on deployment :) But indeed I guess you folks want to announce this more widely and maybe gather a bit more feedback from other devs? I think automatic is cool but like with everything automatic not easy
Théo Zimmermann (Apr 23 2021 at 14:28):Indeed, let's talk about it in the next Coq Call to gather additional feedback.
Théo Zimmermann (Jun 02 2021 at 07:08):There should be a way to silence coqbot or maybe it should silence itself once if it is going to post a message identical to its previous one. It can produce too much spam in PRs such as https://github.com/coq/coq/pull/13895
Jason Gross (Jun 06 2021 at 02:19):Technically there's a way to silence it by applying a label that doesn't actually exist yet on GitHub (I don't recall what I named the label, something like "skip coqbot minimization"). This might be too heavy a solution?
Théo Zimmermann (Jun 06 2021 at 07:02):Yeah OK, but it should probably also auto-silence itself in some cases if we don't want people to be too annoyed by it. I guess a solution would be checking the last 10 messages to verify that there isn't an identical message in this list. (BTW we could also do the same when posting the warning for fiat-crypto legacy.)
Théo Zimmermann (Jun 06 2021 at 07:03):Let me know if you want me to implement this!
Jason Gross (Jun 08 2021 at 23:05):I'll let you know, though I'm pretty hosed currently and, as far as coqbot work goes, am prioritizing getting minimization to work well on all the CI developments. (Currently metacoq seems to be the main one that it doesn't like.) (I guess I should also squash a bunch of commits so you can merge the PR)
Théo Zimmermann (Jun 09 2021 at 07:21):"hosed" meaning "out-of-luck"? Regarding coqbot or other things? In any case, what I mean is precisely that if it's helpful, I can take over the coqbot side of things since I have a tiny bit more time on my hands now.
Théo Zimmermann (Jun 09 2021 at 07:24):Including the squashing (if you tell me what level of granularity you want to keep). As I said, I don't have as strong expectations about clean PRs for coqbot as for Coq.
Théo Zimmermann (Jun 09 2021 at 10:15):Oh, but you've already done it!
Jason Gross (Jun 09 2021 at 13:42):Sorry, "hosed" meaning "short-on-time" (c.f. http://slugwiki.mit.edu/index.php/Hosed, I had thought it was more common-usage jargon, but I guess it's mainly MIT-jargon).
Indeed, having you take over the coqbot side of things would be great!
Last updated: Dec 07 2023 at 17:01 UTC