Comments from Original PR #21838

This section contains 3 comment(s) from the original PR, excluding bot comments.

@mergify (2025-02-13 17:59 UTC):
⚠️ The sha of the head commit of this PR conflicts with #21834. Mergify cannot evaluate rules on this PR. ⚠️

@joneugster (2025-03-05 09:58 UTC):
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 (· != "")

@joneugster (2025-04-04 14:01 UTC):
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.

PR summary 88bb6d226a

Import changes for modified files

No significant changes to the import graph

Declarations diff

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

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

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