Stream: coqbot devs & users

Topic: Failing to respond

view this post on Zulip Jason Gross (Apr 12 2021 at 21:21):

I believe I messaged coqbot at 2021-04-07T21:50:17.0776865Z via curl (see https://github.com/coq-community/run-coq-bug-minimizer/runs/2289409730?check_suite_focus=true#step:5:33390 ; curl -X POST --data-binary @/tmp/tmp.scpn6rfvNd https://coqbot.herokuapp.com/coq-bug-minimizer). I believe the request started with

MDU6SXNzdWU4MzM4Njc1ODY= JasonGross coq-community/run-coq-bug-minimizer run-coq-bug-minimizer-79991500942 coq-community run-coq-bug-minimizer

But coqbot does not seem to have replied on the relevant issue at https://github.com/coq-community/run-coq-bug-minimizer/issues/5

How do I diagnose what's going on here?

view this post on Zulip Théo Zimmermann (Apr 13 2021 at 09:00):

Hey Jason, I'll look into this. But I think it would help if I gave you access to Heroku so that you can check the logs by yourself. What would be your availabilities to schedule a call together?

view this post on Zulip Théo Zimmermann (Apr 13 2021 at 09:05):

FTR in this case, the log shows that coqbot received the request and deleted the branch run-coq-bug-minimizer-79991500942 as a result.

view this post on Zulip Théo Zimmermann (Apr 13 2021 at 09:08):

Actually the request was at the URL /coq-bug-minimizer not /run-coq-bug-minimizer (which doesn't exist as an endpoint), but this is irrelevant I think.

view this post on Zulip Théo Zimmermann (Apr 13 2021 at 09:17):

Can the fact that this step in the GitHub Action failed be linked with an HTTP error code?

view this post on Zulip Théo Zimmermann (Apr 13 2021 at 09:18):

This endpoint is supposed to respond either "200 OK" or "400 Bad request" if it failed to parse the body.

view this post on Zulip Théo Zimmermann (Apr 13 2021 at 09:19):

No, that can't be it because it wouldn't delete the branch if the request had been unsuccessful.

view this post on Zulip Théo Zimmermann (Apr 13 2021 at 09:27):

Also, I can see the log of coqbot retrieving the access token to prepare for posting the comment.

view this post on Zulip Théo Zimmermann (Apr 13 2021 at 09:30):

So the comment should have been posted. And I cannot see an error in the log, so this should mean that the request was successful...

view this post on Zulip Théo Zimmermann (Apr 13 2021 at 09:56):

I should improve the logging!

view this post on Zulip Jason Gross (Apr 13 2021 at 13:10):

If the URL endpoint is supposed to be /run-coq-bug-minimizer and not /coq-bug-minimizer, then https://github.com/coq/bot/blob/90f0b8f7b5ef984291b13a691b9351341c2fc0d8/coq_bug_minimizer.sh#L30 should be updated (the url comes from the bot itself).

Indeed, the branch was deleted. Maybe the log should include a link to the comment after posting it?

view this post on Zulip Jason Gross (Apr 13 2021 at 13:12):

But I think it would help if I gave you access to Heroku so that you can check the logs by yourself. What would be your availabilities to schedule a call together?

Sure! If you're still around @Théo Zimmermann , I'm free for a call for the next couple of hours. I'm also free tomorrow for the hour before the weekly Coq calls, and most mornings starting at around 9am EST / 3pm Paris time (though not this Friday). (I'm assuming that you're in Paris time; if you're in a different timezone, I'm also free later in the day (EST) some days.)

view this post on Zulip Théo Zimmermann (Apr 13 2021 at 13:16):

Jason Gross said:

If the URL endpoint is supposed to be /run-coq-bug-minimizer and not /coq-bug-minimizer, then https://github.com/coq/bot/blob/90f0b8f7b5ef984291b13a691b9351341c2fc0d8/coq_bug_minimizer.sh#L30 should be updated (the url comes from the bot itself).

Indeed, the branch was deleted. Maybe the log should include a link to the comment after posting it?

No, it's supposed to be /coq-bug-minimizer.

Last updated: Sep 26 2023 at 13:01 UTC