Skip to content

Commit 788e365

Browse files
alvinyltalvinylt
committed
Add linter tests
1 parent add4d25 commit 788e365

1 file changed

Lines changed: 172 additions & 0 deletions

File tree

‎Iris/IrisTest/Linter.lean‎

Lines changed: 172 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,172 @@
1+
/-
2+
Copyright (c) The Iris-Lean Contributors
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Alvin Tang
5+
-/
6+
module
7+
8+
meta import Iris.Std.Linter.Style
9+
meta import Iris.Std.Linter.DupNamespace
10+
meta import Iris.Std.Linter.Whitespace
11+
12+
@[expose] public section
13+
14+
namespace IrisTest
15+
16+
/-! ## `linter.iris.style.cdot` -/
17+
18+
/- Tests that a focusing dot typed as a plain `.` is flagged. -/
19+
/-- warning: Please, use '·' (typed as `\.`) instead of '.' as 'cdot'. -/
20+
#guard_msgs (whitespace := lax, substring := true) in
21+
example : True := by
22+
. trivial
23+
24+
/- Tests that a cdot sitting alone on its line is flagged, even when typed correctly. -/
25+
/-- warning: This central dot `·` is isolated; please merge it with the next line. -/
26+
#guard_msgs (whitespace := lax, substring := true) in
27+
example : True := by
28+
·
29+
trivial
30+
31+
/-! ## `linter.iris.style.dollarSyntax` -/
32+
33+
/- Tests that `$` used as the pipe operator is flagged. -/
34+
/-- warning: Please use '<|' instead of '$' for the pipe operator. -/
35+
#guard_msgs (whitespace := lax, substring := true) in
36+
example : Nat := id $ 0
37+
38+
/-! ## `linter.iris.style.lambdaSyntax` -/
39+
40+
/- Tests that `λ` is flagged. -/
41+
/--
42+
warning: Please use 'fun' and not 'λ' to define anonymous functions.
43+
Following the Mathlib style guide, the 'λ' syntax is deprecated in Iris-Lean.
44+
-/
45+
#guard_msgs (whitespace := lax, substring := true) in
46+
set_option linter.iris.style.lambdaSyntax true in
47+
example : Nat → Nat := λ n => n
48+
49+
/-! ## `linter.iris.style.nameCheck` -/
50+
51+
/- Tests that a declaration name containing `__` is flagged. -/
52+
/--
53+
warning: The declaration 'foo__bar' contains '__', which does not follow the Iris-Lean naming
54+
conventions. Consider using single underscores instead.
55+
-/
56+
#guard_msgs (whitespace := lax, substring := true) in
57+
set_option linter.iris.style.nameCheck true in
58+
theorem foo__bar : True := trivial
59+
60+
/-! ## `linter.iris.style.openClassical` -/
61+
62+
section OpenClassical
63+
64+
/- Tests that an unscoped `open Classical` is flagged. -/
65+
/--
66+
warning: please avoid 'open (scoped) Classical' statements: this can hide theorem statements
67+
which would be better stated with explicit decidability statements.
68+
Instead, use `open Classical in` for definitions or instances, the `classical` tactic for proofs.
69+
For theorem statements, either add missing decidability assumptions or use `open Classical in`.
70+
-/
71+
#guard_msgs (whitespace := lax, substring := true) in
72+
open Classical
73+
74+
/- Tests that `open scoped Classical` is flagged too. -/
75+
/--
76+
warning: please avoid 'open (scoped) Classical' statements: this can hide theorem statements
77+
which would be better stated with explicit decidability statements.
78+
Instead, use `open Classical in` for definitions or instances, the `classical` tactic for proofs.
79+
For theorem statements, either add missing decidability assumptions or use `open Classical in`.
80+
-/
81+
#guard_msgs (whitespace := lax, substring := true) in
82+
open scoped Classical
83+
84+
/- Tests that `open Classical in` is accepted. -/
85+
#guard_msgs in
86+
open Classical in
87+
theorem openClassicalScoped : True := trivial
88+
89+
end OpenClassical
90+
91+
/-! ## `linter.iris.style.show` -/
92+
93+
/- Tests that a `show` which changes the goal is flagged. -/
94+
/--
95+
warning: The `show` tactic should only be used to indicate intermediate goal states for
96+
readability.
97+
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.
98+
-/
99+
#guard_msgs (whitespace := lax, substring := true) in
100+
example : id True := by
101+
show True
102+
trivial
103+
104+
/- Tests that a `show` which restates the goal verbatim is accepted. -/
105+
#guard_msgs in
106+
example : True := by
107+
show True
108+
trivial
109+
110+
/-! ## `linter.iris.dupNamespace` -/
111+
112+
namespace Dup
113+
114+
/- Tests the single-duplicate branch of the linter. -/
115+
/--
116+
warning: The namespace `Dup` is duplicated in the declaration `IrisTest.Dup.Dup.foo`.
117+
-/
118+
#guard_msgs (whitespace := lax, substring := true) in
119+
theorem Dup.foo : True := trivial
120+
121+
end Dup
122+
123+
namespace Alpha
124+
namespace Beta
125+
126+
/- Tests the duplicate sequences of namespaces. -/
127+
/--
128+
warning: The namespaces `Alpha` and `Beta` are duplicated in the declaration
129+
`IrisTest.Alpha.Beta.Alpha.Beta.foo`.
130+
-/
131+
#guard_msgs (whitespace := lax, substring := true) in
132+
theorem Alpha.Beta.foo : True := trivial
133+
134+
end Beta
135+
end Alpha
136+
137+
/-! ## `linter.iris.style.whitespace` -/
138+
139+
/- Tests missing spaces. -/
140+
/--
141+
warning: missing space in the source
142+
143+
This part of the code
144+
'(a: Nat)'
145+
should be written as
146+
'(a : Nat)'
147+
-/
148+
#guard_msgs (whitespace := lax, substring := true) in
149+
example (a: Nat) : a = a := rfl
150+
151+
/- Tests extra spaces. -/
152+
/--
153+
warning: extra space in the source
154+
155+
This part of the code
156+
'Nat ) :'
157+
should be written as
158+
'Nat) : a'
159+
-/
160+
#guard_msgs (whitespace := lax, substring := true) in
161+
example (a : Nat ) : a = a := rfl
162+
163+
/- Tests incorrect indentation. -/
164+
/--
165+
warning: 'example : True := trivial' starts on column 2, but all commands should start at the
166+
beginning of the line.
167+
-/
168+
#guard_msgs (whitespace := lax, substring := true) in
169+
set_option linter.iris.style.whitespace true in
170+
example : True := trivial
171+
172+
end IrisTest

0 commit comments

Comments
 (0)