Zulip Chat Archive

Stream: triage

Topic: workflow failure

Bryan Gin-ge Chen (Apr 28 2021 at 15:44):

Not sure if this is a temporary thing or if Zulip changed something, but I got this notification that one of the workflows failed: https://github.com/leanprover-community/azure-scripts/actions/runs/792941660

Rob Lewis (Apr 28 2021 at 15:48):

I'm gonna guess this is an empty array issue, like there are no PRs that meet the cutoffs for recent activity and recently posted about

Rob Lewis (Apr 28 2021 at 15:48):

The script isn't exactly robust

Gabriel Ebner (Apr 28 2021 at 16:41):

AFAICT the error happens before the script even fetches the PRs. So my guess is zulip API change, but we can wait until tomorrow and see if it fails again.

Bryan Gin-ge Chen (Apr 29 2021 at 15:32):

Indeed, it failed again: https://github.com/leanprover-community/azure-scripts/runs/2467521107?check_suite_focus=true

Johan Commelin (May 20 2021 at 06:06):

Have we already understood the exact issue? Is it easy to fix?

Bryan Gin-ge Chen (May 20 2021 at 06:08):

I haven't looked into it yet, sorry!

Johan Commelin (May 20 2021 at 06:11):

While we're at it. Should the triage bot also include issues from the lean repo?

Last updated: Dec 20 2023 at 11:08 UTC