coq
Minimizer should report less when continuing minimization
See https://github.com/coq/coq/pull/15693#issuecomment-1075206602
The minimizer should not spam the almost minimized files and instead wait for the user to ask about the status. We could have @coqbot check minimization or something to get a partially minimized file.
cc @JasonGross
Ah, I should have written my answer here:
Another option would be to use the check run tab to store more detailed information about the minimization, including this kind of things.
Alternatively the bot could edit the existing comment every time minimization makes progress, and if/when it finally terminates, delete the old comment and post a new one (so that we do get a notification that minimization completed)
Would that require remembering the last comment? Or would we have to look for it every time?
Either of the two options (remembering the comment ID can be done through the information that we pass to the minimizer infrastructure as a "stamp"). Looking for the comment is what we do when we get a request to merge a PR (so that we check that it was not created by email).
Why not just link to the action? It has the full file in the artifacts. eg
"Minimization interrupted by timeout, being automatically continued. Current results at https://github.com/coq-community/run-coq-bug-minimizer/actions/runs/7572077026"
GHA logs and artifacts are deleted after a month or so, and I want to be able to dig into the archives in case minimization is interrupted before being completed. But I've made it so that everything is now wrapped in a single <details> block in https://github.com/coq-community/run-coq-bug-minimizer/commit/f24447ddbf50861c0b4d5eee27049c21bedd3ccd, so the messages should at least be way shorter when collapsed.