Weird CI error

Stream: mathlib4

[Yaël Dillies]

Does anybody know what this error means? https://github.com/leanprover-community/mathlib4/actions/runs/8474149232/job/23219982915?pr=11750
This is a new one to me

[Ruben Van de Velde]

There's something wrong with the script, but it's trying to point out that you left a #minimize_imports in

[Damiano Testa]

Btw, the #-command linter did not flag it, since it is in Archive and the linter is only active in Mathlib. The error from that linter would have hopefully been more informative.

[Yaël Dillies]

Does anybody know what this error means https://github.com/leanprover-community/mathlib4/actions/runs/8986149647/job/24685474223?pr=11855 ?

[Matthew Ballard]

8BitJonny?

[Matthew Ballard]

GitHub is having issues and wait?

[Ruben Van de Velde]

Maybe that you pushed too fast

[Ruben Van de Velde]

Wait n

[Ruben Van de Velde]

o

[Matthew Ballard]

I got it too

[Yaël Dillies]

Oh indeed https://www.githubstatus.com says something is up

[Matthew Ballard]

If GitHub is passing mal-formed json via its APIs, then there is a bigger problem

[Ruben Van de Velde]

It's just an empty response

[Matthew Ballard]

You can quickly review #12729 in your newly found spare time :)

[Richard Osborn]

it's an http error 500 response which means the service is overloaded

[Anatole Dedecker]

Probably related: #queue appears empty to me (congrats to all reviewers, we made it :tada:)

[Bernhard Reinke]

Does anybody know what this error means? https://github.com/leanprover-community/mathlib4/actions/runs/13785712351/job/38553179596?pr=22823

[Ruben Van de Velde]

Eek

[Ruben Van de Velde]

Let's try that again