Jason Gross
Jason Gross
In addition to posting comments, and perhaps even when the test-suite fails, each failure in the checks tab ([example](https://github.com/coq/coq/pull/15341/checks?check_run_id=4494061751)) could get a line that says something like "🚀 Click [here](#)...
It might be nice to have a link in the "here's the minimized file" comment for "Click here to have coqbot create a PR against this PR branch adding this...
Currently it's "latest released", and there's no good way to configure it when invoking the minimizer. Perhaps it should be configurable?
When checks finish at the head of a branch in Coq, all open PR with a CI failure on ci-XXX which also fails on the CI of the base commit,...
Currently when a user initiates (non-ci) minimization, the commit message is just "Added user script in coqbot.sh". It should be something like "Added user script from coq/coq# in coqbot.sh" and...
Probably by commenting on https://github.com/coq-community/run-coq-bug-minimizer/issues/8, or editing a comment there, with some log of uses. Possible data that's useful to track: - PRs that minimization was possible on - PRs...
I was reading up on delta debugging and found that one use case is to find the minimal set of changes in a diff that can be removed to restore...
This might make it easier to know whether the issue is a problem with coqbot seeing the comment at all vs coqbot parsing the comment. (This idea came up after...
Sometimes I run `dev/tools/make-changelog` before actually creating the PR, and thus can get the number wrong. It would be nice if coqbot warned me if the PR number was not...