max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

perf: do not lint unused variables defined in tactics by default (#5338)

Browse source 
Should ensure we visit at most as many expr nodes as in the final expr
instead of many possibly overlapping mvar assignments. This is likely
the only way we can ensure acceptable performance in all cases.

---------

Co-authored-by: Kim Morrison <kim@tqft.net>
This commit is contained in:
Sebastian Ullrich 2024-10-17 11:55:11 +02:00 • committed by GitHub
parent 08d8a0873e
commit f2ac0d03c6
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
9 changed files with 240 additions and 163 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Init/Data/Option/Attach.lean
View file

@ -44,7 +44,7 @@ theorem attach_congr {o₁ o₂ : Option α} (h : o₁ = o₂) :
simp
theorem attachWith_congr {o₁ o₂ : Option α} (w : o₁ = o₂) {P : α → Prop} {H : ∀ x ∈ o₁, P x} :
o₁.attachWith P H = o₂.attachWith P fun x h => H _ (w ▸ h) := by
o₁.attachWith P H = o₂.attachWith P fun _ h => H _ (w ▸ h) := by
subst w
simp
@ -128,12 +128,12 @@ theorem attach_map {o : Option α} (f : α → β) :
cases o <;> simp
theorem attachWith_map {o : Option α} (f : α → β) {P : β → Prop} {H : ∀ (b : β), b ∈ o.map f → P b} :
(o.map f).attachWith P H = (o.attachWith (P ∘ f) (fun a h => H _ (mem_map_of_mem f h))).map
(o.map f).attachWith P H = (o.attachWith (P ∘ f) (fun _ h => H _ (mem_map_of_mem f h))).map
fun ⟨x, h⟩ => ⟨f x, h⟩ := by
cases o <;> simp
theorem map_attach {o : Option α} (f : { x // x ∈ o } → β) :
o.attach.map f = o.pmap (fun a (h : a ∈ o) => f ⟨a, h⟩) (fun a h => h) := by
o.attach.map f = o.pmap (fun a (h : a ∈ o) => f ⟨a, h⟩) (fun _ h => h) := by
cases o <;> simp
theorem map_attachWith {o : Option α} {P : α → Prop} {H : ∀ (a : α), a ∈ o → P a}

1
src/Lean/Elab/LetRec.lean
View file

@ -90,6 +90,7 @@ private def elabLetRecDeclValues (view : LetRecView) : TermElabM (Array Expr) :=
for i in [0:view.binderIds.size] do
addLocalVarInfo view.binderIds[i]! xs[i]!
withDeclName view.declName do
withInfoContext' view.valStx (mkInfo := mkTermInfo `MutualDef.body view.valStx) do
let value ← elabTermEnsuringType view.valStx type
mkLambdaFVars xs value

14
src/Lean/Elab/MutualDef.lean
View file

@ -410,11 +410,15 @@ private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr
-- skip auto-bound prefix in `xs`
addLocalVarInfo header.binderIds[i] xs[header.numParams - header.binderIds.size + i]!
let val ← withReader ({ · with tacSnap? := header.tacSnap? }) do
-- synthesize mvars here to force the top-level tactic block (if any) to run
elabTermEnsuringType valStx type <* synthesizeSyntheticMVarsNoPostponing
-- NOTE: without this `instantiatedMVars`, `mkLambdaFVars` may leave around a redex that
-- leads to more section variables being included than necessary
let val ← instantiateMVarsProfiling val
-- Store instantiated body in info tree for the benefit of the unused variables linter
-- and other metaprograms that may want to inspect it without paying for the instantiation
-- again
withInfoContext' valStx (mkInfo := mkTermInfo `MutualDef.body valStx) do
-- synthesize mvars here to force the top-level tactic block (if any) to run
let val ← elabTermEnsuringType valStx type <* synthesizeSyntheticMVarsNoPostponing
-- NOTE: without this `instantiatedMVars`, `mkLambdaFVars` may leave around a redex that
-- leads to more section variables being included than necessary
instantiateMVarsProfiling val
let val ← mkLambdaFVars xs val
if linter.unusedSectionVars.get (← getOptions) && !header.type.hasSorry && !val.hasSorry then
let unusedVars ← vars.filterMapM fun var => do

2
src/Lean/Linter/ConstructorAsVariable.lean
View file

@ -37,7 +37,7 @@ def constructorNameAsVariable : Linter where
let warnings : IO.Ref (Std.HashMap String.Range (Syntax × Name × Name)) ← IO.mkRef {}
for tree in infoTrees do
tree.visitM' (preNode := fun ci info _ => do
tree.visitM' (postNode := fun ci info _ => do
match info with
| .ofTermInfo ti =>
match ti.expr with

190
src/Lean/Linter/UnusedVariables.lean
View file

@ -10,41 +10,55 @@ set_option linter.missingDocs true -- keep it documented
/-! # Unused variable Linter
This file implements the unused variable linter, which runs automatically on all commands
and reports any local variables that are never referred to, using information from the info tree.
This file implements the unused variable linter, which runs automatically on all
commands and reports any local variables that are never referred to, using
information from the info tree.
It is not immediately obvious but this is a surprisingly expensive check without some optimizations.
The main complication is that it can be difficult to determine what constitutes a "use".
For example, we would like this to be considered a use of `x`:
It is not immediately obvious but this is a surprisingly expensive check without
some optimizations. The main complication is that it can be difficult to
determine what constitutes a "use" apart from direct references to a variable
that we can easily find in the info tree. For example, we would like this to be
considered a use of `x`:
```
def foo (x : Nat) : Nat := by assumption
```
The final proof term is `fun x => x` so clearly `x` was used, but we can't make use of this because
the final proof term is after we have abstracted over the original `fvar` for `x`. If we look
further into the tactic state we can see the `fvar` show up in the instantiation to the original
goal metavariable `?m : Nat := x`, but it is not always the case that we can follow metavariable
instantiations to determine what happened after the fact, because tactics might skip the goal
metavariable and instantiate some other metavariable created prior to it instead.
The final proof term is `fun x => x` so clearly `x` was used, but we can't make
use of this because the final proof term is after we have abstracted over the
original `fvar` for `x`. Instead, we make sure to store the proof term before
abstraction but after instantiation of mvars in the info tree and retrieve it in
the linter. Using the instantiated term is very important as redoing that step
in the linter can be prohibitively expensive. The downside of special-casing the
definition body in this way is that while it works for parameters, it does not
work for local variables in the body, so we ignore them by default if any tactic
infos are present (`linter.unusedVariables.analyzeTactics`).
Instead, we use a (much more expensive) overapproximation, which is just to look through the entire
metavariable context looking for occurrences of `x`. We use caching to ensure that this is still
linear in the size of the info tree, even though there are many metavariable contexts in all the
intermediate stages of elaboration; these are highly similar and make use of `PersistentHashMap`
so there is a lot of subterm sharing we can take advantage of.
If we do turn on this option and look further into the tactic state, we can see
the `fvar` show up in the instantiation to the original goal metavariable
`?m : Nat := x`, but it is not always the case that we can follow metavariable
instantiations to determine what happened after the fact, because tactics might
skip the goal metavariable and instantiate some other metavariable created prior
to it instead. Instead, we use a (much more expensive) overapproximation, which
is just to look through the entire metavariable context looking for occurrences
of `x`. We use caching to ensure that this is still linear in the size of the
info tree, even though there are many metavariable contexts in all the
intermediate stages of elaboration; these are highly similar and make use of
`PersistentHashMap` so there is a lot of subterm sharing we can take advantage
of.
## The `@[unused_variables_ignore_fn]` attribute
Some occurrences of variables are deliberately unused, or at least we don't want to lint on unused
variables in these positions. For example:
Some occurrences of variables are deliberately unused, or at least we don't want
to lint on unused variables in these positions. For example:
```
def foo (x : Nat) : (y : Nat) → Nat := fun _ => x
-- ^ don't lint this unused variable because it is public API
```
They are generally a syntactic criterion, so we allow adding custom `IgnoreFunction`s so that
external syntax can also opt in to lint suppression, like so:
They are generally a syntactic criterion, so we allow adding custom
`IgnoreFunction`s so that external syntax can also opt in to lint suppression,
like so:
```
macro (name := foobarKind) "foobar " name:ident : command => `(def foo ($name : Nat) := 0)
@ -77,6 +91,17 @@ register_builtin_option linter.unusedVariables.patternVars : Bool := {
defValue := true,
descr := "enable the 'unused variables' linter to mark unused pattern variables"
}
/-- Enables linting variables defined in tactic blocks, may be expensive for complex proofs -/
register_builtin_option linter.unusedVariables.analyzeTactics : Bool := {
defValue := false
descr := "enable analysis of local variables in presence of tactic proofs\
\n\
\nBy default, the linter will limit itself to linting a declaration's parameters \
whenever tactic proofs are present as these can be expensive to analyze. Enabling this \
option extends linting to local variables both inside and outside tactic proofs, \
though it can also lead to some false negatives as intermediate tactic states may \
reference some variables without the declaration ultimately depending on them."
}
/-- Gets the status of `linter.unusedVariables` -/
def getLinterUnusedVariables (o : Options) : Bool :=
@ -356,55 +381,82 @@ structure References where
/-- Collect information from the `infoTrees` into `References`.
See `References` for more information about the return value. -/
def collectReferences (infoTrees : Array Elab.InfoTree) (cmdStxRange : String.Range) :
StateRefT References IO Unit := do
for tree in infoTrees do
tree.visitM' (preNode := fun ci info _ => do
match info with
| .ofTermInfo ti =>
match ti.expr with
| .const .. =>
if ti.isBinder then
let some range := info.range? | return
let .original .. := info.stx.getHeadInfo | return -- we are not interested in canonical syntax here
modify fun s => { s with constDecls := s.constDecls.insert range }
| .fvar id .. =>
let some range := info.range? | return
let .original .. := info.stx.getHeadInfo | return -- we are not interested in canonical syntax here
if ti.isBinder then
-- This is a local variable declaration.
let some ldecl := ti.lctx.find? id | return
-- Skip declarations which are outside the command syntax range, like `variable`s
-- (it would be confusing to lint these), or those which are macro-generated
if !cmdStxRange.contains range.start || ldecl.userName.hasMacroScopes then return
let opts := ci.options
-- we have to check for the option again here because it can be set locally
if !getLinterUnusedVariables opts then return
let stx := skipDeclIdIfPresent info.stx
if let .str _ s := stx.getId then
-- If the variable name is `_foo` then it is intentionally (possibly) unused, so skip.
-- This is the suggested way to silence the warning
if s.startsWith "_" then return
-- Record this either as a new `fvarDefs`, or an alias of an existing one
modify fun s =>
if let some ref := s.fvarDefs[range]? then
{ s with fvarDefs := s.fvarDefs.insert range { ref with aliases := ref.aliases.push id } }
else
{ s with fvarDefs := s.fvarDefs.insert range { userName := ldecl.userName, stx, opts, aliases := #[id] } }
else
-- Found a direct use, keep track of it
modify fun s => { s with fvarUses := s.fvarUses.insert id }
| _ => pure ()
| .ofTacticInfo ti =>
-- Keep track of the `MetavarContext` after a tactic for later
modify fun s => { s with assignments := s.assignments.push ti.mctxAfter.eAssignment }
| .ofFVarAliasInfo i =>
-- record any aliases we find
modify fun s =>
let id := followAliases s.fvarAliases i.baseId
{ s with fvarAliases := s.fvarAliases.insert i.id id }
| _ => pure ())
partial def collectReferences (infoTrees : Array Elab.InfoTree) (cmdStxRange : String.Range) :
StateRefT References IO Unit := ReaderT.run (r := false) <| go infoTrees none
where
go infoTrees ctx? := do
for tree in infoTrees do
tree.visitM' (ctx? := ctx?) (preNode := fun ci info children => do
-- set if `analyzeTactics` is unset, tactic infos are present, and we're inside the body
let ignored ← read
match info with
| .ofTermInfo ti =>
-- NOTE: we have to do this check *before* `ignored` because nested bodies (e.g. from
-- nested `let rec`s) do need to be included to find all `Expr` uses of the top-level
-- parameters
if ti.elaborator == `MutualDef.body &&
!linter.unusedVariables.analyzeTactics.get ci.options then
-- the body is the only `Expr` we will analyze in this case
-- NOTE: we include it even if no tactics are present as at least for parameters we want
-- to lint only truly unused binders
let (e, _) := instantiateMVarsCore ci.mctx ti.expr
modify fun s => { s with
assignments := s.assignments.push (.insert {} ⟨.anonymous⟩ e) }
let tacticsPresent := children.any (·.findInfo? (· matches .ofTacticInfo ..) |>.isSome)
withReader (· || tacticsPresent) do
go children.toArray ci
return false
if ignored then return true
match ti.expr with
| .const .. =>
if ti.isBinder then
let some range := info.range? | return true
let .original .. := info.stx.getHeadInfo | return true -- we are not interested in canonical syntax here
modify fun s => { s with constDecls := s.constDecls.insert range }
| .fvar id .. =>
let some range := info.range? | return true
let .original .. := info.stx.getHeadInfo | return true -- we are not interested in canonical syntax here
if ti.isBinder then
-- This is a local variable declaration.
if ignored then return true
let some ldecl := ti.lctx.find? id | return true
-- Skip declarations which are outside the command syntax range, like `variable`s
-- (it would be confusing to lint these), or those which are macro-generated
if !cmdStxRange.contains range.start || ldecl.userName.hasMacroScopes then return true
let opts := ci.options
-- we have to check for the option again here because it can be set locally
if !getLinterUnusedVariables opts then return true
let stx := skipDeclIdIfPresent info.stx
if let .str _ s := stx.getId then
-- If the variable name is `_foo` then it is intentionally (possibly) unused, so skip.
-- This is the suggested way to silence the warning
if s.startsWith "_" then return true
-- Record this either as a new `fvarDefs`, or an alias of an existing one
modify fun s =>
if let some ref := s.fvarDefs[range]? then
{ s with fvarDefs := s.fvarDefs.insert range { ref with aliases := ref.aliases.push id } }
else
{ s with fvarDefs := s.fvarDefs.insert range { userName := ldecl.userName, stx, opts, aliases := #[id] } }
else
-- Found a direct use, keep track of it
modify fun s => { s with fvarUses := s.fvarUses.insert id }
| _ => pure ()
return true
| .ofTacticInfo ti =>
-- When ignoring new binders, no need to look at intermediate tactic states either as
-- references to binders outside the body will be covered by the body `Expr`
if ignored then return true
-- Keep track of the `MetavarContext` after a tactic for later
modify fun s => { s with assignments := s.assignments.push ti.mctxAfter.eAssignment }
return true
| .ofFVarAliasInfo i =>
if ignored then return true
-- record any aliases we find
modify fun s =>
let id := followAliases s.fvarAliases i.baseId
{ s with fvarAliases := s.fvarAliases.insert i.id id }
return true
| _ => return true)
/-- Since declarations attach the declaration info to the `declId`,
we skip that to get to the `.ident` if possible. -/
skipDeclIdIfPresent (stx : Syntax) : Syntax :=
@ -493,7 +545,7 @@ def unusedVariables : Linter where
-- collect additional `fvarUses` from tactic assignments
visitAssignments (← IO.mkRef {}) fvarUsesRef s.assignments
-- Resolve potential aliases again to preserve `fvarUsesRef` invariant
fvarUsesRef.modify fun fvarUses => fvarUses.fold (·.insert <| getCanonVar ·) {}
fvarUsesRef.modify fun fvarUses => fvarUses.toArray.map getCanonVar |> .insertMany {}
initializedMVars := true
let fvarUses ← fvarUsesRef.get
-- Redo the initial check because `fvarUses` could be bigger now

30
src/Lean/Server/InfoUtils.lean
View file

@ -40,27 +40,34 @@ structure InfoWithCtx where
info : Elab.Info
children : PersistentArray InfoTree
/-- Visit nodes, passing in a surrounding context (the innermost one combined with all outer ones)
and accumulating results on the way back up. -/
/--
Visit nodes, passing in a surrounding context (the innermost one combined with all outer ones) and
accumulating results on the way back up. If `preNode` returns `false`, the children of the current
node are skipped and `postNode` is invoked with an empty list of results.
-/
partial def InfoTree.visitM [Monad m]
(preNode : ContextInfo → Info → (children : PersistentArray InfoTree) → m Unit := fun _ _ _ => pure ())
(preNode : ContextInfo → Info → (children : PersistentArray InfoTree) → m Bool := fun _ _ _ => pure true)
(postNode : ContextInfo → Info → (children : PersistentArray InfoTree) → List (Option α) → m α)
: InfoTree → m (Option α) :=
go none
(ctx? : Option ContextInfo := none) : InfoTree → m (Option α) :=
go ctx?
where go
| ctx?, context ctx t => go (ctx.mergeIntoOuter? ctx?) t
| some ctx, node i cs => do
preNode ctx i cs
let as ← cs.toList.mapM (go <| i.updateContext? ctx)
postNode ctx i cs as
let visitChildren ← preNode ctx i cs
if !visitChildren then
postNode ctx i cs []
else
let as ← cs.toList.mapM (go <| i.updateContext? ctx)
postNode ctx i cs as
| none, node .. => panic! "unexpected context-free info tree node"
| _, hole .. => pure none
/-- `InfoTree.visitM` specialized to `Unit` return type -/
def InfoTree.visitM' [Monad m]
(preNode : ContextInfo → Info → (children : PersistentArray InfoTree) → m Unit := fun _ _ _ => pure ())
(preNode : ContextInfo → Info → (children : PersistentArray InfoTree) → m Bool := fun _ _ _ => pure true)
(postNode : ContextInfo → Info → (children : PersistentArray InfoTree) → m Unit := fun _ _ _ => pure ())
(t : InfoTree) : m Unit := t.visitM preNode (fun ci i cs _ => postNode ci i cs) |> discard
(ctx? : Option ContextInfo := none) (t : InfoTree) : m Unit :=
t.visitM preNode (fun ci i cs _ => postNode ci i cs) ctx? |> discard
/--
Visit nodes bottom-up, passing in a surrounding context (the innermost one) and the union of nested results (empty at leaves). -/
@ -410,6 +417,9 @@ where go ci?
match ci?, i with
| some ci, .ofTermInfo ti
| some ci, .ofOmissionInfo { toTermInfo := ti, .. } => do
-- NOTE: `instantiateMVars` can potentially be expensive but we rely on the elaborator
-- creating a fully instantiated `MutualDef.body` term info node which has the implicit effect
-- of making the `instantiateMVars` here a no-op and avoids further recursing into the body
let expr ← ti.runMetaM ci (instantiateMVars ti.expr)
return expr.hasSorry
-- we assume that `cs` are subterms of `ti.expr` and

91
tests/lean/1018unknowMVarIssue.lean.expected.out
View file

@ -31,49 +31,52 @@ a : α
• x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
• match α, β, x, a with
| α_1, .(α_1), Fam2.any, a => ?m x α_1 a
| .(Nat), .(Nat), Fam2.nat n, a => n : β @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabMatch
• x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ @ Lean.Elab.Term.elabIdent
• [.] x : none @ ⟨8, 8⟩-⟨8, 9⟩
• x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩
• x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ @ Lean.Elab.Term.elabIdent
• [.] x : none @ ⟨8, 8⟩-⟨8, 9⟩
• x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩
• [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
• [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
• @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
• [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
• Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
• [.] n : none @ ⟨10, 13⟩-⟨10, 14⟩
• [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
• [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
• @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
• [.] a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
• [.] Fam2.any : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨9, 4⟩-⟨9, 12⟩
• [.] a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
• α (isBinder := true) : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
• α : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
• Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
• α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
• a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
• FVarAlias a: _uniq.636 -> _uniq.312
• FVarAlias α: _uniq.635 -> _uniq.310
• ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
• [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
• Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
• [.] n : none @ ⟨10, 13⟩-⟨10, 14⟩
• [.] a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
• [.] Fam2.nat : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨10, 4⟩-⟨10, 12⟩
• [.] n : some Nat @ ⟨10, 13⟩-⟨10, 14⟩
• [.] a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
• Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
• Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
• Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
• n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
• a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
• FVarAlias a: _uniq.667 -> _uniq.312
• FVarAlias n: _uniq.666 -> _uniq.310
• n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
• [.] n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
• n : Nat @ ⟨10, 18⟩-⟨10, 19⟩
| .(Nat), .(Nat), Fam2.nat n, a => n : β @ ⟨8, 2⟩-⟨10, 19⟩ @ MutualDef.body
• match α, β, x, a with
| α_1, .(α_1), Fam2.any, a => ?m x α_1 a
| .(Nat), .(Nat), Fam2.nat n, a => n : β @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabMatch
• x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ @ Lean.Elab.Term.elabIdent
• [.] x : none @ ⟨8, 8⟩-⟨8, 9⟩
• x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩
• x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ @ Lean.Elab.Term.elabIdent
• [.] x : none @ ⟨8, 8⟩-⟨8, 9⟩
• x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩
• [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
• [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
• @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
• [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
• Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
• [.] n : none @ ⟨10, 13⟩-⟨10, 14⟩
• [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
• [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
• @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
• [.] a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
• [.] Fam2.any : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨9, 4⟩-⟨9, 12⟩
• [.] a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
• α (isBinder := true) : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
• α : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
• Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
• α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
• a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
• FVarAlias a: _uniq.636 -> _uniq.312
• FVarAlias α: _uniq.635 -> _uniq.310
• ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
• [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
• Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
• [.] n : none @ ⟨10, 13⟩-⟨10, 14⟩
• [.] a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
• [.] Fam2.nat : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨10, 4⟩-⟨10, 12⟩
• [.] n : some Nat @ ⟨10, 13⟩-⟨10, 14⟩
• [.] a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
• Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
• Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
• Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
• n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
• a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
• FVarAlias a: _uniq.667 -> _uniq.312
• FVarAlias n: _uniq.666 -> _uniq.310
• n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
• [.] n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
• n : Nat @ ⟨10, 18⟩-⟨10, 19⟩
• @_example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩-⟨7, 7⟩
[Elab.info] • command @ ⟨11, 0⟩-⟨11, 0⟩ @ Lean.Elab.Command.elabEoi

21
tests/lean/linterUnusedVariables.lean
View file

@ -129,6 +129,7 @@ def nolintPatternVars (x : Option (Option Nat)) : Nat :=
| some (some y) => (fun z => 1) 2
| _ => 0
set_option linter.unusedVariables.analyzeTactics true in
set_option linter.unusedVariables.patternVars false in
theorem nolintPatternVarsInduction (n : Nat) : True := by
induction n with
@ -188,9 +189,12 @@ opaque foo (x : Nat) : Nat
opaque foo' (x : Nat) : Nat :=
let y := 5
3
section
variable (bar)
variable (bar' : (x : Nat) → Nat)
variable {α β} [inst : ToString α]
end
@[specialize]
def specializeDef (x : Nat) : Nat := 3
@ -210,6 +214,8 @@ opaque externConst (x : Nat) : Nat :=
let y := 3
5
section
variable {α : Type}
macro "useArg " name:declId arg:ident : command => `(def $name ($arg : α) : α := $arg)
useArg usedMacroVariable a
@ -222,6 +228,7 @@ doNotUseArg unusedMacroVariable b
def ignoreDoNotUse : Lean.Linter.IgnoreFunction := fun _ stack _ => stack.matches [``doNotUse]
doNotUseArg unusedMacroVariable2 b
end
macro "ignoreArg " id:declId sig:declSig : command => `(opaque $id $sig)
ignoreArg ignoredMacroVariable (x : UInt32) : UInt32
@ -246,6 +253,7 @@ def Nat.discriminate (n : Nat) (H1 : n = 0 → α) (H2 : ∀ m, n = succ m →
| 0 => H1 rfl
| succ m => H2 m rfl
/-! These are *not* linted against anymore as they are parameters used in the eventual body term. -/
example [ord : Ord β] (f : α → β) (x y : α) : Ordering := compare (f x) (f y)
example {α β} [ord : Ord β] (f : α → β) (x y : α) : Ordering := compare (f x) (f y)
example {h : Decidable True} (t e : α) : ite True t e = t := if_pos trivial
@ -267,3 +275,16 @@ inaccessible annotation.
-/
example : (x = y) → y = x
| .refl _ => .refl _
/-! We do lint parameters by default (`analyzeTactics false`) even when they have lexical uses -/
theorem lexicalTacticUse (p : α → Prop) (ha : p a) (hb : p b) : p b := by
simp [ha, hb]
/-!
... however, `analyzeTactics true` consistently takes lexical uses for all variables into account
-/
set_option linter.unusedVariables.analyzeTactics true in
theorem lexicalTacticUse' (p : α → Prop) (ha : p a) (hb : p b) : p b := by
simp [ha, hb]

48
tests/lean/linterUnusedVariables.lean.expected.out
View file

@ -30,51 +30,37 @@ linterUnusedVariables.lean:119:6-119:7: warning: unused variable `a`
note: this linter can be disabled with `set_option linter.unusedVariables false`
linterUnusedVariables.lean:129:26-129:27: warning: unused variable `z`
note: this linter can be disabled with `set_option linter.unusedVariables false`
linterUnusedVariables.lean:137:9-137:10: warning: unused variable `h`
linterUnusedVariables.lean:138:9-138:10: warning: unused variable `h`
note: this linter can be disabled with `set_option linter.unusedVariables false`
linterUnusedVariables.lean:151:8-151:9: warning: unused variable `y`
linterUnusedVariables.lean:152:8-152:9: warning: unused variable `y`
note: this linter can be disabled with `set_option linter.unusedVariables false`
linterUnusedVariables.lean:154:20-154:21: warning: unused variable `β`
linterUnusedVariables.lean:155:20-155:21: warning: unused variable `β`
note: this linter can be disabled with `set_option linter.unusedVariables false`
linterUnusedVariables.lean:155:7-155:8: warning: unused variable `x`
linterUnusedVariables.lean:156:7-156:8: warning: unused variable `x`
note: this linter can be disabled with `set_option linter.unusedVariables false`
linterUnusedVariables.lean:165:6-165:7: warning: unused variable `s`
linterUnusedVariables.lean:166:6-166:7: warning: unused variable `s`
note: this linter can be disabled with `set_option linter.unusedVariables false`
linterUnusedVariables.lean:189:6-189:7: warning: unused variable `y`
linterUnusedVariables.lean:190:6-190:7: warning: unused variable `y`
note: this linter can be disabled with `set_option linter.unusedVariables false`
linterUnusedVariables.lean:196:19-196:20: warning: unused variable `x`
linterUnusedVariables.lean:200:19-200:20: warning: unused variable `x`
note: this linter can be disabled with `set_option linter.unusedVariables false`
linterUnusedVariables.lean:200:6-200:7: warning: unused variable `y`
linterUnusedVariables.lean:204:6-204:7: warning: unused variable `y`
note: this linter can be disabled with `set_option linter.unusedVariables false`
linterUnusedVariables.lean:205:6-205:7: warning: unused variable `y`
linterUnusedVariables.lean:209:6-209:7: warning: unused variable `y`
note: this linter can be disabled with `set_option linter.unusedVariables false`
linterUnusedVariables.lean:210:6-210:7: warning: unused variable `y`
linterUnusedVariables.lean:214:6-214:7: warning: unused variable `y`
note: this linter can be disabled with `set_option linter.unusedVariables false`
linterUnusedVariables.lean:219:32-219:33: warning: unused variable `b`
linterUnusedVariables.lean:225:32-225:33: warning: unused variable `b`
note: this linter can be disabled with `set_option linter.unusedVariables false`
linterUnusedVariables.lean:236:27-236:28: error: don't know how to synthesize placeholder
linterUnusedVariables.lean:243:27-243:28: error: don't know how to synthesize placeholder
context:
bar : ?m
bar' : Nat → Nat
α : Type ?u
β : ?m
inst : ToString α
a : Nat
⊢ Nat
linterUnusedVariables.lean:237:0-237:7: warning: declaration uses 'sorry'
linterUnusedVariables.lean:238:0-238:7: warning: declaration uses 'sorry'
linterUnusedVariables.lean:239:29-241:7: error: unexpected token 'theorem'; expected '{' or tactic
linterUnusedVariables.lean:239:27-239:29: error: unsolved goals
bar : ?m
bar' : Nat → Nat
α : Type ?u
β : ?m
inst : ToString α
linterUnusedVariables.lean:244:0-244:7: warning: declaration uses 'sorry'
linterUnusedVariables.lean:245:0-245:7: warning: declaration uses 'sorry'
linterUnusedVariables.lean:246:29-248:7: error: unexpected token 'theorem'; expected '{' or tactic
linterUnusedVariables.lean:246:27-246:29: error: unsolved goals
a : Nat
⊢ Nat
linterUnusedVariables.lean:249:9-249:12: warning: unused variable `ord`
note: this linter can be disabled with `set_option linter.unusedVariables false`
linterUnusedVariables.lean:250:15-250:18: warning: unused variable `ord`
note: this linter can be disabled with `set_option linter.unusedVariables false`
linterUnusedVariables.lean:251:9-251:10: warning: unused variable `h`
linterUnusedVariables.lean:281:41-281:43: warning: unused variable `ha`
note: this linter can be disabled with `set_option linter.unusedVariables false`