Skip to content

Commit 526b330

Browse files
joneugsterjoneugster
committed
chore: move test files and recapitalise file names (part 2) (leanprover-community#39681)
Moves all test files about linters to a folder `Linter` and capitalises their names.
1 parent ff7e349 commit 526b330

26 files changed

Lines changed: 39 additions & 47 deletions

‎MathlibTest/DeprecatedModuleTest.lean‎

Lines changed: 0 additions & 25 deletions
This file was deleted.

MathlibTest/DeprecatedModule.lean renamed to MathlibTest/Linter/DeprecatedModule/Basic.lean

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ deprecated_module (since := "2025-04-10")
77
/--
88
info: Deprecated modules
99
10-
'MathlibTest.DeprecatedModule' deprecates to
10+
'MathlibTest.Linter.DeprecatedModule.Basic' deprecates to
1111
#[Mathlib.Tactic.Linter.DocPrime, Mathlib.Tactic.Linter.DocString]
1212
with no message
1313
-/
@@ -20,13 +20,13 @@ deprecated_module "We can also give more details about the deprecation" (since :
2020
/--
2121
info: Deprecated modules
2222
23-
'MathlibTest.DeprecatedModule' deprecates to
23+
'MathlibTest.Linter.DeprecatedModule.Basic' deprecates to
2424
#[Mathlib.Tactic.Linter.DocPrime, Mathlib.Tactic.Linter.DocString]
25-
with message 'We can also give more details about the deprecation'
25+
with no message
2626
27-
'MathlibTest.DeprecatedModule' deprecates to
27+
'MathlibTest.Linter.DeprecatedModule.Basic' deprecates to
2828
#[Mathlib.Tactic.Linter.DocPrime, Mathlib.Tactic.Linter.DocString]
29-
with no message
29+
with message 'We can also give more details about the deprecation'
3030
-/
3131
#guard_msgs in
3232
#show_deprecated_modules
@@ -42,13 +42,13 @@ deprecated_module "Text" (since := "2025-02-31")
4242
/--
4343
info: Deprecated modules
4444
45-
'MathlibTest.DeprecatedModule' deprecates to
45+
'MathlibTest.Linter.DeprecatedModule.Basic' deprecates to
4646
#[Mathlib.Tactic.Linter.DocPrime, Mathlib.Tactic.Linter.DocString]
47-
with message 'We can also give more details about the deprecation'
47+
with no message
4848
49-
'MathlibTest.DeprecatedModule' deprecates to
49+
'MathlibTest.Linter.DeprecatedModule.Basic' deprecates to
5050
#[Mathlib.Tactic.Linter.DocPrime, Mathlib.Tactic.Linter.DocString]
51-
with no message
51+
with message 'We can also give more details about the deprecation'
5252
-/
5353
#guard_msgs in
5454
#show_deprecated_modules

MathlibTest/DeprecatedModuleAllTest.lean renamed to MathlibTest/Linter/DeprecatedModule/ImportAsAll.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
module
22

3-
import all MathlibTest.DeprecatedModuleNew
3+
import all MathlibTest.Linter.DeprecatedModule.ImportBase
44

55
/--
66
warning: Testing public import deprecation
7-
'MathlibTest.DeprecatedModuleNew' has been deprecated: please replace this import by
7+
'MathlibTest.Linter.DeprecatedModule.ImportBase' has been deprecated: please replace this import by
88
99
import Mathlib.Tactic.Linter.DocPrime
1010
import Mathlib.Tactic.Linter.DocString

MathlibTest/DeprecatedModuleMetaTest.lean renamed to MathlibTest/Linter/DeprecatedModule/ImportAsMeta.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
module
22

3-
meta import MathlibTest.DeprecatedModuleNew
3+
meta import MathlibTest.Linter.DeprecatedModule.ImportBase
44

55
/--
66
warning: Testing public import deprecation
7-
'MathlibTest.DeprecatedModuleNew' has been deprecated: please replace this import by
7+
'MathlibTest.Linter.DeprecatedModule.ImportBase' has been deprecated: please replace this import by
88
99
import Mathlib.Tactic.Linter.DocPrime
1010
import Mathlib.Tactic.Linter.DocString

‎MathlibTest/Linter/DeprecatedModule/ImportAsPlain.lean‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
import MathlibTest.Linter.DeprecatedModule.ImportBase
2+
3+
/--
4+
warning: Testing public import deprecation
5+
'MathlibTest.Linter.DeprecatedModule.ImportBase' has been deprecated: please replace this import by
6+
7+
import Mathlib.Tactic.Linter.DocPrime
8+
import Mathlib.Tactic.Linter.DocString
9+
10+
11+
Note: This linter can be disabled with `set_option linter.deprecated.module false`
12+
-/
13+
#guard_msgs in
14+
/-!
15+
This file imports a deprecated module.
16+
-/

MathlibTest/DeprecatedModulePublicTest.lean renamed to MathlibTest/Linter/DeprecatedModule/ImportAsPublic.lean

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,11 @@
11
module
22

3-
public import MathlibTest.DeprecatedModuleNew
3+
public import MathlibTest.Linter.DeprecatedModule.ImportBase
4+
45

56
/--
67
warning: Testing public import deprecation
7-
'MathlibTest.DeprecatedModuleNew' has been deprecated: please replace this import by
8+
'MathlibTest.Linter.DeprecatedModule.ImportBase' has been deprecated: please replace this import by
89
910
import Mathlib.Tactic.Linter.DocPrime
1011
import Mathlib.Tactic.Linter.DocString

MathlibTest/DeprecatedModuleNew.lean renamed to MathlibTest/Linter/DeprecatedModule/ImportBase.lean

File renamed without changes.

MathlibTest/DeprecatedModulePublicMetaTest.lean renamed to MathlibTest/Linter/DeprecatedModule/ImportsAsPublicMeta.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
module
22

3-
public meta import MathlibTest.DeprecatedModuleNew
3+
public meta import MathlibTest.Linter.DeprecatedModule.ImportBase
44

55
/--
66
warning: Testing public import deprecation
7-
'MathlibTest.DeprecatedModuleNew' has been deprecated: please replace this import by
7+
'MathlibTest.Linter.DeprecatedModule.ImportBase' has been deprecated: please replace this import by
88
99
import Mathlib.Tactic.Linter.DocPrime
1010
import Mathlib.Tactic.Linter.DocString

MathlibTest/DeprecatedSyntaxLinter.lean renamed to MathlibTest/Linter/DeprecatedSyntax.lean

File renamed without changes.

MathlibTest/DocPrime.lean renamed to MathlibTest/Linter/DocPrime.lean

File renamed without changes.

0 commit comments

Comments
 (0)