Jason Gross

> 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...

@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...

I think 1 is superseded by #182

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 "[❌...

> 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 fact that it commented at all shows that it received the hook. The sentence "The requested target 'analysis' could not be found among the jobs ." is only emitted...

Right, so I think it was having issues with web hooks, but I also think this is a separate issue unrelated to that issue, because it did respond to your...

How hard would it be to move the branch name generation from bash in https://github.com/coq/bot/blob/6c0433160deb6a400c42c7f33952134d604a59fe/coq_bug_minimizer.sh#L17 https://github.com/coq/bot/blob/6c0433160deb6a400c42c7f33952134d604a59fe/run_ci_minimization.sh#L24 to OCaml? I think this is my main blocker for implementing a solution to...

I think the reason I originally did this was to also not have to provide `library:` vs `plugin:`, but we should just strip these things off both the request and...

We may want to create PRs automatically without asking the user, using, e.g., a branch `auto-minimized-pr-NNNN-ci-XXXX` and a test-suite file `bug_NNNN_ci_XXXX.v`, and mention in the comment that this PR was...