mathlib4/MathlibTest/HashCommandLinter.lean at master · Stars1233/mathlib4 · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
import Lean.Elab.GuardMsgs
import Mathlib.Tactic.AdaptationNote
import Mathlib.Tactic.Linter.HashCommandLinter

set_option linter.hashCommand true

section ignored_commands

-- As a consequence of https://github.com/leanprover/lean4/pull/5644, `#guard_msgs in`, even without a doc-string,
-- does not triggers the `#`-command linter.
#guard_msgs in
#guard_msgs in
#adaptation_note /-- testing that the hashCommand linter ignores this. -/

/-- info: 0 -/
#guard_msgs in
-- emits a message -- the linter allows it
#eval 0

/-- info: constructor PUnit.unit.{u} : PUnit -/
#guard_msgs in
-- emits a message -- the linter allows it
#print PUnit.unit

/-- info: 0 : Nat -/
#guard_msgs in
-- emits a message -- the linter allows it
#check 0

/--
warning: `#`-commands, such as '#eval', are not allowed in 'Mathlib'

Note: This linter can be disabled with `set_option linter.hashCommand false`
-/
#guard_msgs in
-- emits an empty message -- the linter allows it
#eval show Lean.MetaM _ from do guard true

-- not a `#`-command and not emitting a message: the linter allows it
run_cmd if false then Lean.logInfo "0"
end ignored_commands

section linted_commands
/--
warning: `#`-commands, such as '#guard', are not allowed in 'Mathlib'

Note: This linter can be disabled with `set_option linter.hashCommand false`
-/
#guard_msgs in
#guard true

set_option linter.unusedTactic false in
/--
warning: `#`-commands, such as '#check_tactic', are not allowed in 'Mathlib'

Note: This linter can be disabled with `set_option linter.hashCommand false`
-/
#guard_msgs in
#check_tactic True ~> True by skip

-- Testing that the linter enters `in` recursively.

/--
warning: `#`-commands, such as '#guard', are not allowed in 'Mathlib'

Note: This linter can be disabled with `set_option linter.hashCommand false`
-/
#guard_msgs in
variable (n : Nat) in
#guard true

/--
warning: `#`-commands, such as '#guard', are not allowed in 'Mathlib'

Note: This linter can be disabled with `set_option linter.hashCommand false`
-/
#guard_msgs in
open Nat in
variable (n : Nat) in
variable (n : Nat) in
#guard true

/--
warning: `#`-commands, such as '#guard', are not allowed in 'Mathlib'

Note: This linter can be disabled with `set_option linter.hashCommand false`
-/
#guard_msgs in
open Nat in
variable (n : Nat) in
#guard true

-- a test for `withSetOptionIn'`
set_option linter.unusedVariables false in
example {n : Nat} : Nat := 0

section warningAsError

-- if `warningAsError = true`, log an info (instead of a warning) on all `#`-commands, noisy or not
set_option warningAsError true
/--
info: 0
---
info: `#`-commands, such as '#eval', are not allowed in 'Mathlib' [linter.hashCommand]
-/
#guard_msgs in
#eval 0

/--
info: `#`-commands, such as '#guard', are not allowed in 'Mathlib' [linter.hashCommand]
-/
#guard_msgs in
#guard true

end warningAsError

end linted_commands