Uncaught exception

Stream: mathlib4

[Jeremy Tan]

The new shake tool appears to be causing problems in #9403:
https://github.com/leanprover-community/mathlib4/actions/runs/7524334618/job/20478989708#step:17:4161

[Kim Morrison]

Is there a reason you think shake is involved? I don't see any mention of it in the errors.

[Mario Carneiro]

tentative fix at #9752

[Mario Carneiro]

or at least, if there are still errors that PR should help make them less impenetrable

[Kim Morrison]

Okay, 'd, lets see what happens!

[Mario Carneiro]

aha:

curl: (56) OpenSSL SSL_read: Connection reset by peer, errno 104

[Jeremy Tan]

@Mario Carneiro ready!

[Mauricio Collares]

Judging from the transient failures, lake exe cache put Archive.lean packs and uploads almost the whole of mathlib. Which makes sense, but does this mean mathlib oleans get uploaded thrice (Mathlib, archive, counterexamples)?

[Mario Carneiro]

Note that there is currently a bug in the printing code, it's supposed to show the files that are actually uploaded but the pruning is being done server-side so not all of those are actually uploaded for real

[Mario Carneiro]

Sebastian Ullrich has a PR which should help with that: #9687

[Mario Carneiro]

(this is a problem for the new cloudflare cache, because it doesn't know how to not overwrite, so we end up with a lot more redundant traffic if we don't handle the pruning client-side)