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.
(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.)
That sounds amazing! As author of PRs that will inevitably spawn bug reports I definitely want this! :)
Jason Gross said:
automatically extract the buggy file name from a log of running
I guess this piece of info can be provided by the user no?
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.
@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
This is the place where to listen for a comment addressed to @coqbot: https://github.com/coq/bot/blob/2b75281e4035ef3cd0feeb370fbce2142de0e216/bot.ml#L778-L785
You should then be able to prepare the PR branch thanks to
git_push and inspired by
If you give permission to the bot to push to your repo, this should avoid the need to create a fork.
@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 error
coqbot 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-stampthat can be used to identify which thread to respond on once minimization is done
reply-coqbot.shwhich 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.shwhich 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 Thanks! Let me know if you want me to try to code up some part of it.
This topic was moved here from #Coq devs & plugin devs > coqbot services by Théo Zimmermann
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-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?
@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
@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-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
Thanks! Indeed, this simplifies the parsing of the requests server side.
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
run.sh might cause this. What do you think?
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.
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.
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).)
I don't know either, but yes, it'd be definitely worth.
What's the procedure for moving a repo to coq-community?
Last updated: May 28 2023 at 16:30 UTC