Zulip Chat Archive

Stream: nightly-testing

Topic: Mathlib `lake update` failure

github mathlib4 bot (Jul 27 2025 at 02:38):

:cross_mark: lake update failed. Found PR 27530.

Bryan Gin-ge Chen (Jul 27 2025 at 02:43):

This bot was stuck since early July for some reason which I haven't figured out yet; I closed the previous PR and re-ran it.

github mathlib4 bot (Jul 27 2025 at 03:46):

:cross_mark: lake update failed. Found PR 27530.

github mathlib4 bot (Jul 27 2025 at 04:32):

:cross_mark: lake update failed. Found PR 27530.

Bryan Gin-ge Chen (Jul 27 2025 at 04:58):

Various files are just missing some imports after batteries#1205, I think. Will push a fix within the hour.

github mathlib4 bot (Jul 27 2025 at 06:41):

:cross_mark: lake update failed. Found PR 27530.

Bryan Gin-ge Chen (Jul 27 2025 at 06:54):

The failure after my fixes is now in Mathlib.lean:

error: Mathlib.lean:1:0: import Batteries.Data.String.Lemmas failed, environment already contains 'String.instTransOrd' from Std.Classes.Ord.String

I'm out of time to look into this further, but I guess it's related to the problem that this line in Batteries.Data.String.Lemmas is supposed to fix.

Since I pushed directly to branch#update-dependencies-bot-use-only, I manually disabled the "Update Mathlib Dependencies" workflow temporarily so that it wouldn't force push over my work. Feel free to turn it back on if needed.

edit: workflow re-enabled

Kim Morrison (Jul 27 2025 at 07:14):

Fixed in batteries#1348

github mathlib4 bot (Jul 27 2025 at 15:15):

:cross_mark: lake update failed. No PR found for this run! If you are feeling impatient and have write access, please go to the following page and click the "Run workflow" button!
https://github.com/leanprover-community/mathlib4/actions/workflows/update_dependencies.yml

Robin Arnez (Jul 27 2025 at 19:05):

(deleted)

github mathlib4 bot (Jul 28 2025 at 22:10):

:cross_mark: lake update failed. No PR found for this run! If you are feeling impatient and have write access, please go to the following page and click the "Run workflow" button!
https://github.com/leanprover-community/mathlib4/actions/workflows/update_dependencies.yml

Bryan Gin-ge Chen (Jul 28 2025 at 22:20):

429 (Too Many Requests) error when trying to download actions/checkout. Presumably this will go away in the next run.

Bryan Gin-ge Chen (Jul 28 2025 at 22:21):

Ah, it's a GitHub incident: https://www.githubstatus.com/incidents/s6d4x8c6cvv5

github mathlib4 bot (Jul 29 2025 at 00:35):

:cross_mark: lake update failed. No PR found for this run! If you are feeling impatient and have write access, please go to the following page and click the "Run workflow" button!
https://github.com/leanprover-community/mathlib4/actions/workflows/update_dependencies.yml

Bryan Gin-ge Chen (Jul 29 2025 at 01:32):

Looks like it's another (?) github incident? https://www.githubstatus.com/incidents/61btx2g21zc6

github mathlib4 bot (Jul 29 2025 at 16:18):

:cross_mark: lake update failed. No PR found for this run! If you are feeling impatient and have write access, please go to the following page and click the "Run workflow" button!
https://github.com/leanprover-community/mathlib4/actions/workflows/update_dependencies.yml

github mathlib4 bot (Aug 04 2025 at 01:43):

:cross_mark: lake update failed. Found PR 27916.

github mathlib4 bot (Aug 04 2025 at 02:55):

:cross_mark: lake update failed. Found PR 27916.

github mathlib4 bot (Aug 04 2025 at 03:45):

:cross_mark: lake update failed. Found PR 27916.

github mathlib4 bot (Aug 04 2025 at 04:33):

:cross_mark: lake update failed. Found PR 27916.

Kim Morrison (Aug 04 2025 at 13:37):

