feat(Cache): add miniget command, a minimal version of get
#20568
Conversation
This downloads only cache files for every Lean file in some subdirectory.
grunweg
requested review from
kim-em,
Kha and
arthurpaulino
and removed request for
Kha
PR summary d3593d5f13Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo 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 No changes to technical debt.You can run this locally as
|
grunweg
changed the title
miniget commandget only download the cache for every file imported from a .lean file
|
Good idea! I have changed |
Cache/Main.lean
Outdated
| If no arguments are given, 'get', 'get!' and 'get-' download information about all files imported | ||
| in some .lean file in the current directory or a subdirectory thereof (ignoring .lake folders). |
There was a problem hiding this comment.
Isn't this the same as lake exe cache get .?
There was a problem hiding this comment.
Good question! Running this in sphere-eversion (i.e., a project downstream of mathlib) yields uncaught exception: Unknown package directory for . - so I would say no :-)
|
By the way: running this in |
|
This step adds about a second to my I think we should disable it if we're in Mathlib. |
kim-em
added
the
awaiting-author
Fair point. I don't think Cache knows about the current workspace, though - so don't see how to easily disable this. Perhaps it's better to make this a separate command, after all? What do you think? |
| @@ -83,8 +102,22 @@ def main (args : List String) : IO Unit := do | |||
| let goodCurl ← pure !curlArgs.contains (args.headD "") <||> validateCurl | |||
| if leanTarArgs.contains (args.headD "") then validateLeanTar | |||
| let get (args : List String) (force := false) (decompress := true) := do | |||
| let hashMap ← if args.isEmpty then pure hashMap else hashMemo.filterByFilePaths (toPaths args) | |||
There was a problem hiding this comment.
Doesn't hashMemo already contain the dependency information?
There was a problem hiding this comment.
It only contains this for all files it has memoized this for. This is mathlib and all extraRoots (i.e., arguments passed to it). Running just lake exe cache get in a dependent project does not parse the files in the downstream project.
There was a problem hiding this comment.
Can we reuse the same code that populates this in miniget?
|
Thinking about this again and having discussed with @fpvandoorn, it seems better to not change the default behaviour of cache, and make this a separate command instead. I'll re-instance |
grunweg
changed the title
get only download the cache for every file imported from a .lean fileminiget command, a minimal version of get
grunweg
removed
the
awaiting-author
- document two definitions - fix description of `get-` - mention `get-`, which also takes arguments Split from #20568.
- document two definitions - fix description of `get-` - mention `get-`, which also takes arguments Split from #20568.
leanprover-community-bot-assistant
added
the
merge-conflict
|
Closing in favour of #21238. |
Add a
minigetcommand, a more minimal version of thegetcommand. Instead of downloading the entire mathlib cache, it finds all .lean files in the current directory (excluding .lake directorires), reads all "import Mathlib X.Y.Z" lines in them, and runslake exe cache get X/Y/Z.leanfor these lines In short, this just downloads the cache necessary for a certain project.Inspired by a zulip comment of
kim-em.A (hopefully less controversial) part of #20567.