Stream: coqbot devs & users

Topic: coqbot services


view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip Janno (May 29 2020 at 08:08):

That sounds amazing! As author of PRs that will inevitably spawn bug reports I definitely want this! :)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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:

  1. A user makes a comment like @coqbot minimize: script to run to get the error
  2. 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:

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?

view this post on Zulip Théo Zimmermann (Jun 01 2020 at 08:06):

Yes

view this post on Zulip 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.

view this post on Zulip Notification Bot (Jun 12 2020 at 11:40):

This topic was moved here from #Coq devs & plugin devs > coqbot services by Théo Zimmermann

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Julien Coolen (Jul 14 2020 at 17:56):

Thanks! Indeed, this simplifies the parsing of the requests server side.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).)

view this post on Zulip Théo Zimmermann (Jul 19 2020 at 18:15):

I don't know either, but yes, it'd be definitely worth.

view this post on Zulip Jason Gross (Jul 21 2020 at 18:12):

What's the procedure for moving a repo to coq-community?


Last updated: May 28 2023 at 16:30 UTC