We've now merged a lake update manually, so the errors have (hopefully) stopped.

github mathlib4 bot (Aug 06 2025 at 16:52):

:cross_mark: lake update failed. Found PR 28051.

github mathlib4 bot (Aug 06 2025 at 17:46):

:cross_mark: lake update failed. Found PR 28051.

github mathlib4 bot (Aug 06 2025 at 18:44):

:cross_mark: lake update failed. Found PR 28051.

github mathlib4 bot (Aug 06 2025 at 20:11):

:cross_mark: lake update failed. Found PR 28051.

github mathlib4 bot (Aug 06 2025 at 21:38):

:cross_mark: lake update failed. Found PR 28051.

github mathlib4 bot (Aug 06 2025 at 23:49):

:cross_mark: lake update failed. Found PR 28051.

Bryan Gin-ge Chen (Aug 07 2025 at 00:21):

I'm looking at this now.

Kim Morrison (Aug 07 2025 at 00:28):

Oh, me too!

Kim Morrison (Aug 07 2025 at 00:28):

I have a local build going.

Kim Morrison (Aug 07 2025 at 00:29):

2270/7035 with no errors so far. If you're further on I'll stop :-)

Bryan Gin-ge Chen (Aug 07 2025 at 00:29):

I pushed a fix that built locally and tagged it auto-merge-after-CI. :crossed:

Bryan Gin-ge Chen (Aug 07 2025 at 00:30):

I have no idea why this commit to batteries, which only changes stuff in the Batteries.CodeAction namespace caused this breakage though.

github mathlib4 bot (Aug 08 2025 at 04:56):

:cross_mark: lake update failed. Found PR 28107.

Kim Morrison (Aug 08 2025 at 05:00):

#28108

github mathlib4 bot (Aug 08 2025 at 06:29):

:cross_mark: lake update failed. Found PR 28107.

github mathlib4 bot (Aug 08 2025 at 08:27):

:cross_mark: lake update failed. Found PR 28107.

github mathlib4 bot (Aug 08 2025 at 09:25):

:cross_mark: lake update failed. Found PR 28107.

github mathlib4 bot (Aug 08 2025 at 10:22):

:cross_mark: lake update failed. Found PR 28107.

github mathlib4 bot (Aug 08 2025 at 11:37):

:cross_mark: lake update failed. Found PR 28107.

github mathlib4 bot (Aug 08 2025 at 12:40):

:cross_mark: lake update failed. Found PR 28107.

github mathlib4 bot (Aug 08 2025 at 13:35):

:cross_mark: lake update failed. Found PR 28107.

github mathlib4 bot (Aug 16 2025 at 14:09):

:cross_mark: lake update failed. No PR found for this run! If you are feeling impatient and have write access, please go to the following page and click the "Run workflow" button!
https://github.com/leanprover-community/mathlib4/actions/workflows/update_dependencies.yml

Bryan Gin-ge Chen (Aug 16 2025 at 14:12):

Weird error while downloading the cache - hopefully will go away.

Recv failure: Connection reset by peer
Send failure: Broken pipe

edit: I re-ran the job above since it was causing a red x on master. Here's a link to the first (failed) run: https://github.com/leanprover-community/mathlib4/actions/runs/17009269932/job/48223110744#step:16:25

github mathlib4 bot (Aug 17 2025 at 17:09):

:cross_mark: lake update failed. No PR found for this run! If you are feeling impatient and have write access, please go to the following page and click the "Run workflow" button!
https://github.com/leanprover-community/mathlib4/actions/workflows/update_dependencies.yml

Bryan Gin-ge Chen (Aug 17 2025 at 17:47):

The same weird error - is this something we should raise with a hosting provider?

From https://github.com/leanprover-community/mathlib4/actions/runs/17023664560/job/48256205798#step:16:42

Send failure: Broken pipe

Kim Morrison (Aug 17 2025 at 22:59):

@Mac Malone, I guess these errors are arising after we've switched over the cache back end. Have we seen it happening elsewhere?

