Get-cache

Stream: mathlib4

[Moritz Doll]

Are there any plans to set up caching for the builds on github? Running lake build is still ok for me, but it is way slower now that we have some files ported and I suspect that in a few weeks it will be much slower.

[Kevin Buzzard]

It takes a few minutes for me right now

[Alex J. Best]

I notice that lake has an upload option now to up/download build artifacts to releases (see https://github.com/leanprover/lake#github-release-builds) but I'm not sure if this will do what we want or is just for executables

[Mario Carneiro]

I would appreciate if someone did some tests with it and give an experience report before we deploy it on mathlib

[Moritz Doll]

I've had a look and I am afraid that it does not really work for our purposes: you have to create a git-tag for each artifact and we probably want to have automatic builds for all branches.
It seems like we probably have to adapt leanproject to mathlib4.
I don't have any knowledge how the CI works in mathlib3, but I feel there are some nontrivial decisions to be made: since the builds are now machine dependent we have to figure out how to build for the fewest possible targets without excluding people from using the caches that have exotic hardware/OSes. Building for all possible Lean 4 targets is probably a huge waste of space and time, but I don't have a good idea on how to tell github which branches should build for which target

[Mario Carneiro]

Lean 4 already has a fairly limited set of tested OSs in its own CI setup

[Mario Carneiro]

we could just support those

[Mario Carneiro]

Also, it's possible that we can still use it for a different purpose than the leanproject cache-everything approach. For example, it would be nice if you didn't have to spend the first 2 minutes compiling Std and Aesop before you can even get to mathlib

[Mario Carneiro]

those tags sound like a lot of mess though. Something like std will probably want to tag every commit

[Moritz Doll]

I agree that the lake upload feature might be very useful for std and aesop (Jannis wanted to try it out).

[Moritz Doll]

My guess was just to create nightly tags

[Moritz Doll]

I don't know how fast std is intended to change

[Mario Carneiro]

it usually only gets 1-5 commits a day, and is dormant for days at a time (at least currently)

[Mario Carneiro]

mostly because I don't have that much time to devote to it and the PR queue is very modest

[Mario Carneiro]

I don't want the train of nightly releases to push things out by multiple days though

[Mario Carneiro]

so an update on every commit seems like a good tradeoff right now. Even if things pick up we will probably only want even more CI coverage

[Gabriel Ebner]

Another complication is that we want to bump the Lean version at least once per day as well.

[Mario Carneiro]

mathlib is the same way, it's working at breakneck pace and we still want releases for every commit

[Gabriel Ebner]

(Every Lean version requires different binaries of course.)

[Mario Carneiro]

we currently don't bump the lean version every day, it's more like every 4 days

[Moritz Doll]

but for mathlib4, even if we have only 6 targets (linux, windows, mac * amd64, aarch64), then it will increase the build times for the branches significantly and I don't know how careful we have to be with harddisk space. If it is no probably on the cloud side it is most likely trivial to add a flag in leanproject4 to download only the correct caches

[Mario Carneiro]

@Gabriel Ebner How feasible would you say it is to have cross OS, same arch binary compatibility of oleans? that would cut the matrix down to just 2

[Mario Carneiro]

the way I see it, we mostly only care about data layout of the structs and since everything is in the lean runtime we don't have to worry about interfacing with the OS most of the time. It's only things like the endianness of the machine that is visible in every instruction, for OS calls we can afford to do OS specific translation

[Gabriel Ebner]

We are fully committed to support cross-platform oleans. Precisely because of the mathlib CI. It is completely infeasible to build mathlib more than once. Compute is already the big bottleneck, we don't need any additional potholes on the road to 10MLOC.

[Gabriel Ebner]

(We are also depending on cross-platform olean support right now: the aarch64 builds are cross-compiled and the oleans are generated by the amd64 binary.)

[Gabriel Ebner]

(Cross-platform is defined as 64-bit little-endian of course. :smile:)

[Gabriel Ebner]

It would be super cool if we had more fine-grained caches than we had for Lean 3, i.e., file-level.

[Eric Wieser]

Moritz Doll said:

I've had a look and I am afraid that it does not really work for our purposes: you have to create a git-tag for each artifact and we probably want to have automatic builds for all branches.

Why is this the case? The artifacts api for _actions_ (not tags) ought to work, right? (https://docs.github.com/en/rest/actions/artifacts?apiVersion=2022-11-28)

[Eric Wieser]

Filtering the JSON response by workflow_run.head_sha ought to do the trick

[Eric Wieser]

Or better yet, do:

• GET /repos/{owner}/{repo}/actions/runs?head_sha=SHA (and extract the run ids)
• GET /repos/{owner}/{repo}/actions/runs/{run_id}/artifacts (for each run id until you find a successful one)
• GET {archive_download_url}

[Sebastian Ullrich]

Note that you need to be logged in to download artifacts

[Eric Wieser]

That makes it a bit harder, but it would be possible for get-cache to use oauth

[Eric Wieser]

And anyone working on mathlib likely already has a github account, which at least while we're porting is the main audience

[Gabriel Ebner]

I think you (Eric) and Moritz have been talking about different things. Moritz was talking about the lake upload feature, which requires git tags (i.e., a no go). You (Eric) were talking about github action artifacts. (Those are deleted after 60 (?) days, so not suitable for build caching either.)

[Scott Morrison]

At least for the porting efforts, build artifacts being deleted after 60 days (after 6 days even!) would not be a problem.

[Eric Wieser]

I would guess that 60 days is enough for 90% of the development that happens in mathlib3 (although I guess it might clear out faster than that if it hits a storage limit before a time limit)

[Eric Wieser]

Thanks for the clarification though!

[Jannis Limperg]

Gabriel Ebner said:

which requires git tags (i.e., a no go)

Why? I was just about to configure my CI to generate a tag for every commit, which is certainly ugly but is it a big problem?

[Gabriel Ebner]

There's two problems here: 1) that you get an enormous amount of git tags, and every time you pull you also pull all those tags. That might still work for rarely updated projects like aesop, but it doesn't help with mathlib4. 2) it doesn't actually fix the problem: we need a cache from revision×lean-toolchain → oleans, not revision→oleans. We're bumping Lean versions very quickly on mathlib4, faster than aesop.

[Jannis Limperg]

The "too many tags" issue I understand, but doesn't each commit fix its Lean toolchain?

[Gabriel Ebner]

We import the same Aesop revision with multiple Lean versions (as specified in mathlib4).

[Jannis Limperg]

Okay, that I can't support. If you'd like to move to a mode of operations where std4/aesop/mathlib4 always bump their lean-toolchain at the same time, Mario already has commit rights for Aesop and I'd be happy to give them to other people as well.

[Jannis Limperg]

If I enable the prebuilt releases now, will that mess up mathlib4 consumers with mismatched toolchains or will Lake/Lean recognise the discrepancy?

[Sebastian Ullrich]

If I understood Lake directly, it will simply ignore the downloaded oleans in that case because the Lean version is part of the fingerprint

[Jannis Limperg]

Okay, nice!

[Sebastian Ullrich]

Is this the right time to mention my splendid idea of having Nix download oleans from a Nix cache and put them in Lake's build directory :upside_down: ? While that would avoid the issue of getting Nix builds on Windows working, getting just the evaluation and downloading part on Windows working might not be trivial even with Cygwin speaking from experience, and cross-platform oleans would first have to be solved as well e.g. with the content-addressing hack I outlined at some point.

[Sebastian Ullrich]

So just to motivate this far-out idea for those not familiar with Nix: the upside would be that Nix has a really robust system for downloading build results independent of releases/git commits/..., just based on the build recipe and inputs. So for a new commit only the changed oleans would have to be stored and downloaded. And services like https://www.cachix.org/ make it trivial to spin up such a store of a reasonable size for free.

[Mario Carneiro]

Is there a reason we can't just make a homebrew version of Nix tailored to our needs? It seems like the ideas are more important than the execution there

[Sebastian Ullrich]

That's another possibility, sure. I wouldn't like to e.g. drive libcurl from inside a Lean program in order to efficiently download many small files, but I guess this can always be done in an FFI wrapper.

[Sebastian Ullrich]

With that, checking olean availability over HTTPS by Lake fingerprint shouldn't be too hard. Then the main remaining questions would be where to host stuff (not GitHub Pages, I assume) and what protocol (and authentication) to use for uploading.

[Jannis Limperg]

I managed to set up prebuilt releases for Aesop, but they don't seem to get used (i.e. Lake downloads them but then recompiles anyway). Maybe this is because Aesop needs not just oleans but also compilation; maybe it's because the std4 dependency gets compiled in some subtly different way that affects the fingerprints; maybe I didn't package the build outputs correctly. If anyone is interested in the mostly-working setup, the CI script is on the ci-experiments branch.

[Gabriel Ebner]

With that, checking olean availability over HTTPS by Lake fingerprint shouldn't be too hard. Then the main remaining questions would be where to host stuff (not GitHub Pages, I assume) and what protocol (and authentication) to use for uploading.

The hosting part isn't too hard. Once you have curl, you can just PUT it.

[Sebastian Ullrich]

Yeah, and I'm sure hosting for mathlib will also not be hard to find. I was more wondering about the greater ecosystem, though perhaps a generous sponsor could be found covering all open-source Lean libraries...

[James Gallicchio]

This sounds a bit like a job for a theoretical Reservoir (Lake : Reservoir :: cargo :: crates.io). There's some decent documentation here: https://github.com/rust-lang/crates.io/blob/master/docs/ARCHITECTURE.md

[James Gallicchio]

Oh nevermind, the docs get sparse very fast..........

[Gabriel Ebner]

In case you haven't seen it already: there's a very similarly named and highly relevant thread: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/lake.20get-cache/near/319306115

[James Gallicchio]

oh! Thank you!