-
Notifications
You must be signed in to change notification settings - Fork 384
/
Copy pathLint.lean
200 lines (160 loc) · 7.35 KB
/
Lint.lean
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
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
/-
Copyright (c) 2023 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn
-/
import Lean.Linter.Util
import Batteries.Data.Array.Basic
import Batteries.Tactic.Lint
/-!
# Linters for Mathlib
In this file we define additional linters for mathlib.
Perhaps these should be moved to Batteries in the future.
-/
namespace Std.Tactic.Lint
open Lean Meta
/--
Linter that checks whether a structure should be in Prop.
-/
@[env_linter] def structureInType : Linter where
noErrorsFound := "no structures that should be in Prop found."
errorsFound := "FOUND STRUCTURES THAT SHOULD BE IN PROP."
test declName := do
unless isStructure (← getEnv) declName do return none
-- remark: using `Lean.Meta.isProp` doesn't suffice here, because it doesn't (always?)
-- recognize predicates as propositional.
let isProp ← forallTelescopeReducing (← inferType (← mkConstWithLevelParams declName))
fun _ ty => return ty == .sort .zero
if isProp then return none
let projs := (getStructureInfo? (← getEnv) declName).get!.fieldNames
if projs.isEmpty then return none -- don't flag empty structures
let allProofs ← projs.allM (do isProof <| ← mkConstWithLevelParams <| declName ++ ·)
unless allProofs do return none
return m!"all fields are propositional but the structure isn't."
/-- Linter that check that all `deprecated` tags come with `since` dates. -/
@[env_linter] def deprecatedNoSince : Linter where
noErrorsFound := "no `deprecated` tags without `since` dates."
errorsFound := "FOUND `deprecated` tags without `since` dates."
test declName := do
let some info := Lean.Linter.deprecatedAttr.getParam? (← getEnv) declName | return none
match info.since? with
| some _ => return none -- TODO: enforce `YYYY-MM-DD` format
| none => return m!"`deprecated` attribute without `since` date"
end Std.Tactic.Lint
namespace Mathlib.Linter
/-!
# `dupNamespace` linter
The `dupNamespace` linter produces a warning when a declaration contains the same namespace
at least twice consecutively.
For instance, `Nat.Nat.foo` and `One.two.two` trigger a warning, while `Nat.One.Nat` does not.
-/
/--
The `dupNamespace` linter is set on by default. Lean emits a warning on any declaration that
contains the same namespace at least twice consecutively.
For instance, `Nat.Nat.foo` and `One.two.two` trigger a warning, while `Nat.One.Nat` does not.
*Note.*
This linter will not detect duplication in namespaces of autogenerated declarations
(other than the one whose `declId` is present in the source declaration).
-/
register_option linter.dupNamespace : Bool := {
defValue := true
descr := "enable the duplicated namespace linter"
}
namespace DupNamespaceLinter
open Lean Parser Elab Command Meta
/-- Gets the value of the `linter.dupNamespace` option. -/
def getLinterDupNamespace (o : Options) : Bool := Linter.getLinterValue linter.dupNamespace o
/-- `getIds stx` extracts the `declId` nodes from the `Syntax` `stx`.
If `stx` is an `alias` or an `export`, then it extracts an `ident`, instead of a `declId`. -/
partial
def getIds : Syntax → Array Syntax
| .node _ `Batteries.Tactic.Alias.alias args => args[2:3]
| .node _ ``Lean.Parser.Command.export args => (args[3:4] : Array Syntax).map (·[0])
| stx@(.node _ _ args) =>
((args.attach.map fun ⟨a, _⟩ => getIds a).foldl (· ++ ·) #[stx]).filter (·.getKind == ``declId)
| _ => default
@[inherit_doc linter.dupNamespace]
def dupNamespace : Linter where run := withSetOptionIn fun stx => do
if getLinterDupNamespace (← getOptions) then
match getIds stx with
| #[id] =>
let ns := (← getScope).currNamespace
let declName := ns ++ (if id.getKind == ``declId then id[0].getId else id.getId)
let nm := declName.components
let some (dup, _) := nm.zip (nm.tailD []) |>.find? fun (x, y) => x == y
| return
Linter.logLint linter.dupNamespace id
m!"The namespace '{dup}' is duplicated in the declaration '{declName}'"
| _ => return
initialize addLinter dupNamespace
end DupNamespaceLinter
/-!
# `oneLineAlign` linter
The `oneLineAlign` linter checks that `#align` statements span a single line,
which is desirable as it allows them to be parsed by very simple parsers.
-/
/--
The `oneLineAlign` linter is set on by default. Lean emits a warning on `#align` statements
spanning more than one line.
-/
register_option linter.oneLineAlign : Bool := {
defValue := true
descr := "enable the one-line align linter"
}
namespace OneLineAlignLinter
open Lean
/-- Gets the value of the `linter.oneLineAlign` option. -/
def getLinterOneLineAlign (o : Options) : Bool := Linter.getLinterValue linter.oneLineAlign o
@[inherit_doc linter.oneLineAlign]
def oneLineAlign : Linter where run := withSetOptionIn fun stx => do
if getLinterOneLineAlign (← getOptions) then
if stx.isOfKind `Mathlib.Prelude.Rename.align then
if let some spos := stx.getRange? then
let fm ← getFileMap
let lines := (fm.toPosition spos.stop).line - (fm.toPosition spos.start).line + 1
if lines != 1 then
Linter.logLint linter.oneLineAlign stx
m!"This `#align` spans {lines} lines, instead of just one.\n\
Do not worry, the 100 character limit does not apply to `#align` statements!"
initialize addLinter oneLineAlign
end OneLineAlignLinter
/-!
# The "EndOf" linter
The "EndOf" linter emits a warning on non-closed `section`s and `namespace`s.
It allows the "outermost" `noncomputable section` to be left open (whether or not it is named).
-/
open Lean Elab Command
/-- The "EndOf" linter emits a warning on non-closed `section`s and `namespace`s.
It allows the "outermost" `noncomputable section` to be left open (whether or not it is named).
-/
register_option linter.endOf : Bool := {
defValue := true
descr := "enable the EndOf linter"
}
namespace EndOf
/-- Gets the value of the `linter.endOf` option. -/
def getLinterHash (o : Options) : Bool := Linter.getLinterValue linter.endOf o
@[inherit_doc Mathlib.Linter.linter.endOf]
def endOfLinter : Linter where run := withSetOptionIn fun stx ↦ do
-- Only run this linter at the end of a module.
unless stx.isOfKind ``Lean.Parser.Command.eoi do return
-- TODO: once mathlib's Lean version includes leanprover/lean4#4741, make this configurable
unless #[`Mathlib, `test, `Archive, `Counterexamples].contains (← getMainModule).getRoot do
return
if getLinterHash (← getOptions) && !(← MonadState.get).messages.hasErrors then
let sc ← getScopes
-- The last scope is always the "base scope", corresponding to no active `section`s or
-- `namespace`s. We are interested in any *other* unclosed scopes.
if sc.length == 1 then return
let ends := sc.dropLast.map fun s ↦ (s.header, s.isNoncomputable)
-- If the outermost scope corresponds to a `noncomputable section`, we ignore it.
let ends := if ends.getLast!.2 then ends.dropLast else ends
-- If there are any further un-closed scopes, we emit a warning.
if !ends.isEmpty then
let ending := (ends.map Prod.fst).foldl (init := "") fun a b ↦
a ++ s!"\n\nend{if b == "" then "" else " "}{b}"
Linter.logLint linter.endOf stx
m!"unclosed sections or namespaces; expected: '{ending}'"
initialize addLinter endOfLinter
end EndOf
end Mathlib.Linter