Bryan Gin-ge Chen (Aug 18 2025 at 01:33):

This seems to have also affected #26074 (which broke around the same time as the most recent failure above).

From: https://github.com/leanprover-community/mathlib4/actions/runs/17021894997/job/48252113959#step:24:19

Attempting to download 2 file(s) from leanprover-community/mathlib4 cache
Downloaded: 0 file(s) [attempted 2/2 = 100%] (0% success), 2 failed
2 download(s) failed

Bryan Gin-ge Chen (Aug 18 2025 at 23:06):

Same error on #26157 about 3 hours ago: https://github.com/leanprover-community/mathlib4/actions/runs/17050398350/job/48336370726#step:16:23

Send failure: Broken pipe

Bryan Gin-ge Chen (Aug 19 2025 at 02:19):

This might be the same issue? From a staging run about 15 minutes ago: https://github.com/leanprover-community/mathlib4/actions/runs/17056729073/job/48357766838#step:3:389

Send failure: Broken pipe

github mathlib4 bot (Aug 20 2025 at 07:18):

:cross_mark: lake update failed. No PR found for this run! If you are feeling impatient and have write access, please go to the following page and click the "Run workflow" button!
https://github.com/leanprover-community/mathlib4/actions/workflows/update_dependencies.yml

Bryan Gin-ge Chen (Aug 20 2025 at 11:26):

The above failure seems to have been a network error while trying to get elan from GitHub: https://github.com/leanprover-community/mathlib4/actions/runs/17091220493/job/48465821791#step:3:25

Bryan Gin-ge Chen (Aug 20 2025 at 11:31):

Still seems like there's issues with downloading from lean-lang.org. From a failed "Update Mathlib Dependencies" run about 23 minutes ago: https://github.com/leanprover-community/mathlib4/actions/runs/17096555725/job/48482261230#step:8:5

error: leanprover-community/plausible: Reservoir lookup failed; server returned invalid JSON: offset 58: expected end of input

Bryan Gin-ge Chen (Aug 21 2025 at 11:52):

Same issue as above about 45 mins ago: https://github.com/leanprover-community/mathlib4/actions/runs/17125091332/job/48574799115#step:8:5

error: leanprover-community/plausible: Reservoir lookup failed; server returned invalid JSON: offset 58: expected end of input
error: leanprover-community/plausible: could not materialize package: this may be a transient error or a bug in Lake or Reservoir

Bryan Gin-ge Chen (Aug 21 2025 at 15:31):

More cache flakiness, this time hitting a staging run: https://github.com/leanprover-community/mathlib4/actions/runs/17130338957/job/48592596128#step:16:133

Send failure: Broken pipe

Kim Morrison (Aug 21 2025 at 23:13):

github had an overnight outage

Bryan Gin-ge Chen (Aug 21 2025 at 23:35):

That incident did indeed cause lots of our CI jobs to fail due to not getting GitHub hosted runners in time, but the timing only intersected with the staging failure I posted above, and I'm not sure that it could have caused the "Send failure" cache download errors in that log (which have also shown up in lots of the other failures from the past 5 days).

Bryan Gin-ge Chen (Aug 22 2025 at 16:25):

15 minutes ago, from https://github.com/leanprover-community/mathlib4/actions/runs/17160212638/job/48687302541#step:8:5

error: leanprover-community/plausible: Reservoir lookup failed; server returned invalid JSON: offset 58: expected end of input
error: leanprover-community/plausible: could not materialize package: this may be a transient error or a bug in Lake or Reservoir

github mathlib4 bot (Aug 23 2025 at 18:18):

:cross_mark: lake update failed. No PR found for this run! If you are feeling impatient and have write access, please go to the following page and click the "Run workflow" button!
https://github.com/leanprover-community/mathlib4/actions/workflows/update_dependencies.yml

github mathlib4 bot (Aug 27 2025 at 14:20):

:cross_mark: lake update failed. No PR found for this run! If you are feeling impatient and have write access, please go to the following page and click the "Run workflow" button!
https://github.com/leanprover-community/mathlib4/actions/workflows/update_dependencies.yml

