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?
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?
FTR in this case, the log shows that coqbot received the request and deleted the branch run-coq-bug-minimizer-79991500942
as a result.
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.
Can the fact that this step in the GitHub Action failed be linked with an HTTP error code?
This endpoint is supposed to respond either "200 OK" or "400 Bad request" if it failed to parse the body.
No, that can't be it because it wouldn't delete the branch if the request had been unsuccessful.
Also, I can see the log of coqbot retrieving the access token to prepare for posting the comment.
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...
I should improve the logging!
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?
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.)
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