Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
joneugster wants to merge 3 commits into
base: master
Choose a base branch
from
Open

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
7fbff92
chore: move linter test files
joneugster May 22, 2026
86fd22c
review
joneugster May 22, 2026
7061f1e
review
joneugster May 23, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 5 additions & 5 deletions MathlibTest/DeprecatedModule.lean → ...er/DeprecatedModule/DeprecatedModule.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ deprecated_module (since := "2025-04-10")
/--
info: Deprecated modules

'MathlibTest.DeprecatedModule' deprecates to
'MathlibTest.Linter.DeprecatedModule.DeprecatedModule' deprecates to
#[Mathlib.Tactic.Linter.DocPrime, Mathlib.Tactic.Linter.DocString]
with no message
-/
Expand All @@ -20,11 +20,11 @@ deprecated_module "We can also give more details about the deprecation" (since :
/--
info: Deprecated modules

'MathlibTest.DeprecatedModule' deprecates to
'MathlibTest.Linter.DeprecatedModule.DeprecatedModule' deprecates to
#[Mathlib.Tactic.Linter.DocPrime, Mathlib.Tactic.Linter.DocString]
with message 'We can also give more details about the deprecation'

'MathlibTest.DeprecatedModule' deprecates to
'MathlibTest.Linter.DeprecatedModule.DeprecatedModule' deprecates to
#[Mathlib.Tactic.Linter.DocPrime, Mathlib.Tactic.Linter.DocString]
with no message
-/
Expand All @@ -42,11 +42,11 @@ deprecated_module "Text" (since := "2025-02-31")
/--
info: Deprecated modules

'MathlibTest.DeprecatedModule' deprecates to
'MathlibTest.Linter.DeprecatedModule.DeprecatedModule' deprecates to
#[Mathlib.Tactic.Linter.DocPrime, Mathlib.Tactic.Linter.DocString]
with message 'We can also give more details about the deprecation'

'MathlibTest.DeprecatedModule' deprecates to
'MathlibTest.Linter.DeprecatedModule.DeprecatedModule' deprecates to
#[Mathlib.Tactic.Linter.DocPrime, Mathlib.Tactic.Linter.DocString]
with no message
-/
Expand Down
4 changes: 2 additions & 2 deletions MathlibTest/DeprecatedModuleAllTest.lean → ...ecatedModule/DeprecatedModuleAllTest.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
module

import all MathlibTest.DeprecatedModuleNew
import all MathlibTest.Linter.DeprecatedModule.DeprecatedModuleNew
Copy link
Copy Markdown
Contributor

@grunweg grunweg May 22, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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


/--
warning: Testing public import deprecation
'MathlibTest.DeprecatedModuleNew' has been deprecated: please replace this import by
'MathlibTest.Linter.DeprecatedModule.DeprecatedModuleNew' has been deprecated: please replace this import by
import Mathlib.Tactic.Linter.DocPrime
import Mathlib.Tactic.Linter.DocString
Expand Down
4 changes: 2 additions & 2 deletions MathlibTest/DeprecatedModuleMetaTest.lean → ...catedModule/DeprecatedModuleMetaTest.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
module

meta import MathlibTest.DeprecatedModuleNew
meta import MathlibTest.Linter.DeprecatedModule.DeprecatedModuleNew
Copy link
Copy Markdown
Contributor

@grunweg grunweg May 22, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

MetaImport.lean?


/--
warning: Testing public import deprecation
'MathlibTest.DeprecatedModuleNew' has been deprecated: please replace this import by
'MathlibTest.Linter.DeprecatedModule.DeprecatedModuleNew' has been deprecated: please replace this import by
import Mathlib.Tactic.Linter.DocPrime
import Mathlib.Tactic.Linter.DocString
Expand Down
0 MathlibTest/DeprecatedModuleNew.lean → ...DeprecatedModule/DeprecatedModuleNew.lean
View file
Open in desktop
Copy link
Copy Markdown
Contributor

@grunweg grunweg May 22, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

File renamed without changes.
4 changes: 2 additions & 2 deletions ...bTest/DeprecatedModulePublicMetaTest.lean → ...odule/DeprecatedModulePublicMetaTest.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
module

public meta import MathlibTest.DeprecatedModuleNew
public meta import MathlibTest.Linter.DeprecatedModule.DeprecatedModuleNew
Copy link
Copy Markdown
Contributor

@grunweg grunweg May 22, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

PublicMetaImport.lean maybe?


/--
warning: Testing public import deprecation
'MathlibTest.DeprecatedModuleNew' has been deprecated: please replace this import by
'MathlibTest.Linter.DeprecatedModule.DeprecatedModuleNew' has been deprecated: please replace this import by
import Mathlib.Tactic.Linter.DocPrime
import Mathlib.Tactic.Linter.DocString
Expand Down
4 changes: 2 additions & 2 deletions MathlibTest/DeprecatedModulePublicTest.lean → ...tedModule/DeprecatedModulePublicTest.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
module

public import MathlibTest.DeprecatedModuleNew
public import MathlibTest.Linter.DeprecatedModule.DeprecatedModuleNew
Copy link
Copy Markdown
Contributor

@grunweg grunweg May 22, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

PublicModule.lean?


/--
warning: Testing public import deprecation
'MathlibTest.DeprecatedModuleNew' has been deprecated: please replace this import by
'MathlibTest.Linter.DeprecatedModule.DeprecatedModuleNew' has been deprecated: please replace this import by
import Mathlib.Tactic.Linter.DocPrime
import Mathlib.Tactic.Linter.DocString
Expand Down
6 changes: 3 additions & 3 deletions MathlibTest/DeprecatedModuleTest.lean → ...eprecatedModule/DeprecatedModuleTest.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
import MathlibTest.DeprecatedModule
import MathlibTest.Linter.DeprecatedModule.DeprecatedModule

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

@grunweg grunweg May 22, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

... and find a good name here.

'MathlibTest.Linter.DeprecatedModule.DeprecatedModule' has been deprecated: please replace this import by

import Mathlib.Tactic.Linter.DocPrime
import Mathlib.Tactic.Linter.DocString
Expand All @@ -11,7 +11,7 @@ import Mathlib.Tactic.Linter.DocString
Note: This linter can be disabled with `set_option linter.deprecated.module false`
---
warning:
'MathlibTest.DeprecatedModule' has been deprecated: please replace this import by
'MathlibTest.Linter.DeprecatedModule.DeprecatedModule' has been deprecated: please replace this import by

import Mathlib.Tactic.Linter.DocPrime
import Mathlib.Tactic.Linter.DocString
Expand Down
0 MathlibTest/DeprecatedSyntaxLinter.lean → MathlibTest/Linter/DeprecatedSyntax.lean
View file
Open in desktop
Comment thread
joneugster marked this conversation as resolved.
File renamed without changes.
0 MathlibTest/DocPrime.lean → MathlibTest/Linter/DocPrime.lean
View file
Open in desktop
File renamed without changes.
0 MathlibTest/DocString.lean → MathlibTest/Linter/DocString.lean
View file
Open in desktop
File renamed without changes.
0 MathlibTest/EmptyLine.lean → MathlibTest/Linter/EmptyLine.lean
View file
Open in desktop
File renamed without changes.
0 MathlibTest/FlexibleLinter.lean → MathlibTest/Linter/FlexibleLinter.lean
View file
Open in desktop
File renamed without changes.
0 MathlibTest/ForbiddenModuleNames.lean → MathlibTest/Linter/ForbiddenModuleNames.lean
View file
Open in desktop
File renamed without changes.
0 MathlibTest/ImportHeavyFlexibleLinter.lean → ...est/Linter/ImportHeavyFlexibleLinter.lean
View file
Open in desktop
File renamed without changes.
0 MathlibTest/ModuleCasing.lean → MathlibTest/Linter/ModuleCasing.lean
View file
Open in desktop
File renamed without changes.
0 MathlibTest/oldObtain.lean → MathlibTest/Linter/OldObtain.lean
View file
Open in desktop
File renamed without changes.
0 ...t/PrivateModuleLinter/hasOnlyPrivate.lean → .../Linter/PrivateModule/HasOnlyPrivate.lean
View file
Open in desktop
File renamed without changes.
0 ...ibTest/PrivateModuleLinter/hasPublic.lean → ...bTest/Linter/PrivateModule/HasPublic.lean
View file
Open in desktop
File renamed without changes.
0 ...bTest/PrivateModuleLinter/importOnly.lean → ...Test/Linter/PrivateModule/ImportOnly.lean
View file
Open in desktop
File renamed without changes.
0 ...bTest/PrivateModuleLinter/initialize.lean → ...Test/Linter/PrivateModule/Initialize.lean
View file
Open in desktop
File renamed without changes.
0 ...ibTest/PrivateModuleLinter/nonModule.lean → ...bTest/Linter/PrivateModule/NonModule.lean
View file
Open in desktop
File renamed without changes.
8 changes: 4 additions & 4 deletions ...ibTest/PrivateModuleLinter/notation3.lean → ...bTest/Linter/PrivateModule/Notation3.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,10 +10,10 @@ local notation3 "MyList[" (x", "* => foldr (a b => List.cons a b) List.nil) "]"
/- Check that we have indeed created declarations, and aren't not linting just due to being an
empty file: -/
/--
info: [_private.MathlibTest.PrivateModuleLinter.notation3.0.«_aux_MathlibTest_PrivateModuleLinter_notation3___delab_app__private_MathlibTest_PrivateModuleLinter_notation3_0_termMyList[_,]_2»,
_private.MathlibTest.PrivateModuleLinter.notation3.0.«termMyList[_,]»,
_private.MathlibTest.PrivateModuleLinter.notation3.0.«_aux_MathlibTest_PrivateModuleLinter_notation3___delab_app__private_MathlibTest_PrivateModuleLinter_notation3_0_termMyList[_,]_1»,
_private.MathlibTest.PrivateModuleLinter.notation3.0.«_aux_MathlibTest_PrivateModuleLinter_notation3___macroRules__private_MathlibTest_PrivateModuleLinter_notation3_0_termMyList[_,]_1»]
info: [_private.MathlibTest.Linter.PrivateModule.Notation3.0.«termMyList[_,]»,
_private.MathlibTest.Linter.PrivateModule.Notation3.0.«_aux_MathlibTest_Linter_PrivateModule_Notation3___macroRules__private_MathlibTest_Linter_PrivateModule_Notation3_0_termMyList[_,]_1»,
_private.MathlibTest.Linter.PrivateModule.Notation3.0.«_aux_MathlibTest_Linter_PrivateModule_Notation3___delab_app__private_MathlibTest_Linter_PrivateModule_Notation3_0_termMyList[_,]_2»,
_private.MathlibTest.Linter.PrivateModule.Notation3.0.«_aux_MathlibTest_Linter_PrivateModule_Notation3___delab_app__private_MathlibTest_Linter_PrivateModule_Notation3_0_termMyList[_,]_1»]
-/
#guard_msgs in
run_cmd do
Expand Down
0 ...st/PrivateModuleLinter/reservedName1.lean → ...t/Linter/PrivateModule/ReservedName1.lean
View file
Open in desktop
File renamed without changes.
2 changes: 1 addition & 1 deletion ...st/PrivateModuleLinter/reservedName2.lean → ...t/Linter/PrivateModule/ReservedName2.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ module

import Mathlib.Init
import all Mathlib.Tactic.Linter.PrivateModule
public import MathlibTest.PrivateModuleLinter.reservedName1
public import MathlibTest.Linter.PrivateModule.ReservedName1

open Lean

Expand Down
Loading