github mathlib4 bot (Aug 27 2025 at 16:26):

:cross_mark: lake update failed. No PR found for this run! If you are feeling impatient and have write access, please go to the following page and click the "Run workflow" button!
https://github.com/leanprover-community/mathlib4/actions/workflows/update_dependencies.yml

github mathlib4 bot (Aug 28 2025 at 15:10):

:cross_mark: lake update failed. No PR found for this run! If you are feeling impatient and have write access, please go to the following page and click the "Run workflow" button!
https://github.com/leanprover-community/mathlib4/actions/workflows/update_dependencies.yml

Bryan Gin-ge Chen (Aug 28 2025 at 15:46):

The above failure is from Cache host issues again https://github.com/leanprover-community/mathlib4/actions/runs/17299992484/job/49108262654#step:16:250

Send failure: Broken pipe

github mathlib4 bot (Aug 30 2025 at 13:22):

:cross_mark: lake update failed. Found PR 29139.

github mathlib4 bot (Aug 30 2025 at 20:17):

:cross_mark: lake update failed. Found PR 29146.

github mathlib4 bot (Aug 30 2025 at 21:10):

:cross_mark: lake update failed. Found PR 29146.

github mathlib4 bot (Aug 30 2025 at 23:09):

:cross_mark: lake update failed. Found PR 29146.

github mathlib4 bot (Aug 31 2025 at 00:35):

:cross_mark: lake update failed. Found PR 29146.

github mathlib4 bot (Aug 31 2025 at 01:37):

:cross_mark: lake update failed. Found PR 29146.

Bryan Gin-ge Chen (Aug 31 2025 at 02:04):

Will be fixed after #29142 lands.

github mathlib4 bot (Aug 31 2025 at 02:39):

:cross_mark: lake update failed. Found PR 29146.

github mathlib4 bot (Aug 31 2025 at 14:09):

:cross_mark: lake update failed. No PR found for this run! If you are feeling impatient and have write access, please go to the following page and click the "Run workflow" button!
https://github.com/leanprover-community/mathlib4/actions/workflows/update_dependencies.yml

Bryan Gin-ge Chen (Aug 31 2025 at 14:22):

on mobile, but more cache network issues

github mathlib4 bot (Sep 02 2025 at 23:18):

:cross_mark: lake update failed. No PR found for this run! If you are feeling impatient and have write access, please go to the following page and click the "Run workflow" button!
https://github.com/leanprover-community/mathlib4/actions/workflows/update_dependencies.yml

Bryan Gin-ge Chen (Sep 03 2025 at 04:10):

https://github.com/leanprover-community/mathlib4/actions/runs/17418164779/job/49451562003#step:3:187

Send failure: Broken pipe

Bryan Gin-ge Chen (Sep 03 2025 at 19:16):

Resevoir network issue? https://github.com/leanprover-community/mathlib4/actions/runs/17443477838/job/49532010865#step:8:5

Kim Morrison (Sep 03 2025 at 23:17):

@Mac Malone:

error: leanprover-community/plausible: Reservoir lookup failed; server returned invalid JSON: offset 58: expected end of input
error: leanprover-community/plausible: could not materialize package: this may be a transient error or a bug in Lake or Reservoir

Can we improve the situation here? Ideally the error message would tell the user whether it is a transient error or something they should escalate.

(e.g. maybe add a retry if not already present, or print the actual input received, or detect whether it is actually an HTML error message, etc)?

Mac Malone (Sep 03 2025 at 23:25):

@Kim Morrison It does retry. If run with -v, it will also print the whole reponse. It unfortunately does not print the verbose log automatically on the error due to technical differences between logging during configuration and logging during build jobs. However, I am hoping to revamping logging for configuration in the coming days, so I will put this on my TODO list.

Kim Morrison (Sep 04 2025 at 03:01):

Thank you! In the meantime I think I will add -v to all lake commands in CI. No point not having this info in the logs.

