chore: move test files and recapitalise file names (part 2) by joneugster · Pull Request #39681 · leanprover-community/mathlib4

joneugster · 2026-05-22T03:31:32Z

Moves all test files about linters to a folder Linter and capitalises their names.

github-actions · 2026-05-22T03:32:50Z

PR summary 86fd22c480

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

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.

No changes to strong technical debt.

No changes to weak technical debt.

note: file MathlibTest/PrivateModuleLinter/importOnly.lean` was renamed to `MathlibTest/Linter/PrivateModule/ImportOnly.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

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

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

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

note: file MathlibTest/PrivateModuleLinter/reservedName2.lean` was renamed to `MathlibTest/Linter/PrivateModule/ReservedName2.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file MathlibTest/PrivateModuleLinter/initialize.lean` was renamed to `MathlibTest/Linter/PrivateModule/Initialize.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

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

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

note: file MathlibTest/PrivateModuleLinter/reservedName1.lean` was renamed to `MathlibTest/Linter/PrivateModule/ReservedName1.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file MathlibTest/PrivateModuleLinter/hasOnlyPrivate.lean` was renamed to `MathlibTest/Linter/PrivateModule/HasOnlyPrivate.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

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

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

note: file MathlibTest/PrivateModuleLinter/notation3.lean` was renamed to `MathlibTest/Linter/PrivateModule/Notation3.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

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

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

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

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

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

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

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

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

note: file MathlibTest/PrivateModuleLinter/hasPublic.lean` was renamed to `MathlibTest/Linter/PrivateModule/HasPublic.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

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

note: file MathlibTest/PrivateModuleLinter/nonModule.lean` was renamed to `MathlibTest/Linter/PrivateModule/NonModule.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

grunweg

Thanks. Some tweaks that would be good:

keep ValidatePRTitle where it is, maybe? (It is not a syntax or environment linter.)
Linter/PrivateModuleLinter can become Linter/PrivateModule, I guess?
(Only skimmed the rest so far.)

joneugster · 2026-05-22T09:51:18Z

Done that :)

grunweg

Thanks. A few more (kind of pre-existing) comments.
awaiting-author

grunweg · 2026-05-22T10:17:21Z

 import Mathlib.Tactic.Linter.DocPrime
 import Mathlib.Tactic.Linter.DocString

 deprecated_module (since := "2025-04-10")


How about DeprecatedModule/Basic.lean (or so)?

grunweg · 2026-05-22T10:17:45Z

 module

-import all MathlibTest.DeprecatedModuleNew
+import all MathlibTest.Linter.DeprecatedModule.DeprecatedModuleNew


and ImportAll.lean here --- perhaps with adding a brief module doc-string what this tests?

grunweg · 2026-05-22T10:17:55Z

 module

-meta import MathlibTest.DeprecatedModuleNew
+meta import MathlibTest.Linter.DeprecatedModule.DeprecatedModuleNew


MetaImport.lean?

grunweg · 2026-05-22T10:18:32Z

Not sure how to name this one... can you do the git archeology here? Sorry...

grunweg · 2026-05-22T10:18:44Z

 module

-public meta import MathlibTest.DeprecatedModuleNew
+public meta import MathlibTest.Linter.DeprecatedModule.DeprecatedModuleNew


PublicMetaImport.lean maybe?

grunweg · 2026-05-22T10:18:58Z

 module

-public import MathlibTest.DeprecatedModuleNew
+public import MathlibTest.Linter.DeprecatedModule.DeprecatedModuleNew


PublicModule.lean?

grunweg · 2026-05-22T10:19:19Z


 /--
 warning: We can also give more details about the deprecation
-'MathlibTest.DeprecatedModule' has been deprecated: please replace this import by


... and find a good name here.

grunweg · 2026-05-22T10:20:03Z

Should this be DeprecatedSyntax.lean instead (and perhaps the linter file also renamed)?

joneugster mentioned this pull request May 22, 2026

chore: move test files and recapitalise filennames #39676

Open

3 tasks

github-actions Bot added the file-removed A Lean module was (re)moved without a `deprecated_module` annotation label May 22, 2026

chore: move linter test files

7fbff92

joneugster force-pushed the test/cleanup-tests-004 branch from 67f7481 to 7fbff92 Compare May 22, 2026 03:38

grunweg reviewed May 22, 2026

View reviewed changes

grunweg added the awaiting-author A reviewer has asked the author a question or requested changes. label May 22, 2026

grunweg self-assigned this May 22, 2026

review

86fd22c

joneugster removed the awaiting-author A reviewer has asked the author a question or requested changes. label May 22, 2026

grunweg reviewed May 22, 2026

View reviewed changes

grunweg added the awaiting-author A reviewer has asked the author a question or requested changes. label May 22, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

chore: move test files and recapitalise file names (part 2)#39681

chore: move test files and recapitalise file names (part 2)#39681
joneugster wants to merge 2 commits into
leanprover-community:masterfrom
joneugster:test/cleanup-tests-004

joneugster commented May 22, 2026

Uh oh!

github-actions Bot commented May 22, 2026 •

edited

Loading

Declarations diff

Uh oh!

grunweg left a comment

Uh oh!

joneugster commented May 22, 2026

Uh oh!

grunweg left a comment

Uh oh!

grunweg May 22, 2026

Uh oh!

grunweg May 22, 2026

Uh oh!

grunweg May 22, 2026

Uh oh!

grunweg May 22, 2026

Uh oh!

grunweg May 22, 2026

Uh oh!

grunweg May 22, 2026

Uh oh!

grunweg May 22, 2026

Uh oh!

grunweg May 22, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

joneugster commented May 22, 2026

Uh oh!

github-actions Bot commented May 22, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 86fd22c480

Import changes for modified files

Declarations diff

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

joneugster commented May 22, 2026

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

github-actions Bot commented May 22, 2026 •

edited

Loading