feat(Cache): enable partial cache in downstream projects

[joneugster]

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
• accept paths Mathlib/Init.lean and modules Mathlib.Init likewise
  feat(Cache): extend argument-parsing to allow module names, file names and directory names #21822
• accept folders in the form Mathlib/Data or Mathlib.Data and does a directory walk to find all.lean files therein
  feat(Cache): extend argument-parsing to allow module names, file names and directory names #21822,
  feat(Cache): Allow arguments of the form Mathlib.Data which correspond to a folder but not a file #21838
• throw error if sources contain a build loop.
  [Merged by Bors] - fix(Cache): error on import loop #21632
• cleanup
  • internally cache now works with the module names as keys (used paths before)
    refactor(Cache): use module name as key instead of unresolved file path #21834
  • eliminate need of parsing the lake_manifest.json, use the Lean search path from LEAN_SRC_PATH instead.
    [Merged by Bors] - refactor(Cache): use the Lean search path instead of lake-manifest to determine Mathlib root. #21666
  • eliminate most hard-coded file paths, generating them from the module name with Lean.findLean
    chore(Cache): remove unused hardcoded package directories #21818
  • add documentation

---

• depends on: refactor(Cache): rewrite getFileImports to use search path and return module names and source file location #21815
• depends on: feat(Cache): extend argument-parsing to allow module names, file names and directory names #21822
• depends on: refactor(Cache): use module name as key instead of unresolved file path #21834
• depends on: feat(Cache): Allow arguments of the form Mathlib.Data which correspond to a folder but not a file #21838

Follow-up PR:

• refactor(Cache): use module name for file hash instead of non-resolved file path #21842
• doc(Cache): add note about future improvements concerning file paths in leantar files #21848

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:

• depends on: [Merged by Bors] - fix(Cache): error on import loop #21632
• depends on: feat(Cache): add file Cache.Lean with helper functions and cleanup checkForToolchainMismatch #21663
• depends on: [Merged by Bors] - refactor(Cache): use the Lean search path instead of lake-manifest to determine Mathlib root. #21666
• depends on: [Merged by Bors] - doc(Cache): mention arguments to cache lookup help #21701
• depends on: [Merged by Bors] - doc(Cache): add docstring for CacheM.Context #21703
• depends on: [Merged by Bors] - chore(Cache): rename HashMap to ModuleHashMap #21704
• depends on: [Merged by Bors] - chore(Cache): use createDirAll #21705
• depends on: [Merged by Bors] - chore(Cache): stylistic change to not use default #21707
• depends on: [Merged by Bors] - doc(Cache/Hashing): add docstring for HashMemo #21711
• depends on: [Merged by Bors] - chore(Cache): cleanup getMathlibRoot #21750
• depends on: [Merged by Bors] - chore(Cache): move helper functions to Cache.Lean #21816
• depends on: [Merged by Bors] - refactor(Cache): refactor getPackageDir to not use manually provided package directories #21817
• depends on: chore(Cache): remove unused hardcoded package directories #21818
• depends on: [Merged by Bors] - chore(Cache): remove unnecessary imports #21830

[github-actions]

PR summary bf24f6145a

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ HashMemo.filterByRootModules
+ isFromMathlib
+ isInLeanCore
+ isPartOfMathlibCache
+ parseArgs
- HashMemo.filterByFilePaths
- PackageDirs
- getPackageDirs
- isPathFromMathlib
- toPaths

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