Kim Morrison (Sep 04 2025 at 03:05):

#29338 just adds -v to lake update

Kim Morrison (Sep 04 2025 at 03:06):

I think lake build -v is too verbose by default, even for CI logs

github mathlib4 bot (Sep 08 2025 at 01:23):

:cross_mark: lake update failed. Found PR 29417.

Kim Morrison (Sep 08 2025 at 02:15):

I think this was an intermittent failure while we switched over the cache.

Bryan Gin-ge Chen (Sep 08 2025 at 04:07):

The same error hit #29419, twice now: #rss > mathlib bors notifications @ 💬

github mathlib4 bot (Sep 08 2025 at 06:07):

:cross_mark: lake update failed. Found PR 29417.

github mathlib4 bot (Sep 17 2025 at 09:03):

:cross_mark: lake update failed. Found PR 29738.

github mathlib4 bot (Sep 17 2025 at 09:22):

:cross_mark: lake update failed. Found PR 29738.

github mathlib4 bot (Sep 17 2025 at 10:29):

:cross_mark: lake update failed. Found PR 29738.

github mathlib4 bot (Sep 17 2025 at 11:37):

:cross_mark: lake update failed. Found PR 29738.

github mathlib4 bot (Sep 17 2025 at 12:54):

:cross_mark: lake update failed. Found PR 29738.

github mathlib4 bot (Sep 17 2025 at 14:00):

:cross_mark: lake update failed. Found PR 29738.

github mathlib4 bot (Sep 17 2025 at 14:20):

:cross_mark: lake update failed. Found PR 29738.

github mathlib4 bot (Sep 17 2025 at 15:31):

:cross_mark: lake update failed. Found PR 29738.

github mathlib4 bot (Sep 17 2025 at 16:12):

:cross_mark: lake update failed. Found PR 29738.

github mathlib4 bot (Sep 17 2025 at 17:10):

:cross_mark: lake update failed. Found PR 29738.

github mathlib4 bot (Sep 17 2025 at 18:58):

:cross_mark: lake update failed. Found PR 29738.

github mathlib4 bot (Sep 17 2025 at 19:38):

:cross_mark: lake update failed. Found PR 29738.

Bryan Gin-ge Chen (Sep 17 2025 at 19:44):

https://github.com/leanprover-community/mathlib4/actions/runs/17808028615/job/50624631044?pr=29738#step:20:255

Error: error: Mathlib/Testing/Plausible/Functions.lean:363:12: invalid do notation, expected type is not a monad application Arbitrary (InjectiveFunction ℤ)

Robin Arnez (Sep 17 2025 at 20:17):

I have https://github.com/leanprover-community/mathlib4-nightly-testing/commit/90a85422a20137251a9edc48739a18fbeea15d6a if anyone wants to put cherry-pick that in there

Bryan Gin-ge Chen (Sep 17 2025 at 20:25):

Done #29757

github mathlib4 bot (Sep 17 2025 at 21:11):

:cross_mark: lake update failed. Found PR 29738.

Bryan Gin-ge Chen (Sep 17 2025 at 21:19):

Bryan Gin-ge Chen said:

Done #29757

I've merged this myself, thanks for the fix Robin!

github mathlib4 bot (Sep 23 2025 at 15:18):

:cross_mark: lake update failed. Found PR 29910.

github mathlib4 bot (Sep 23 2025 at 17:09):

:cross_mark: lake update failed. Found PR 29910.

github mathlib4 bot (Sep 23 2025 at 19:14):

:cross_mark: lake update failed. Found PR 29910.

github mathlib4 bot (Sep 23 2025 at 20:11):

:cross_mark: lake update failed. Found PR 29910.

github mathlib4 bot (Sep 24 2025 at 03:23):

:cross_mark: lake update failed. Found PR 29910.

github mathlib4 bot (Sep 24 2025 at 04:12):

:cross_mark: lake update failed. Found PR 29910.

github mathlib4 bot (Sep 24 2025 at 07:17):

:cross_mark: lake update failed. Found PR 29910.

