feat(Cache): Allow arguments of the form `Mathlib.Data.+` which correspond to a folder but not a file by joneugster · Pull Request #21838 · leanprover-community/mathlib4

joneugster · 2025-02-13T17:58:33Z

Extend lake exe cache get to get cache for all files inside a specified folder, as well as the dependencies of these files.

his can be used as lake exe cache get Mathlib/Data/ or lake exe cache get Mathlib.Data.+. There is also the syntax lake exe cache get Mathlib.Data.* which means either file or folder.

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

mergify · 2025-02-13T17:59:16Z

⚠️ The sha of the head commit of this PR conflicts with #21834. Mergify cannot evaluate rules on this PR. ⚠️

github-actions · 2025-02-13T17:59:29Z

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

No declarations were harmed in the making of this PR! 🐙

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).

joneugster · 2025-03-05T09:58:13Z

Note to myself: check if something like the following is needed:

  -- TODO: This could be `(argₛ : FilePath).normalize` if the comment there got addressed
  -- (which says "TODO: normalize `a/`, `a//b`, etc.")
  let arg : FilePath := System.mkFilePath <| (argₛ : FilePath).components.filter (· != "")

mathlib4-dependent-issues-bot · 2025-04-03T02:30:10Z

This PR/issue depends on:

~~[Merged by Bors] - refactor(Cache): use module name as key instead of unresolved file path #21834~~
By Dependent Issues (🤖). Happy coding!

joneugster · 2025-04-04T14:01:08Z

I've tested this with two lake new CacheTest math.lean, one setting mathlib to this branch, one setting it to a local copy at ../../mathlib4. In both cases lake exe cache get Mathlib.Data seemed to work just fine.

eric-wieser · 2025-05-11T21:00:59Z


 1. `Mathlib.Algebra.Fields.Basic`: there exists such a Lean file
-2. `Mathlib.Algebra.Fields`: no Lean file exists but a folder (TODO)
+2. `Mathlib.Algebra.Fields`: no Lean file exists but a folder


I think we should match lake here, and use .+ syntax. Otherwise we're stuck if both Foo/Bar.lean and Foo/Bar/Baz.lean exist.

We could also support .* syntax, which would mean "load both of the above", though of course the user has to remember to escape it in some shells.

Implemented both your suggestions

leanprover-community-bot-assistant · 2025-07-13T19:38:48Z

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

eric-wieser · 2026-01-31T21:20:27Z

  else
    -- provided a module
-    let mod := argₛ.toName
+    -- user might provide `.*` or `.+` to include folders


Perhaps this shoudl be parsed with Lake.Glob.ofString??

(and then use glob.forEachModuleIn)

That's a good idea. However, if I understand things correctly, I cannot import Lake.Glob.ofString? since Cache is not a module yet and Lake.Glob.ofString? is not public.

I could offer to create a follow-up PR (once this PR has been merged) to convert Cache into a module and incorporate this suggestion there.

I've added this as TODO comment

You can use open private from batteries I think,

Implemented your suggestion 👍

joneugster · 2026-02-16T16:47:26Z

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

joneugster changed the base branch from master to eugster/cache_use_mod_instead_of_path February 13, 2025 17:59

joneugster mentioned this pull request Feb 13, 2025

feat(Cache): enable partial cache in downstream projects #21238

Closed

17 tasks

joneugster added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-meta Tactics, attributes or user commands CI Modifies the continuous integration setup or other automation labels Feb 13, 2025

joneugster force-pushed the eugster/cache_pseudo_module_args branch from 8c89c93 to 053bfae Compare February 13, 2025 18:12

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 13, 2025

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 14, 2025

joneugster changed the base branch from eugster/cache_use_mod_instead_of_path to master February 24, 2025 16:23

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 27, 2025

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 28, 2025

joneugster changed the base branch from master to eugster/cache_use_mod_instead_of_path March 7, 2025 09:29

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 31, 2025

eric-wieser reviewed Mar 31, 2025

View reviewed changes

Comment thread Cache/IO.lean Outdated

eric-wieser reviewed Mar 31, 2025

View reviewed changes

Comment thread Cache/IO.lean Outdated

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Apr 1, 2025

joneugster changed the base branch from eugster/cache_use_mod_instead_of_path to master April 1, 2025 10:17

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Apr 3, 2025

joneugster added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 4, 2025

joneugster removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 4, 2025

eric-wieser reviewed May 11, 2025

View reviewed changes

grunweg added the awaiting-author A reviewer has asked the author a question or requested changes. label May 22, 2025

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 13, 2025

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 31, 2026

joneugster removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 31, 2026

joneugster changed the title ~~feat(Cache): Allow arguments of the form Mathlib.Data which correspond to a folder but not a file~~ feat(Cache): Allow arguments of the form Mathlib.Data.+ which correspond to a folder but not a file Jan 31, 2026

eric-wieser reviewed Jan 31, 2026

View reviewed changes

joneugster assigned eric-wieser Feb 7, 2026

squashed changes

068bac4

joneugster force-pushed the eugster/cache_pseudo_module_args branch from 677ebdc to 068bac4 Compare February 15, 2026 00:35

cleanup

a062dd9

This was referenced Feb 15, 2026

refactor(Cache): use module name for file hash instead of non-resolved file path #21842

Closed

feat(Cache): Allow arguments of the form Mathlib.Data.+ which correspond to a folder but not a file #35414

Open

joneugster added the migrated-to-fork label Feb 16, 2026

joneugster closed this Feb 16, 2026

Conversation

joneugster commented Feb 13, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mergify bot commented Feb 13, 2025

Uh oh!

github-actions bot commented Feb 13, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 88bb6d226a

Import changes for modified files

Declarations diff

Uh oh!

joneugster commented Mar 5, 2025

Uh oh!

Uh oh!

Uh oh!

mathlib4-dependent-issues-bot commented Apr 3, 2025

Uh oh!

joneugster commented Apr 4, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

leanprover-community-bot-assistant commented Jul 13, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

joneugster commented Feb 16, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

joneugster commented Feb 13, 2025 •

edited

Loading

github-actions bot commented Feb 13, 2025 •

edited

Loading