Stream: coqbot devs & users

Topic: Bad Request


view this post on Zulip Jason Gross (Oct 31 2021 at 21:08):

How do I debug coqbot responding with "bad request"?

curl -X POST --data-binary @/tmp/tmp.hirbUs9jkn https://coqbot.herokuapp.com/coq-bug-minimizer
    % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                   Dload  Upload   Total   Spent    Left  Speed

    0     0    0     0    0     0      0      0 --:--:-- --:--:-- --:--:--     0
    0     0    0     0    0     0      0      0 --:--:-- --:--:-- --:--:--     0
  100 30322    0     0  100 30322      0  24199  0:00:01  0:00:01 --:--:-- 24180
  100 30322    0     0  100 30322      0  13446  0:00:02  0:00:02 --:--:-- 13440
  100 30322    0     0  100 30322      0   9312  0:00:03  0:00:03 --:--:--  9309
  100 30322    0     0  100 30322      0   7122  0:00:04  0:00:04 --:--:--  7121
  100 30333  100    11  100 30322      2   6645  0:00:05  0:00:04  0:00:01  7013
  Bad request

https://github.com/coq-community/run-coq-bug-minimizer/runs/4057998503?check_suite_focus=true#step:5:10656

I can't find anything in the herokuapp logs.

view this post on Zulip Théo Zimmermann (Nov 01 2021 at 09:37):

This happens if the body cannot be parsed with the following code: https://github.com/coq/bot/blob/2879bc6269bb49c0eda05ca0208cc13812162e03/src/actions.ml#L1549-L1553

view this post on Zulip Théo Zimmermann (Nov 01 2021 at 09:37):

The most likely explanation is that this is an unwanted consequence of https://github.com/coq/bot/commit/074d40282c0840e02265dd6713887423d1d20910.


Last updated: Jan 31 2023 at 10:01 UTC