Zulip Chat Archive

Stream: mathlib4

Topic: Get-cache


Moritz Doll (Nov 17 2022 at 02:20):

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 (Nov 17 2022 at 07:41):

It takes a few minutes for me right now

Alex J. Best (Nov 17 2022 at 13:02):

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 (Nov 17 2022 at 13:12):

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

Moritz Doll (Dec 06 2022 at 01:16):

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 (Dec 06 2022 at 01:18):

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

Mario Carneiro (Dec 06 2022 at 01:18):

we could just support those

Mario Carneiro (Dec 06 2022 at 01:20):

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 (Dec 06 2022 at 01:21):

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

Moritz Doll (Dec 06 2022 at 01:21):

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

Moritz Doll (Dec 06 2022 at 01:22):

My guess was just to create nightly tags

Moritz Doll (Dec 06 2022 at 01:22):

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

Mario Carneiro (Dec 06 2022 at 01:23):

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

Mario Carneiro (Dec 06 2022 at 01:24):

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

Mario Carneiro (Dec 06 2022 at 01:24):

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

Mario Carneiro (Dec 06 2022 at 01:26):

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 (Dec 06 2022 at 01:26):

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

Mario Carneiro (Dec 06 2022 at 01:26):

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

Gabriel Ebner (Dec 06 2022 at 01:27):

(Every Lean version requires different binaries of course.)

Mario Carneiro (Dec 06 2022 at 01:27):

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

Moritz Doll (Dec 06 2022 at 01:28):

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 (Dec 06 2022 at 01:30):

@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 (Dec 06 2022 at 01:33):

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 (Dec 06 2022 at 01:37):

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 (Dec 06 2022 at 01:38):

(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 (Dec 06 2022 at 01:39):

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

Gabriel Ebner (Dec 06 2022 at 01:41):

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

Eric Wieser (Dec 06 2022 at 12:16):

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 (Dec 06 2022 at 12:18):

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

Eric Wieser (Dec 06 2022 at 12:20):

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 (Dec 06 2022 at 12:21):

Note that you need to be logged in to download artifacts

Eric Wieser (Dec 06 2022 at 12:33):

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

Eric Wieser (Dec 06 2022 at 12:34):

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

Gabriel Ebner (Dec 06 2022 at 21:04):

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 (Dec 06 2022 at 21:57):

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

Eric Wieser (Dec 06 2022 at 22:14):

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 (Dec 06 2022 at 22:14):

Thanks for the clarification though!

Jannis Limperg (Dec 06 2022 at 23:17):

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 (Dec 06 2022 at 23:41):

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 (Dec 06 2022 at 23:58):

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

Gabriel Ebner (Dec 07 2022 at 00:03):

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

Jannis Limperg (Dec 07 2022 at 09:54):

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 (Dec 07 2022 at 10:01):

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 (Dec 07 2022 at 10:11):

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 (Dec 07 2022 at 10:12):

Okay, nice!

Sebastian Ullrich (Dec 07 2022 at 10:23):

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 (Dec 07 2022 at 10:25):

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 (Dec 07 2022 at 10:38):

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 (Dec 07 2022 at 12:00):

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 (Dec 07 2022 at 12:03):

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 (Dec 07 2022 at 14:26):

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 (Dec 07 2022 at 18:48):

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 (Dec 07 2022 at 19:51):

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 (Jan 10 2023 at 03:36):

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 (Jan 10 2023 at 03:38):

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

Gabriel Ebner (Jan 10 2023 at 03:49):

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 (Jan 10 2023 at 06:00):

oh! Thank you!


Last updated: Dec 20 2023 at 11:08 UTC