Stream: coqbot devs & users

Topic: ✔ Issue with coqbot not closing stale PRs today, etc.


view this post on Zulip Théo Zimmermann (Aug 25 2021 at 17:38):

Hey @Pierre-Marie Pédrot, you said that coqbot acted on too many PRs today. I suppose you were the one to trigger it and you triggered it only once. But did it actually mark more than ten PRs as stale? Or did it just say that it would close many many PRs (you didn't put any limitation on the latter).

view this post on Zulip Pierre-Marie Pédrot (Aug 25 2021 at 17:41):

I did not trigger it myself in any case.

view this post on Zulip Pierre-Marie Pédrot (Aug 25 2021 at 17:41):

but I did see a lot of notifications on modified PRs

view this post on Zulip Pierre-Marie Pédrot (Aug 25 2021 at 17:42):

mechanically this couldn't have been more than 20 (10 stale labels + 10 closures) but I think it was more in the ~30 range, and most of them were not closures anyways

view this post on Zulip Théo Zimmermann (Aug 25 2021 at 17:43):

Then the question is who triggered it (since it wasn't me and the PR to automatically trigger it every day hasn't been merged yet).

view this post on Zulip Théo Zimmermann (Aug 25 2021 at 17:47):

If someone triggers it several times, then there is nothing that prevents it to mark more than 10 PRs as stale.

view this post on Zulip Emilio Jesús Gallego Arias (Aug 25 2021 at 18:03):

I saw 50 PRs updated

view this post on Zulip Théo Zimmermann (Aug 25 2021 at 18:16):

Indeed, the logs show that someone triggered it twice in a row today.

view this post on Zulip Théo Zimmermann (Aug 25 2021 at 18:43):

OK so the reason why some PRs were not closed was because we have hit a secondary rate limit: https://docs.github.com/en/rest/overview/resources-in-the-rest-api#secondary-rate-limits

view this post on Zulip Théo Zimmermann (Aug 25 2021 at 18:46):

The solution seems to be to implement a throttle also for closing PRs and to lower the limit of PRs that can be touched in one triggering to coqbot.

view this post on Zulip Théo Zimmermann (Aug 25 2021 at 18:47):

And if needed, we could add a secret to be able to trigger the bot.

view this post on Zulip Enrico Tassi (Aug 26 2021 at 05:36):

How do you trigger it? I have no clue, I hope it cannot be done by misake

view this post on Zulip Théo Zimmermann (Aug 26 2021 at 09:44):

To trigger it, you need to do a specific curl request (see the PR adding a GitHub Action to trigger it every day).

view this post on Zulip Théo Zimmermann (Aug 26 2021 at 09:44):

I'd say it is impossible to do by mistake.

view this post on Zulip Pierre-Marie Pédrot (Aug 26 2021 at 09:59):

Who's been triggering it on a daily basis these days? I've not. Is that you @Théo Zimmermann ?

view this post on Zulip Théo Zimmermann (Aug 26 2021 at 10:00):

Yes, but only on days when I was not on vacations, i.e. not in the last few days.

view this post on Zulip Pierre-Marie Pédrot (Aug 26 2021 at 10:00):

Maybe Google or some bot accessed the URL while crawling?

view this post on Zulip Théo Zimmermann (Aug 26 2021 at 10:00):

You can't trigger it with a simple GET request, you need a POST request with coq:coq as the body.

view this post on Zulip Pierre-Marie Pédrot (Aug 26 2021 at 10:00):

Right.

view this post on Zulip Pierre-Marie Pédrot (Aug 26 2021 at 10:00):

The plot thickens.

view this post on Zulip Pierre-Marie Pédrot (Aug 26 2021 at 10:01):

You obviously don't have the IP of the client in the logs either?

view this post on Zulip Pierre-Marie Pédrot (Aug 26 2021 at 10:02):

Maybe some three-letter agency that thought that Coq was critical for their plans and things were not going as fast as possible...

view this post on Zulip Enrico Tassi (Aug 26 2021 at 10:03):

all your PRs are mine

view this post on Zulip Théo Zimmermann (Aug 26 2021 at 10:11):

Pierre-Marie Pédrot said:

You obviously don't have the IP of the client in the logs either?

Actually, I have. The request came from Mougins, Alpes-Maritimes. I guess that's Inria Sophia then.

view this post on Zulip Théo Zimmermann (Aug 26 2021 at 10:12):

Also, it started with a GET request (something that I had overlooked yesterday), which was therefore ill-formed.

view this post on Zulip Théo Zimmermann (Aug 26 2021 at 10:13):

It followed by a request to /favicon, which is a 404.

view this post on Zulip Théo Zimmermann (Aug 26 2021 at 10:13):

And only then a well-formed POST request.

view this post on Zulip Théo Zimmermann (Aug 26 2021 at 10:15):

And contrary to what I said earlier, there was only one POST request, so this doesn't explain why it marked more than 10 PRs as stale.

view this post on Zulip Théo Zimmermann (Aug 26 2021 at 10:29):

So what really happened is that the bot was triggered only once (which is OK then), but this had the following consequence:

view this post on Zulip Théo Zimmermann (Aug 26 2021 at 12:16):

Fixed (limit is now at 6 new stale PRs and 4 closed PRs).

view this post on Zulip Notification Bot (Aug 26 2021 at 12:16):

Théo Zimmermann has marked this topic as resolved.

view this post on Zulip Enrico Tassi (Aug 26 2021 at 12:17):

Mugins could be me or Laurence. But are you saying this is a bug and the log entry you mentioned was somehting else?

view this post on Zulip Enrico Tassi (Aug 26 2021 at 12:18):

I could have clicked on any GH button by mistake, but I did not do a curl request for sure

view this post on Zulip Enrico Tassi (Aug 26 2021 at 12:18):

So, if there is a silly request from my IP address, there must be a link to it from GH. (I did re-run a few CI jobs for example using the bot links)

view this post on Zulip Théo Zimmermann (Aug 26 2021 at 12:22):

Enrico Tassi said:

Mugins could be me or Laurence. But are you saying this is a bug and the log entry you mentioned was somehting else?

I can give you the exact IP address if you want to check if it's yours.

view this post on Zulip Théo Zimmermann (Aug 26 2021 at 12:23):

Who is Laurence?

view this post on Zulip Enrico Tassi (Aug 26 2021 at 14:07):

Laurence Rideau, not runnig curl by hand either


Last updated: Jan 31 2023 at 09:01 UTC