bot
bot copied to clipboard
coq
CI minimization responses should allow easy creation of PRs augmenting the test-suite
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 file to the test-suite.". This link could target an endpoint of coqbot with a GET request containing a link to the workflow run, the CI target, and some information about the PR (to be provided by coqbot, so that it can find the right branch, repo, etc). Coqbot could then fork the repo (or use a predetermined fork), download the artifact, unpack bug.v, make a branch called pr-branch-name+ci-target+uid which adds bug.v as test-suite/success/pr#_ci_target.v, and then creates a PR against the original PR branch, mentioning the issue comment or something. Perhaps it can then also reply to the issue stating that it created the PR. Alternatively, it could send a redirect to the endpoint webpage so clicking on the endpoint link gets you a "creating PR" page that does some sort of poll or long-lived response that eventually gets redirected to the newly-created PR.
Thoughts?
Until we implement user authentication (allowing the bot to act on behalf of a user), which would also be useful for the @coqbot merge now feature, we will have no choice but to create the commit adding the test-suite file on a branch that @coqbot has access to. This could be a coqbot-owned fork or a fork that we would host elsewhere (as long as we give it access).
Then, the PR can either be created by coqbot itself or by the user (anyone can create a pull request from any branch on a public fork). The only issue with the latter is that the user then cannot give write-access to the maintainers to the branch of the pull request. This can be solved by using a fork that would be owned in the Coq organization itself and where all the @coq/contributors team would have write access (although putting a fork of Coq inside the Coq organization is not trivial, maybe this can be achieved by forking elsewhere and doing a repository renaming + a repository transfer).
FWIW, GitHub plans to add support for forking a repository in the organization of its parent in Q2 2022: https://github.com/github/roadmap/issues/330
Note that the initial proposal that was recorded in #147 (to push a commit adding the test case to the test-suite in the PR where the minimizer was triggered) did not have the problems discussed here.
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 created / link to it. We should only do this when the file is fully minimized (#188) and we should make sure not to create a PR with a truncated file (which can be determined by the "truncated to SIZE" parenthetical in the comment). If the branch/PR already exists, we should overwrite the file and just push an update with the possibly-further-minimized file.
We may want to remove the suggestion to use 🚀 in this case, or just replace that suggestion with a link to the PR that was auto-created.