Zulip Chat Archive

Stream: triage

Topic: workflow failure


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Rob Lewis (Apr 28 2021 at 15:48):

The script isn't exactly robust

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 20 2021 at 06:06):

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

view this post on Zulip Bryan Gin-ge Chen (May 20 2021 at 06:08):

I haven't looked into it yet, sorry!

view this post on Zulip 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: Jun 19 2021 at 23:11 UTC