Basic linter template

Stream: metaprogramming / tactics

[Snir Broshi]

I'm trying to learn how Lean linters work, and I have this:

module

public meta import Mathlib.Tactic.Linter.Header
import Lean.Parser.Syntax

meta section

open Lean Elab Command Linter

namespace Mathlib.Linter

initialize addLinter { run stx := do
  let orig := stx.getSubstring?.getD default
  Linter.logLint linter.all (.ofRange ⟨orig.startPos, orig.stopPos⟩) m!"hello"
  log m!"hello2"
  logInfo m!"hello3"
}

end Mathlib.Linter

end section

def foo := 1337
theorem bar : True := trivial

I was hoping to see some logs or warnings anywhere, I'm trying to figure out which syntax nodes the function runs on (I'll log stx once logging works). What am I doing wrong? Thanks!

[Chris Henson]

Because of initialize you need to import the linter from another file for it to run.