feat(Cache): add miniget command, a minimal version of get

[grunweg]

Add a miniget command, a more minimal version of the get command. 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 runs lake exe cache get X/Y/Z.lean for 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.

---

[github-actions]

PR summary 6373327380

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ ofArray
+ ofList

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

[eric-wieser]

Why not just change get to behave in this way?

[grunweg]

Good idea! I have changed get (and get! and get-) to behave this way instead, if they are passed no arguments.
get with additional arguments is unchanged.

[eric-wieser]

Isn't this the same as lake exe cache get .?

[grunweg]

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

[grunweg]

By the way: running this in sphere-eversion confirms the code works. The new version only wants to download the cache for 2248 files, as opposed to 5833 files before.

[kim-em]

This step adds about a second to my lake exe cache get.

I think we should disable it if we're in Mathlib.

[grunweg]

This step adds about a second to my lake exe cache get.

I think we should disable it if we're in Mathlib.

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?

[eric-wieser]

Doesn't hashMemo already contain the dependency information?

[grunweg]

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.

[grunweg]

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