GitHub Actions complaints

Stream: mathlib4

[Kevin Buzzard]

I was reviewing #11255 on github and in the "Files changed" tab under the actual work of the PR I see several

#### GitHub Actions / Add annotations

Synchronization

messages which look to me to be unrelated to the work. Do I just ignore them? What's going on here? (basically I'm reading more of the smallprint in github nowadays)

[Eric Wieser]

This is a bug in the action that deals with mathlib3 forward ports, which was never quite annoying enough for me to fix

[Michael Rothgang]

Slightly naive question: given the port is complete, and (if I understand correctly!) the forward-ports also, is this CI step still useful? If not, the easiest solution might be to delete that step :-)

[Kim Morrison]

#12784

[Miyahara Kō]

Github actions looks dead... :skull:

[Miyahara Kō]

@github-runners-maintainers

[Miyahara Kō]

@github-runners-maintainers Oh, it looks recovered. Thank you.

[Miyahara Kō]

@github-runners-maintainers No, something went wrong. Finished actions is displayed as in progress and many actions are queued.

[Kim Morrison]

Not sure yet. The list of runners at https://github.com/organizations/leanprover-community/settings/actions/runners says that all but two are idle.

[Yaël Dillies]

We can't see that webpage

[Kim Morrison]

It says all but two are idle. :-)

[Sébastien Gouëzel]

According to https://downdetector.com/status/github/, it's probably a github issue.

[Markus Himmel]

The official status page agrees: https://www.githubstatus.com/

[Kim Morrison]

Everything seems to be running normally again.

[Bolton Bailey]

Kim Morrison said:

Everything seems to be running normally again.

I still can't see the linked webpage. (Are we sure that non-members of the organization are supposed to be able to see it)

[Kim Morrison]

Yes, you're not meant to be able to see it.