unused variable not flagged as unused

Stream: lean4

[Damiano Testa]

The unusedVariable linter does not report the cmd unused variable sometimes with a set State:

import Lean.Elab.Command

open Lean

def unreportedUnused_cmd : Linter where run cmd := do
  set { (← get) with }  -- comment `set` to realize that `cmd` is unused
  set (← get)           -- this, on the other hand, plays no role
  return

[Damiano Testa]

In fact, even an unused let triggers the same behaviour:

import Lean.Elab.Command

open Lean

def unreportedUnused_cmd : Linter where run cmd := do
  let _ := { (← get) with }  -- comment me to realize that `cmd` is unused
  return

[Anders Larsson]

The second example produces an error.

invalid {...} notation, expected type is not of the form (C ...)
LinterLean 4

[Damiano Testa]

Oh, sorry, I meant it to have the same imports and open as before: let me edit.

[Damiano Testa]

I suspect that it is the autofilled name field that is disturbing the unusedVariable linter.

[Damiano Testa]

Ok, this is further minimized (no imports or opens necessary):

structure X where
  r : Unit → Unit
  name : Lean.Name := by exact decl_name%

structure nothing

def unreportedUnused : X where
  -- if `name` is provided, `cmd` is always unused,
  name := `h
  -- otherwise, the `{ ... with }`-syntax interferes with the unused variable linter
  r cmd :=
    let _ := { (⟨⟩ : nothing) with }   -- if `name` is commented, then comment me to realize that `cmd` is unused
    ()

[Damiano Testa]

I've bumped into this again and now I have minimized further:

structure A where
  name : Lean.Name := by exact decl_name%

-- unusedVariable is quiet
example : A :=
  let _ := if let some nat := some 0 then 0 else 0
  {}

-- `nat` is unused
example : A :=
  let _ := if let some nat := some 0 then 0 else 0
  { name := `a }

[Sebastian Ullrich]

Looking for uses in tactic proofs is too brittle, it will be disabled by default in #5338 and then this code will behave as expected

[Damiano Testa]

lean#5338

Great, thanks for the update!