[Merged by Bors] - chore: switch cache to Lean FRO R2 bucket #9409
Conversation
| -- TODO: reimplement using HEAD requests? | ||
| let _ := overwrite |
There was a problem hiding this comment.
I am relatively sure this is not critical, but do we want it back at all? There could be a slight benefit of not paying for more costly write operations, but the number of cache put calls should not matter compared to the many more cache get calls.
There was a problem hiding this comment.
To explain further, the S3 protocol as a distributed storage protocol will always override existing files
There was a problem hiding this comment.
I think we do want to avoid overwriting files if possible. The replacement files will never be the same as the ones that are there already because they contain metadata about the commit on which the CI was run, so this will repeatedly overwrite the files, meaning that there is less room for network caching effects.
There was a problem hiding this comment.
Oh, where is that metadata? I'm only aware of the /c/{githash} files but those are conflict-free
There was a problem hiding this comment.
It's in the ltar files themselves, added via a command line option in the leantar invocation in cache. I added it because it's useful for debugging when you receive a cache file from somewhere which has something weird in it, to track down the CI run that produced it for anomalies.
There was a problem hiding this comment.
I see. Well, HEAD works as a quick existence check if you want to reimplement override that way:
$ curl --head https://mathlib4.lean-cache.cloud/f/be8332708541827a.ltar
HTTP/2 200
date: Wed, 03 Jan 2024 14:13:17 GMT
content-length: 5314
accept-ranges: bytes
etag: "d15505d8f91d3d9772835174e3f4546d"
last-modified: Wed, 03 Jan 2024 13:16:46 GMT
vary: Accept-Encoding
cf-cache-status: DYNAMIC
report-to: {"endpoints":[{"url":"https:\/\/a.nel.cloudflare.com\/report\/v3?s=uq8k15i7F7ba5QhhQELrEAMFILVl5rhgpZIzpv9m2inclQUXjHaU%2FESt0EOCNZH5CiaJG3ubQRBhqs8ACwyA5o0FSGkPoG%2FRE7LUhpjROCMZFDe6y0B7XUNRcSFhyOtukYcv57DfTB9mFcYD5rzD1M86JY9%2Fe5Zp"}],"group":"cf-nel","max_age":604800}
nel: {"success_fraction":0,"report_to":"cf-nel","max_age":604800}
server: cloudflare
cf-ray: 83fbd76c7d014d62-FRA
alt-svc: h3=":443"; ma=86400
Doing separate HEAD/PUT of course suffers from TOCTOU but I assume that's "good enough" in this case
There was a problem hiding this comment.
I think we could also avoid a second request by logging this information when we do lake exe cache get at the beginning of the run. The only case where that would differ is when two CI runs race to produce a given file, and in this case it doesn't really matter who wins.
There was a problem hiding this comment.
Yes. We might even be able to go with mtimes for the sake of simplicity - upload every .olean file newer than the start of the build
There was a problem hiding this comment.
Well we're uploading .ltar files, not .olean files... but I think cache put already has the information needed there, since it calls cache pack which does not replace existing cache files. The trouble is that there might be a cache file that exists locally on the CI machine, which was not cleared by cache clean because it is useful to skip part of the build, but does not exist in the cloud (somehow); in this case it would see that the file already existed previously and would not upload it, meaning that the file would still not exist in the cloud afterwards. Ideally the system should be able to recover from situations like that.
|
It works! 🎉 I'm going to merge this now since it's time critical, but it would be good to follow up with the other things. bors r+ |
|
bors r+ |
This will use a new, fresh cache from this commit onward. We are still working on reviving the old cache for old commits. Co-authored-by: Mario Carneiro <di.gama@gmail.com>
test/RewriteSearch/Basic.lean
Outdated
| /-- | ||
| info: Try this: rw [@List.length_append, @List.length_append, Nat.two_mul, Nat.add_assoc, Nat.add_left_comm, Nat.add_right_comm, Nat.add_assoc] | ||
| -/ |
There was a problem hiding this comment.
This seems odd... tracked in #9410
|
Canceled. |
|
bors r+ |
This will use a new, fresh cache from this commit onward. We are still working on reviving the old cache for old commits. Co-authored-by: Mario Carneiro <di.gama@gmail.com>
|
Canceled. |
|
bors r+ |
This will use a new, fresh cache from this commit onward. We are still working on reviving the old cache for old commits. Co-authored-by: Mario Carneiro <di.gama@gmail.com>
|
Build failed: |
|
bors r+ |
This will use a new, fresh cache from this commit onward. We are still working on reviving the old cache for old commits. Co-authored-by: Mario Carneiro <di.gama@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
As [reported on Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/The.20cache.20doesn't.20work/near/411058849), we're still working out some issues in the new cache provider. Since Azure is back online, let's move back to them while we work out the issues with cloudflare. The code is now set up to be able to toggle between both. Co-authored-by: Mario Carneiro <di.gama@gmail.com>
This will use a new, fresh cache from this commit onward. We are still working on reviving the old cache for old commits.