feat(Cache): make use of local Lake artifact cache#4
Draft
tydeu wants to merge 8 commits intoleanprover-community:nightly-testingfrom
Draft
feat(Cache): make use of local Lake artifact cache#4tydeu wants to merge 8 commits intoleanprover-community:nightly-testingfrom
tydeu wants to merge 8 commits intoleanprover-community:nightly-testingfrom
Conversation
tydeu
force-pushed
the
use-lake-cache
branch
4 times, most recently
from
34a5ed2 to
c9857fe
Compare
kim-em
force-pushed
the
use-lake-cache
branch
from
c9857fe to
ae8c2f0
Compare
tydeu
force-pushed
the
use-lake-cache
branch
3 times, most recently
from
f6efe14 to
b735953
Compare
tydeu
force-pushed
the
use-lake-cache
branch
2 times, most recently
from
55d56cf to
07f1a48
Compare
|
Just recording this for later, but here's what Claude identified as possibly problematic in Mathlib:
|
kim-em
force-pushed
the
nightly-testing
branch
4 times, most recently
from
e1cf1ba to
91522ad
Compare
tydeu
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR extends Mathlib's cache to enable packing and unpacking files to/from the machine-local Lake artifact cache.
In the new caching strategy, a module's artifacts are stored differently in the
leantararchives and thus the new archives are incompatible with setups without the local Lake cache. The archive packs the trace file from the build directory and the artifacts from the local Lake cache. When unpacked, they will also be restored to local Lake cache.With the new setup, after fetching the cache once for a version of Mathlib, the built modules will be available to all instances of Mathlib on the system (if they have the same version of the module).