What projects are eligible for cache?

Stream: lean4

[Heather Macbeth]

Could someone explain a little bit how lake exe cache get works? Is it possible to add one's own projects to the things whose builds are cached?

As of a couple of weeks ago, Mechanics of Proof depends on a fork of duper with a few hacks to downgrade (!) its capabilities for teaching purposes. This has substantially slowed down the setup process because it now needs to include the time to build the duper fork, so I'd love to see the fork cached if that is allowed.

I'm also curious whether there's a way to disable the "warning: package Duper has local changes" message which currently flashes in the infoview because I am on this fork.

[Joachim Breitner]

Currently, the cache infrastructure is a mathlib-specific feature and thus only available there. The FRO has plans to offers something comparable as part of the Reservoir package repository, but don’t hold your breath unless you can go without oxygen for at least a few months.

If you are motivated you can probably fork `cache from mathlib, change a few paths etc, but I don’t expect it to be trivial.

[Heather Macbeth]

OK, thanks for the explanation!

Heather Macbeth said:

I'm also curious whether there's a way to disable the "warning: package Duper has local changes" message which currently flashes in the infoview because I am on this fork.

Do you know the answer to this one?

[Henrik Böving]

One additional question about cache that I couldn't ask because I had to leave: Is there a story for caching packages that interact with C via FFI? That seems like a pretty hard problem given that you usually need per OS and perhaps even shared library version specific code etc.

[Eric Rodriguez]

https://github.com/leanprover/lean4/blob/66aa2c46a84f6755b63c996f79150121704cac3e/src/lake/Lake/Load/Materialize.lean#L162, and elsewhere in this file, seems to be where this error comes from - it seems that if the git repository has no changes with upstream it shouldn't show it?

[Heather Macbeth]

Does that mean that the "upstream" of my duper fork is set to be leanprover-community duper? Is there a way to say within the context of the math2001 repo that hrmacbeth/duper is the canonical version of duper?

[Eric Rodriguez]

https://github.com/hrmacbeth/math2001/blob/main/lakefile.lean Heather's lakefile, for reference

[Eric Rodriguez]

It seems to me that it shouldn't be in some way pointing to the community duper, so I'm surprised it does

[Alex J. Best]

The "local changes" in this case appear to be lakefile.olean which makes me think that all that needs to happen is that that is added to .gitignore or Duper, or the fork

[Alex J. Best]

And it seems core duper has this change already, so that just needs to be copied accross to heathers fork

[Mario Carneiro]

you shouldn't need lakefile.olean in your gitignore anymore, it has been moved to .lake and that folder should be .gitignored instead

[Alex J. Best]

Yes, but duper is still on 4.3rc1 for now at least

[Mac Malone]

Henrik Böving said:

One additional question about cache that I couldn't ask because I had to leave: Is there a story for caching packages that interact with C via FFI? That seems like a pretty hard problem given that you usually need per OS and perhaps even shared library version specific code etc.

A similar questions actually did end up being asked during the meeting. The goal is for Reservoir cloud builds to store per-platform copies of packages. In essence, it is meant to be a more principled and generally applicable version of the lake exe cache and Lake GitHub cloud releases (i.e., lake upload/ lake build :release).

[Scott Morrison]

@Mac Malone, individual oleans, not just whole packages, right?

[Arthur Paulino]

This thread is about https://github.com/leanprover/lake/issues/153
I'm not following the trend of how things are being developed. But the issue I opened was about users having access to a native lake cache that would do caching with the same content-addressing tricks as the one implemented for Mathlib, which saves cloud space, local space and data transfers between those two

[Mac Malone]

Scott Morrison said:

Mac Malone, individual oleans, not just whole packages, right?

Probably both.

[Mac Malone]

(The design here is still not clear.)

[Damiano Testa]

I am not sure that I understand fully, but does this mean that there is no way to download the Std cache, for a project that depends only on Std, but not on all of Mathlib?

[Mario Carneiro]

that is correct, the cache program itself is distributed by mathlib so you can't use mathlib's cache of Std if you have a Std-only project

[Damiano Testa]

Thanks, Mario! I still find the cache business mysterious, so I am grateful for the clear explanation!

[Eric Wieser]

Is this an argument for upstreaming cache to std?

[Mario Carneiro]

I'd rather upstream cache to lake

[Shreyas Srinivas]

How would you handle toolchain conflicts?