[SnirBroshi]

Instead of forbidding <>"/\|?* and whitespace, we forbid everything except for alphanumeric characters and _.

---

I checked downstream_repos.yml and all of them seem to comply except for SciLean with SciLean/Meta/Notation/Let', but they don't run this linter in CI. Also the Mathlib convention is a Prime suffix instead of '.

[github-actions]

PR summary 9a53dff8b8

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

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

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 9a53dff).

• +0 new declarations
• −0 removed declarations

No declaration differences.

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 9a53dff8b8
Reference commit 27402ab39e

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py 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).

[vihdzp]

I think you need to fix the tests.

[joneugster]

Looks good to me, thanks for the PR!

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by joneugster.

[Vierkantor]

I would say this linter is not super likely to be tripped and users can have good reasons to violate the rules. So I'd like to encourage us to focus on more immediately useful linters. But given the PR already exists, and matches unofficial policy within Mathlib I'm okay with being strict here and then allowing exceptions later if the style linter runs in other projects.

bors d+

[mathlib-bors]

✌️ SnirBroshi can now approve this pull request until 2026-11-11 11:27 UTC (in 2 weeks). To approve and merge, reply with bors r+. More detailed instructions are available here.

⚠️ This delegation only covers changes within Archive/**, Counterexamples/**, docs/**, DownstreamTest/**, Mathlib/**, MathlibTest/**, Wanted/**, widget/**, Archive.lean, Counterexamples.lean, docs.lean, Mathlib.lean, Wanted.lean; an author commit touching anything else will revoke it. Bors also revokes it if a later push changes too many files for it to check the full list — even if it stays within scope.

[vihdzp]

Usually I'd be more adamant about this. I think it's a shame that Mathlib embraces Unicode so openly, and yet we hesitate to use it outside of notation, even for the names of living people. But with file systems in particular... every OS stores them their own way, no one wants to deal with UTF-16, and lots of software (notably some LaTeX packages) will give obscure errors if you don't stick to pure ASCII. So I think being careful is warranted.

[SnirBroshi]

I would say this linter is not super likely to be tripped and users can have good reasons to violate the rules. So I'd like to encourage us to focus on more immediately useful linters.

The idea here is similar to the unicode linter: protect against unicode shenanigans.
There are lots of harmful unicode characters which we wouldn't want to exist in filenames, even without the issues with non-ASCII characters that Violeta mentioned above.
Adding exceptions is fine, but the point here was to switch from a denylist to an allowlist.

While I'm not sure if I (or Jon) will work on it soon, the plan is to extend both this and the unicode linter to all the files in Mathlib rather than just Lean modules imported by Mathlib.lean.

Thanks!
bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Build
• ci (staging) / Test and lint
• ci (staging) / Lint style
• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job