batteries
batteries copied to clipboard
Mathlib CI cache not uploading
I am not sure if this is ultimately a mathlib or batteries issue but I have been advised to post this here.
See the discussion at the end of https://leanprover.zulipchat.com/#narrow/channel/348111-batteries/topic/Chain.20and.20Chain'.20and.20Pairwise/with/540902002
In summary: mathlib4-nightly-testing#70 is correctly building mathlib, but the cache fails to be uploaded. This means effectively needing to recompile the whole library every time (because I am making a change in batteries which I have adapted for). I'm on nightly here, but I believe it's occurred for others in regular mathlib.
See https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/CI.3A.20uploading.20cache/with/540879134 for a general discussion of this issue.
In particular, I believe this is the relevant section of the log.
Attempting to upload 7225 file(s) to linesthatinterlace/mathlib4 cache
Non-JSON output from curl:
<?xml version="1.0" encoding="utf-8"?><Error><Code>BlobAlreadyExists</Code><Message>The specified blob already exists.
offset 0: unexpected input
Non-JSON output from curl:
RequestId:ee7f1f9b-701e-005c-05d0-2becc5000000
offset 0: unexpected input