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.
@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 .v
Anything that meets all of these criteria seems like it is almost by definition a good candidate for inclusion into the test-suite, no?
I just mean I don't want the minimizer in most of my PRs, and the criterion still triggers it.
The criteria doesn't work for most of my work which is actually on the infrastructure itself
and destroy coqbot by adding a huge load to it
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]
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.
Quick fix: update the criteria so the minimizer doesn't run on kind: infrastructure
tags.
I guess it should add "some library: job succeeded"
also it would be nice if it linked the failing log it's looking at
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.
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.
Is it already triggering? And can you link to the dune PR?
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?)
Quick fix: update the criteria so the minimizer doesn't run on
kind: infrastructure
tags.
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.
Huh, I'm confused how it's working, as when we tested things, it wasn't working.
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
@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]
Dune PR is this one, https://github.com/coq/coq/pull/13617 , and indeed, the bot minimization triggered and caused pas mal de spam
So I dunno, but I'd suggest to pause the deploy of this and make it an opt-in first
Yet another example, I did set the wrong url in an overlay, this triggers the bot
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.
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.
Sounds great, thanks @Jason Gross ; I'll try to add some thoughts to the current criteria to see if we can automate it.
Awesome, thanks!
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.
This topic was moved here from #Coq devs & plugin devs > Dune Migration by Théo Zimmermann
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.
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
Indeed, let's talk about it in the next Coq Call to gather additional feedback.
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
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?
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.)
Let me know if you want me to implement this!
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)
"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.
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.
Oh, but you've already done it!
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: May 28 2023 at 18:29 UTC