github mathlib4 bot (Sep 24 2025 at 08:12):

:cross_mark: lake update failed. Found PR 29910.

github mathlib4 bot (Sep 24 2025 at 11:10):

:cross_mark: lake update failed. Found PR 29910.

github mathlib4 bot (Sep 24 2025 at 12:23):

:cross_mark: lake update failed. Found PR 29910.

github mathlib4 bot (Sep 24 2025 at 13:18):

:cross_mark: lake update failed. Found PR 29910.

github mathlib4 bot (Sep 24 2025 at 14:10):

:cross_mark: lake update failed. Found PR 29910.

github mathlib4 bot (Sep 24 2025 at 15:12):

:cross_mark: lake update failed. Found PR 29910.

github mathlib4 bot (Sep 24 2025 at 17:16):

:cross_mark: lake update failed. Found PR 29910.

Kim Morrison (Sep 25 2025 at 01:17):

I think this has now come good, once the manual adaptation PR was merged to master.

Bryan Gin-ge Chen (Sep 25 2025 at 01:21):

The "closed" emojis indicate that the PR was closed, which typically only happens when the workflow detects no more changes with master.

github mathlib4 bot (Sep 25 2025 at 03:24):

:cross_mark: lake update failed. No PR found for this run! If you are feeling impatient and have write access, please go to the following page and click the "Run workflow" button!
https://github.com/leanprover-community/mathlib4/actions/workflows/update_dependencies.yml

github mathlib4 bot (Oct 11 2025 at 21:02):

:cross_mark: lake update failed. Found PR 30449.

Bryan Gin-ge Chen (Oct 11 2025 at 21:36):

Error: error: Mathlib/Probability/ProbabilityMassFunction/Binomial.lean:31:4: unsolved goals
case h.e'_2
p : ℝ≥0
h : p ≤ 1
n i : ℕ
hi : i < n + 1
⊢ p ^ ↑⟨i, hi⟩ * (1 - p) ^ (↑(Fin.last n) - ↑⟨i, hi⟩) * ↑(n.choose ↑⟨i, hi⟩) = p ^ i * (1 - p) ^ (n - i) * ↑(n.choose i)
error: Lean exited with code 1

Bryan Gin-ge Chen (Oct 11 2025 at 21:45):

Oh, this is actually fixed in #30447.

github mathlib4 bot (Oct 11 2025 at 22:55):

:cross_mark: lake update failed. Found PR 30449.

github mathlib4 bot (Oct 21 2025 at 08:19):

:cross_mark: lake update failed. No PR found for this run! If you are feeling impatient and have write access, please go to the following page and click the "Run workflow" button!
https://github.com/leanprover-community/mathlib4/actions/workflows/update_dependencies.yml

github mathlib4 bot (Nov 03 2025 at 21:53):

:cross_mark: lake update failed. Found PR 31234.

github mathlib4 bot (Nov 03 2025 at 23:12):

:cross_mark: lake update failed. Found PR 31234.

Kim Morrison (Nov 03 2025 at 23:16):

This will come good once #30138 lands.

github mathlib4 bot (Nov 06 2025 at 23:24):

:cross_mark: lake update failed. Found PR 31335.

Kim Morrison (Nov 07 2025 at 00:16):

This will resolve when #31334 lands.

Bryan Gin-ge Chen (Nov 07 2025 at 01:18):

I don't know if #31335 will run into this, but #31234 got stuck last time due to a bug in the workflow which should be fixed by #31245.

Bryan Gin-ge Chen (Nov 07 2025 at 01:50):

Yep, it looks like #31335 is stuck. If you merge #31245, it should hopefully close itself on the next run, otherwise I'll fix it manually tomorrow.

Kim Morrison (Nov 07 2025 at 02:05):

Okay, let's merge #31245.

Bryan Gin-ge Chen (Nov 07 2025 at 04:49):

Ugh, I missed a case: #31344

I also took the opportunity to make the logging more explicit there.

github mathlib4 bot (Nov 08 2025 at 01:38):

