PR summary 7d9358ee9d

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/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

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

note: file Mathlib/Tactic/LinearCombination'.lean` was renamed to `Mathlib/Tactic/LinearCombinationPrime.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file MathlibTest/linear_combination'.lean` was renamed to `MathlibTest/linear_combination_prime.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

Thank you for addressing this small but annoying developer experience issue.

This closes #25244 .

After this change all filenames in the repo will match on ^[a-zA-Z0-9_./-]*$:

% git ls-files | grep -vE '^[a-zA-Z0-9_./-]*$'
Mathlib/Tactic/LinearCombination'.lean
MathlibTest/linear_combination'.lean

The ' character in filenames causes shell escaping issues in scripts (any find ... -name '*.lean' or similar pattern needs careful quoting to handle these files correctly).

My take on this is that we should avoid writing bash scripts in the first place, either because Python is by all reasonable metrics a safer language, or because we should be dog-fooding ourselves writing our scripts in Lean instead.

While I wouldn't say that keeping these primes is the correct strategy to increase the quality of the mathlib scripts, it probably is an effective one.

Filenames are infrastructure. Infrastructure should be maximally boring and frictionless.

Avoiding ' in filenames isn’t about tool preference: it’s about minimizing edge cases in a shared ecosystem.

Even with Python or Lean tooling, users still interact with Git and shells directly, and quoting issues remain.

The ' character in filenames causes shell escaping issues in scripts (any find ... -name '*.lean' or similar pattern needs careful quoting to handle these files correctly).

My take on this is that we should avoid writing bash scripts in the first place, either because Python is by all reasonable metrics a safer language, or because we should be dog-fooding ourselves writing our scripts in Lean instead.

While I wouldn't say that keeping these primes is the correct strategy to increase the quality of the mathlib scripts, it probably is an effective one.

I presume this is tongue-in-cheek and not an actual objection.

The deprecated module files would need to have ' in their filenames, which would be caught by the new linter added in this PR. So no deprecation for these.

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