bot
bot copied to clipboard
coq
Improve auto-minimization resumption (and give option to stop it).
- instead of posting a new comment for each new run, coqbot could edit the previous comment
- coqbot could give an option to the user to stop the minimization.
In https://github.com/coq/coq/pull/14748#issuecomment-955371910, I've noticed an issue where resumption did not produce a shorter file and thus was running in an infinite loop. This seems to have happened before. If we were to implement point 1, we could check that the new minimization output is actually different from the previous one before automatically resuming the minimization.
I've noticed an issue where resumption did not produce a shorter file and thus was running in an infinite loop.
This is a bug in the minimizer itself that I need to debug. It's not supposed to happen.
Right, but even if this instance is fixed, it could happen again with another bug, and then this defensive strategy would help to be robust against such bugs. One suggestion that was recently made to me while I was giving a talk about the bot is that the bot itself could open an issue when it detects an unexpected behavior!
@Zimmi48 Ah, the issue here is that it takes more than 6 hours to discover that there's nothing to be done without inlining more files :-( (The file being minimized takes about 22 seconds to run, and hence we spend about 45 seconds testing every change. Hence we have time to test fewer than 500 changes, and I guess that's just not enough to make forward progress. Not sure what to do here, but indeed we could have the bot open an issue about this when it detects a loop. (Note that it can't just check for textual equality, and needs to strip out Coq comments first, because the header of the file recording the minimization progress will keep growing.)
If the minimizer gets access to the UID and the ci name, and include this info in the branch name, we can insert a comment with a link like "❌ Cancel minimization" which asks the bot to search for running workflows with the uid and ci name in the branch name and cancel the run and delete the branch.
In fact, as soon as coqbot composes the comment and retriggers minimization itself, we could simply do the triggering before posting the comment, get the workflow ID, and include it in the bot endpoint to cancel minimization.
we could simply do the triggering before posting the comment, get the workflow ID, and include it in the bot endpoint to cancel minimization.
It takes some time before the workflow id is assigned, right? Either we need to do some sort of backoff computation, or else we need to listen to workflow run start events and include enough information in the commit message / branch to find the previous iteration that we're supposed to be commenting about
You are right. I was hoping that one could trigger a workflow through the GraphQL API, in which case we might have got a workflow ID as a reply, but this is not supported yet.