:cross_mark: lake update failed. No PR found for this run! If you are feeling impatient and have write access, please go to the following page and click the "Run workflow" button!
https://github.com/leanprover-community/mathlib4/actions/workflows/update_dependencies.yml

Bryan Gin-ge Chen (Nov 08 2025 at 02:29):

Uh oh, this might have been my docker script change. Let me revert.

edit it turns out I somehow started hoskinson8 on an old version of the GitHub runner, maybe using an old version of the script. The runners are supposed to auto-update but somehow it didn't happen before it got some jobs. Anyways, it's now running the latest version (and the Dockerfile has been updated again) so this should hopefully not happen again.

github mathlib4 bot (Nov 09 2025 at 01:25):

:cross_mark: lake update failed. Found PR 31404.

github mathlib4 bot (Nov 09 2025 at 17:10):

:cross_mark: lake update failed. Found PR 31440.

Bryan Gin-ge Chen (Nov 09 2025 at 17:10):

Will be fixed by #31437

github mathlib4 bot (Nov 09 2025 at 23:26):

:cross_mark: lake update failed. Found PR 31448.

Bryan Gin-ge Chen (Nov 10 2025 at 04:34):

Not sure why the bot isn't triggering, but this has been failing: https://github.com/leanprover-community/mathlib4/actions/runs/19220373453/job/54937283962

Bryan Gin-ge Chen (Nov 10 2025 at 04:37):

@Kim Morrison #31457 should fix this.

Bryan Gin-ge Chen (Nov 10 2025 at 13:20):

#31465 will notify this channel when the workflow itself fails (right now messages are only posted here when a build fails, but things could go wrong before that).

I'm still thinking about the question of whether something in our build workflow should have caught the broken lakefile. Maybe it's not reasonable since the lakefile was still technically valid?

github mathlib4 bot (Nov 16 2025 at 00:48):

:cross_mark: lake update failed. Found PR 31683.

github mathlib4 bot (Nov 17 2025 at 13:35):

:cross_mark: lake update failed. No PR found for this run! If you are feeling impatient and have write access, please go to the following page and click the "Run workflow" button!
https://github.com/leanprover-community/mathlib4/actions/workflows/update_dependencies.yml

Bryan Gin-ge Chen (Nov 17 2025 at 13:37):

Looks like hoskinson4 just went down too. I'll fix this.

edit: done

github mathlib4 bot (Nov 20 2025 at 18:13):

:cross_mark: lake update failed. No PR found for this run! If you are feeling impatient and have write access, please go to the following page and click the "Run workflow" button!
https://github.com/leanprover-community/mathlib4/actions/workflows/update_dependencies.yml

github mathlib4 bot (Nov 23 2025 at 23:08):

"Update dependencies" workflow run failed!

github mathlib4 bot (Nov 24 2025 at 22:19):

:cross_mark: lake update failed. Found PR 32076.

github mathlib4 bot (Nov 26 2025 at 18:24):

:cross_mark: lake update failed. No PR found for this run! If you are feeling impatient and have write access, please go to the following page and click the "Run workflow" button!
https://github.com/leanprover-community/mathlib4/actions/workflows/update_dependencies.yml

github mathlib4 bot (Dec 05 2025 at 01:49):

:cross_mark: lake update failed. Found PR 32446.

github mathlib4 bot (Dec 06 2025 at 17:49):

:cross_mark: lake update failed. Found PR 32512.

github mathlib4 bot (Dec 06 2025 at 22:48):

:cross_mark: lake update failed. Found PR 32512.

github mathlib4 bot (Dec 08 2025 at 05:54):

:cross_mark: lake update failed. Found PR 32512.

github mathlib4 bot (Dec 09 2025 at 20:08):

"Update dependencies" workflow run failed!

github mathlib4 bot (Dec 11 2025 at 14:09):

"Update dependencies" workflow run failed!

github mathlib4 bot (Dec 11 2025 at 15:10):

