feat(Cache): enable partial cache in downstream projects by joneugster · Pull Request #21238 · leanprover-community/mathlib4

joneugster · 2025-01-29T19:22:57Z

Add features to cache and cleanup code:

enable partial cache retrieval in downstream projects: lake exe cache get MyProject.Basic downloads only the relevant cache to build MyProject/Basic.lean

depends on: [Merged by Bors] - refactor(Cache): use module name as key instead of unresolved file path #21834

Notes:

replaces: feat(Cache): enable partial cache in downstream projects #21195
should address: refactor(Cache): tidy lake-manifest parsing in Cache #8767
should address: feat(Cache): add miniget command, a minimal version of get #20568

Completed:

github-actions · 2025-01-29T19:23:52Z

PR summary 88bb6d226a

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ isInLeanCore

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for scripts/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

grunweg · 2025-01-31T13:27:10Z

Thanks for the PR - the PR description looks great! Is there a way you can split this into more incremental pieces? (I could certainly try to review smaller parts, but I won't find time for a +450 -250 lines PR this or the next week.)

joneugster · 2025-01-31T21:28:26Z

Im on vacation next week, so might not respond much.

I can split some trivial cleanup out into a seperate PR; I believe the bulk will still be quite a bit to review.

joneugster · 2025-02-10T09:47:44Z

@grunweg #21631 now contains the trivial cleanup of this PR (docstrings, renaming of variables, etc.)

…rn module names and source file location (#21815) Rewrite `getFileImports` to not use `getPackageDirs` anymore. Additionally, `getFileImports` now returns module names like `Mathlib.Data.Set.Basic` and resolved `.lean` file locations instead of non-resolved file names (`Mathlib/Data/Set/Basic.lean`) like it used to. This is in preparation for #21238. This PR should not change any behaviour in how `cache` works. Co-authored-by: Jon Eugster <[email protected]>

leanprover-community-bot-assistant · 2025-04-17T18:57:22Z

This pull request has conflicts, please merge master and resolve them.

mathlib-dependent-issues · 2026-02-15T02:43:02Z

This PR/issue depends on:

~~[Merged by Bors] - refactor(Cache): use module name as key instead of unresolved file path #21834~~
~~[Merged by Bors] - fix(Cache): error on import loop #21632~~
~~[Merged by Bors] - refactor(Cache): use the Lean search path instead of lake-manifest to determine Mathlib root. #21666~~
~~[Merged by Bors] - doc(Cache): mention arguments to cache lookup help #21701~~
~~[Merged by Bors] - doc(Cache): add docstring for CacheM.Context #21703~~
~~[Merged by Bors] - chore(Cache): rename HashMap to ModuleHashMap #21704~~
~~[Merged by Bors] - chore(Cache): use createDirAll #21705~~
~~[Merged by Bors] - chore(Cache): stylistic change to not use default #21707~~
~~[Merged by Bors] - doc(Cache/Hashing): add docstring for HashMemo #21711~~
~~[Merged by Bors] - chore(Cache): cleanup getMathlibRoot #21750~~
~~[Merged by Bors] - refactor(Cache): rewrite getFileImports to use search path and return module names and source file location #21815~~
~~[Merged by Bors] - chore(Cache): move helper functions to Cache.Lean #21816~~
~~[Merged by Bors] - refactor(Cache): refactor getPackageDir to not use manually provided package directories #21817~~
~~chore(Cache): remove unused hardcoded package directories #21818~~
~~[Merged by Bors] - feat(Cache): extend argument-parsing to allow module names and file names #21822~~
~~[Merged by Bors] - chore(Cache): remove unnecessary imports #21830~~
By Dependent Issues (🤖). Happy coding!

joneugster · 2026-02-16T16:48:18Z

This PR has been migrated to a fork-based workflow: #35415

joneugster added WIP Work in progress t-meta Tactics, attributes or user commands CI Modifies the continuous integration setup or other automation labels Jan 29, 2025

joneugster mentioned this pull request Jan 30, 2025

feat(Cache): decompress downloaded files directly #21275

Closed

1 task

joneugster changed the title ~~refactor(Cache): cleanup cache~~ feat(Cache): enable partial cache in downstream projects Jan 30, 2025