Add "closed-pr" emoji in Zulip?

Stream: PR reviews

[Robert Maxton]

For some reason, #23992 is failing CI because, of all things, it can't add a "closed-pr" emoji in Zulip somewhere? I am very confused and looking at the detailed log doesn't much clarify things.

[Bryan Gin-ge Chen]

I suspect we may be hitting some kind of API limit. Let me ping @Damiano Testa who may be able to give a quicker answer.

For now I would say you can ignore that particular red x. That job isn't required to succeed for us to merge your PR anyways.

[Robert Maxton]

Mmk. So long as it gets into the review queue -- I've got a backlog ^.^;

[Damiano Testa]

I agree with Bryan's assessment: the failure is likely due to hitting an API limit (or maybe just some other random transient issue).

As for it being included in the queue, let me then delegate to @Michael Rothgang since he might know!

[Ruben Van de Velde]

You can check #queueboard to see if it's on the queue

[Ruben Van de Velde]

But we all have a backlog, I'm afraid :)

[Robert Maxton]

Alas
At any rate, I already checked the queue board, it's being held up by CI, which presumably means this specific word thing
I'll try just re-running CI tho

[Michael Rothgang]

I just verified: the queue includes all PRs whose CI passes. CI failing (for any reason, including network errors, or a non-essential workflow like this one) means a PR is not on the queue.

[Michael Rothgang]

Re-running sounds reasonable

[Michael Rothgang]

One could try to change the definition of "queue" to take this into account. For the github-search based qeueue, that will be difficult - for the queueboard, that's not hard.

[Michael Rothgang]

The queueboard already has a notion of "inessential CI jobs which fail". (It was missing this one workflow, which I just added - thanks for making me look!) One could have a bot which looks "are there any such PRs" and posts on zulip, so people could take a look quickly.

[Robert Maxton]

... Mm. Nope, it fails even on rerunning.

[Michael Rothgang]

The error says something about "malformed API key". That doesn't look like a network failure; if it's a rate limit, the error is extremely bad.

[Michael Rothgang]

Update. The PR now appears on this dashboard

[Damiano Testa]

I think that this is an error that other times I interpreted as API limits.

[Damiano Testa]

However, this action is hard to re-run, since I am not sure that clicking on "re-run job" actually does anything.

[Robert Maxton]

Michael Rothgang said:

Update. The PR now appears on this dashboard

I'll take it! (Though if anyone finds something I can do to fix it properly, please let me know!)

[Robert Maxton]

Damiano Testa said:

However, this action is hard to re-run, since I am not sure that clicking on "re-run job" actually does anything.

Would rerunning all jobs change anything?

[Damiano Testa]

This should be the list of all the times that this script ran. I had "re-run" it earlier, but it does not appear in the list above.

[Damiano Testa]

Robert Maxton said:

Damiano Testa said:

However, this action is hard to re-run, since I am not sure that clicking on "re-run job" actually does anything.

Would rerunning all jobs change anything?

I am not sure, since this job runs only when a PR is closed or reopened. In fact, I am not sure why it even triggered on your PR.

[Robert Maxton]

.... Ah. I think this might have been one of the PRs I accidentally first contributed to my own fork and attempted to merge from there.
Or, at least, maybe it shared a branch name with such a PR? I've been using robertmaxton/quiv-helpersN in order, so it's possible I reused a number when I thought a previous PR had been canceled/closed

[Robert Maxton]

I shall endeavor not to do do so in the future :wry:

[Damiano Testa]

That may explain why the action tried to run in the first place. Maybe then the API failure could be that the token it used came from your fork, which is not the one that the mathlib CI was expecting.

[Damiano Testa]

This would make the error message be more pertinent as well. It all seems to line up!

[Robert Maxton]

Mm, maybe. If that's the case it needs to have somehow remembered the wrong token even after I closed and reopened the PR properly -- the CI doesn't actually support merges from forks
If there's a mechanism for that, then yeah, it lines up.

[Damiano Testa]

It is always hard to fully understand CI, but the "troubled history" of this PR is a likely explanation for why things are failing. Very likely, it would be possible to catch these issues and be more graceful about them, but I would not really know how to do that...

[Robert Maxton]

nodnod Fair enough, then

[Damiano Testa]

Besides, I think that getting some mechanism on the #queueboard to list the PRs for which the "relevant" CI checks are successful is definitely a good outcome!

[Damiano Testa]

This means that the error emitted by the emoji script is noticed, can be reviewed, but the PR is still "where it needs to be" in terms of reviewing.

[Damiano Testa]

The review can be, as in this case, "let it go"! :smile:

[Michael Rothgang]

Let me repeat to ensure I understood correctly: you're proposing to change the definition of the queueboard queue, from "CI passes" to "CI passes or there are only inessential failures", right?

[Damiano Testa]

Well, already your "spurious job failure" is a good place! In fact, if this PR were to be merged, I think that bors would ignore this failure: it will do its checks and would not look at the fact that this job failed.

[Michael Rothgang]

Ah, ok! So the only thing that might be missing is surfacing spurious CI errors earlier?

[Michael Rothgang]

How difficult is it to write a workflow that

• downloads a json file from somewhere
• checks if that contains any PRs
• if it does, posts a message on zulip?

Having the queueboard generate a json file with spurious CI failures is easy for me, but I'd need help with the other half.

[Damiano Testa]

There are many scripts already that post messages on Zulip, so the second half should be ok as well. At least if you do not want the message to contain a backtick.

[Michael Rothgang]

No, backticks should not be necessary.

[Damiano Testa]

Here is a sample from .github/workflows/maintainer_merge.yml.

      - name: Send message on Zulip
        if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' }}
        uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
        with:
          api-key: ${{ secrets.ZULIP_API_KEY }}
          email: 'github-mathlib4-bot@leanprover.zulipchat.com'
          organization-url: 'https://leanprover.zulipchat.com'
          to: 'mathlib reviewers'
          type: 'stream'
          topic: ${{ steps.determine_topic.outputs.topic }}
          content: ${{ steps.form_the_message.outputs.title }}

It should be clear what the various fields are. In this case, topic and content were determined by other scripts in the previous CI steps.

[Kevin Buzzard]

Maybe we should modify instructions to users from "please reopen this PR from a branch not a fork" to "... and also ensure that you use a new branch name"

[Kevin Buzzard]

I think we saw this phenomenon at least once before

[Robert Maxton]

As a side note, I checked and can confirm that this was indeed the PR that was originally from a fork.

[Ruben Van de Velde]

Oh, is it then actually the branch name that's the issue or that both PRs are made with the exact same commit hash?

[Kevin Buzzard]

Oh my bet is on the commit hash being the thing which confuses github, I think that was the issue before. Sorry for the noise.