:cross_mark: lake update failed. No PR found for this run! If you are feeling impatient and have write access, please go to the following page and click the "Run workflow" button!
https://github.com/leanprover-community/mathlib4/actions/workflows/update_dependencies.yml

github mathlib4 bot (Dec 11 2025 at 16:11):

"Update dependencies" workflow run failed!

Bryan Gin-ge Chen (Dec 11 2025 at 16:14):

This is probably also #rss > GitHub Status - Incident History @ 💬

github mathlib4 bot (Dec 11 2025 at 17:26):

:cross_mark: lake update failed. No PR found for this run! If you are feeling impatient and have write access, please go to the following page and click the "Run workflow" button!
https://github.com/leanprover-community/mathlib4/actions/workflows/update_dependencies.yml

Snir Broshi (Dec 11 2025 at 17:44):

Bryan Gin-ge Chen said:

This is probably also #rss > GitHub Status - Incident History @ 💬

GitHub reported 20 minutes ago that things are great now, but they still aren't, e.g. 1 2
Is there a way to report to GitHub?

Bryan Gin-ge Chen (Dec 11 2025 at 17:52):

I don't read their latest messages as saying that things are great, rather just that git operations are now working (and everything else might not be). I don't know that there's a way to contact them about this other than via usual GitHub support (which in my experience usually takes a few days to respond)

Snir Broshi (Dec 11 2025 at 17:55):

Bryan Gin-ge Chen said:

I don't read their latest messages as saying that things are great

https://www.githubstatus.com/ says "All Systems Operational", including GitHub Actions and there is no active incident because the recent incident was marked as resolved completely

Bryan Gin-ge Chen (Dec 11 2025 at 17:57):

Ah, it looks like it was marked as resolved while I was writing my message. I was refering to the update:

Git Operations is operating normally.
Posted 36 minutes ago. Dec 11, 2025 - 17:20 UTC

Maybe things are fixed now then?

Snir Broshi (Dec 11 2025 at 17:58):

3 minutes ago: https://github.com/leanprover-community/mathlib4/actions/runs/20142419361/job/57813469322 https://github.com/leanprover-community/mathlib4/actions/runs/20142419561/job/57813469549

Snir Broshi (Dec 11 2025 at 18:13):

Looks a bit flaky but it seems that builds have started working around 10 minutes ago :+1:

github mathlib4 bot (Dec 11 2025 at 18:25):

:cross_mark: lake update failed. No PR found for this run! If you are feeling impatient and have write access, please go to the following page and click the "Run workflow" button!
https://github.com/leanprover-community/mathlib4/actions/workflows/update_dependencies.yml

Snir Broshi (Dec 11 2025 at 18:33):

The problem clearly is still ongoing

Snir Broshi (Dec 11 2025 at 18:34):

I guess there's nothing to do but wait for githubstatus to notice

Snir Broshi (Dec 11 2025 at 18:36):

since there are a few successful builds, my guess is that it depends on which runner you get, so maybe GH rolled a fix but it hasn't propagated to everyone yet

github mathlib4 bot (Dec 15 2025 at 03:37):

"Update dependencies" workflow run failed!

Bryan Gin-ge Chen (Dec 15 2025 at 03:55):

problems downloading elan again: https://github.com/leanprover-community/mathlib4/actions/runs/20219644103/job/58038878638#step:3:26

Bryan Gin-ge Chen (Dec 15 2025 at 03:57):

I was going to report the fact that lean-action succeeds even though it actually failed as an issue, but Ruben beat me to it: https://github.com/leanprover/lean-action/issues/140

github mathlib4 bot (Dec 18 2025 at 03:36):

:cross_mark: lake update failed. No PR found for this run! If you are feeling impatient and have write access, please go to the following page and click the "Run workflow" button!
https://github.com/leanprover-community/mathlib4/actions/workflows/update_dependencies.yml

Bryan Gin-ge Chen (Dec 18 2025 at 03:44):

Runner out of space. Fixing it now.

edit: runner is up again

Last updated: Dec 20 2025 at 21:32 UTC