Jason Gross (May 28 2020 at 23:57): Jason Gross (May 28 2020 at 23:57):Would it be useful to have @coqbot set up so that someone could comment on an Issue @coqbot minimize: or something, followed by a script that displays the error message, and have my bug minimizer minimize it, and have @coqbot reply back with a minimized version? My minimizer is pretty close to being able to support this; all that's left, basically, is setting it up to automatically extract the buggy file name from a log of running make. Otherwise it currently can run automatically on https://github.com/JasonGross/run-coq-bug-minimizer/blob/master/run.sh and will run a minimization on GH actions if you, e.g., submit a PR to the repo modifying the run script. It shouldn't be too hard to extend it to make the interaction fully asynchronous.
Jason Gross (May 28 2020 at 23:58):(Note that I used this to minimize a test-case for https://github.com/coq/coq/pull/12422, without ever having to run the code on my machine.)
Janno (May 29 2020 at 08:08):That sounds amazing! As author of PRs that will inevitably spawn bug reports I definitely want this! :)
Enrico Tassi (May 29 2020 at 08:22):Jason Gross said:
automatically extract the buggy file name from a log of running
make.
I guess this piece of info can be provided by the user no?
Théo Zimmermann (May 29 2020 at 09:30):Great! That sound like a pretty easy thing to do from the @coqbot perspective (just open a PR with the provided content). The infrastructure for reading messages addressed to @coqbot is already in place BTW, even if it isn't used yet.
Jason Gross (May 31 2020 at 02:33):@Enrico Tassi Yes, probably, but I think it might be a bit easier if the user just has to give a script showing the error. I've now set up my repo so that it should be able to run automatically just by submitting a PR with the script in a given file, now I just need to set up some interaction with coqbot, I believe
Théo Zimmermann (May 31 2020 at 15:10):This is the place where to listen for a comment addressed to @coqbot: https://github.com/coq/bot/blob/2b75281e4035ef3cd0feeb370fbce2142de0e216/bot.ml#L778-L785
Théo Zimmermann (May 31 2020 at 15:13):You should then be able to prepare the PR branch thanks to git_fetch, git_push and inspired by git_make_ancestor.
Théo Zimmermann (May 31 2020 at 15:14):If you give permission to the bot to push to your repo, this should avoid the need to create a fork.
Jason Gross (May 31 2020 at 23:32):@Théo Zimmermann I believe I've added the necessary infrastructure to https://github.com/JasonGross/run-coq-bug-minimizer to support integration with coqbot. I've invited coqbot to collaborate on the repo. The workflow should be as follows:
@coqbot minimize: script to run to get the errorcoqbot extracts the script, ideally removing any block quotations, triple backticks, etc, surrounding the script, and pushes a commit to any branch on https://github.com/JasonGross/run-coq-bug-minimizer with the following:
coqbot-request-stamp that can be used to identify which thread to respond on once minimization is donecoqbot.shreply-coqbot.sh which is to be invoked with 5 arguments: the contents of coqbot-request-stamp, the name of the file that was identified as buggy (path should not be assumed to exist), the absolute path to the minimized file, the absolute path to the initial build log (useful for the user to check to see if the error found was the correct one), and the absolute path to the log of the minimizer run (possibly useful for debugging); this script will presumably be some curl invocation, and can possibly be set once on master and thereafter not touched.reply-coqbot-error.sh which is to be invoked when we can't figure out what file to minimize, which gets three arguments: the contents of coqbot-request-stamp, the (possibly empty) name of the file that was identified as buggy (path should not be assumed to exist), and the absolute path to the build log (which can then be used for debugging). This script can also probably be set once on master and thereafter not touched.Currently these last two scripts contain echo curl commands which were my stab at an approximate invocation that should work (though there's no URL).
Presumably coqbot should reply to the relevant thread with something like:
Minimization of $FILE succeeded with [a minimization log](link to uploaded file of the minimization log).
<details><summary>Build Log</summary>
```
$CONTENTS_OF_BUILD_LOG
```
</details>
<details><summary>Minimized File</summary>
```
$CONTENTS_OF_MINIMIZED_FILE
```
</details>
or else a similar message on error. You could also probably link to https://github.com/JasonGross/run-coq-bug-minimizer/actions/runs/$GITHUB_RUN_ID to instruct the user to get more details.
@Théo Zimmermann Would you (or someone else) be willing to write the coqbot-side infrastructure for this interaction?
Théo Zimmermann (Jun 01 2020 at 08:06):Yes
Jason Gross (Jun 01 2020 at 18:07):@Théo Zimmermann Thanks! Let me know if you want me to try to code up some part of it.
Notification Bot (Jun 12 2020 at 11:40):This topic was moved here from #Coq devs & plugin devs > coqbot services by Théo Zimmermann
Julien Coolen (Jul 14 2020 at 13:20):Hello @Jason Gross, I'm writing the server-side code to make use of your minimizer. So far coqbot extracts the script surrounded by triple quotes from a comment beginning with "@coqbot: minimize" (see https://github.com/coqbot-dev/run-coq-bug-minimizer/pull/1#issuecomment-658187622), then pushes the script to a new branch in your repo (https://github.com/coqbot-dev/run-coq-bug-minimizer/tree/coq-bug-minimizer-42792261241).
Now I'm tackling the task of replying back with the output of your minimizer. Are the scripts reply_coqbot.sh and reply-coqbot-error.sh meant to be executed as part of your github action (to send the output of the minimizer to coqbot)? How should we proceed?
Jason Gross (Jul 14 2020 at 15:44):@Julien Coolen great! Yes, if you look at https://github.com/coqbot-dev/run-coq-bug-minimizer/blob/master/run.sh, you'll see how they are invoked by the GitHub action. You can either submit a pull request with the desired content for those scripts (the relevant curl commands or whatever), or you can update them on each push
Jason Gross (Jul 14 2020 at 17:38):@Julien Coolen I've just pushed a commit at https://github.com/JasonGross/run-coq-bug-minimizer (https://github.com/JasonGross/run-coq-bug-minimizer/commit/5780d7a5964f3a61a9409b3a0a69b1915f4033e5) so that if you set COQBOT_URL in coqbot-config.sh to a url, then the actions script will post a request to that url with the id followed by a newline followed by the body of a comment to post at that id. You should feel free to revert this commit if you want a different mode of interaction, but I figured having just a single url for "post a new comment here" might be the simplest thing
Julien Coolen (Jul 14 2020 at 17:56):Thanks! Indeed, this simplifies the parsing of the requests server side.
Julien Coolen (Jul 15 2020 at 15:56):Coqbot receives two consecutive POST requests each time the github action finishes. This makes coqbot reply with two consecutive messages. @Théo Zimmermann suggested that the call to trap in run.sh might cause this. What do you think?
Jason Gross (Jul 15 2020 at 21:33):Ah, indeed, that seems to be the case. I've left the trap (I want it to still trigger if we fail earlier on and exit) and removed the call to cleanup at the end.
Julien Coolen (Jul 16 2020 at 11:35):Thanks! It's working perfectly (here is an example: https://github.com/coqbot-dev/test/issues/6#issuecomment-659331891). I'm going to make a PR to coqbot shortly with this feature.
Jason Gross (Jul 18 2020 at 21:41):Would it make sense to move https://github.com/JasonGross/run-coq-bug-minimizer to coq-community? (I'm a bit worried that if it gets too popular, it'll backlog all of my personal GH Actions runs, since I think GH Actions runners are shared across all repos owned by a user (not sure how it works for organizations).)
Théo Zimmermann (Jul 19 2020 at 18:15):I don't know either, but yes, it'd be definitely worth.
Jason Gross (Jul 21 2020 at 18:12):What's the procedure for moving a repo to coq-community?
Last updated: Dec 01 2023 at 04:01 UTC