feat: run linters in the new frontend

src/Lean.lean

@@ -17,7 +17,6 @@ import Lean.Class
 import Lean.LocalContext
 import Lean.MetavarContext
 import Lean.AuxRecursor
-import Lean.Linter
 import Lean.Meta
 import Lean.Util
 import Lean.Eval

src/Lean/Elab/Command.lean

@@ -54,6 +54,15 @@ structure Context :=
 abbrev CommandElabCoreM (ε) := ReaderT Context $ StateRefT State $ EIO ε
 abbrev CommandElabM := CommandElabCoreM Exception
 abbrev CommandElab  := Syntax → CommandElabM Unit
+abbrev Linter := Syntax → CommandElabM Unit
+
+/- Linters should be loadable as plugins, so store in a global IO ref instead of an attribute managed by the
+    environment (which only contains `import`ed objects). -/
+builtin_initialize lintersRef : IO.Ref (Array Linter) ← IO.mkRef #[]
+
+def addLinter (l : Linter) : IO Unit := do
+let ls ← lintersRef.get
+lintersRef.set (ls.push l)
 
 instance : MonadEnv CommandElabM := {
   getEnv    := do pure (← get).env,
@@ -137,6 +146,18 @@ instance : MonadLog CommandElabM := {
     modify fun s => { s with messages := s.messages.add msg }
 }
 
+def runLinters (stx : Syntax) : CommandElabM Unit := do
+  let linters ← lintersRef.get
+  unless linters.isEmpty do
+    for linter in linters do
+      let savedState ← get
+      try
+        linter stx
+      catch ex =>
+        logException ex
+      finally
+        modify fun s => { savedState with messages := s.messages }
+
 protected def getCurrMacroScope : CommandElabM Nat  := do pure (← read).currMacroScope
 protected def getMainModule     : CommandElabM Name := do pure (← getEnv).mainModule
 
@@ -194,7 +215,9 @@ instance : MonadRecDepth CommandElabM := {
 builtin_initialize registerTraceClass `Elab.command
 
 partial def elabCommand : Syntax → CommandElabM Unit
-  | stx => withLogging $ withRef stx $ withIncRecDepth $ withFreshMacroScope $ match stx with
+  | stx => withLogging $ withRef stx $ withIncRecDepth $ withFreshMacroScope do
+    runLinters stx
+    match stx with
     | Syntax.node k args =>
       if k == nullKind then
         -- list of commands => elaborate in order
@@ -618,4 +641,8 @@ def expandDeclId (declId : Syntax) (modifiers : Modifiers) : CommandElabM Expand
   let currLevelNames ← getLevelNames
   Lean.Elab.expandDeclId currNamespace currLevelNames declId modifiers
 
-end Lean.Elab.Command
+end Elab.Command
+
+export Elab.Command (Linter addLinter)
+
+end Lean

src/Lean/Elab/DefView.lean

@@ -15,121 +15,121 @@ import Lean.Elab.DeclUtil
 namespace Lean.Elab
 
 inductive DefKind
-| «def» | «theorem» | «example» | «opaque» | «abbrev»
+  | «def» | «theorem» | «example» | «opaque» | «abbrev»
 
 def DefKind.isTheorem : DefKind → Bool
-| «theorem» => true
-| _         => false
+  | «theorem» => true
+  | _         => false
 
 def DefKind.isDefOrAbbrevOrOpaque : DefKind → Bool
-| «def»    => true
-| «opaque» => true
-| «abbrev» => true
-| _        => false
+  | «def»    => true
+  | «opaque» => true
+  | «abbrev» => true
+  | _        => false
 
 def DefKind.isExample : DefKind → Bool
-| «example» => true
-| _         => false
+  | «example» => true
+  | _         => false
 
 structure DefView :=
-(kind          : DefKind)
-(ref           : Syntax)
-(modifiers     : Modifiers)
-(declId        : Syntax)
-(binders       : Syntax)
-(type?         : Option Syntax)
-(value         : Syntax)
+  (kind          : DefKind)
+  (ref           : Syntax)
+  (modifiers     : Modifiers)
+  (declId        : Syntax)
+  (binders       : Syntax)
+  (type?         : Option Syntax)
+  (value         : Syntax)
 
 namespace Command
 
 open Meta
 
 def mkDefViewOfAbbrev (modifiers : Modifiers) (stx : Syntax) : DefView :=
--- parser! "abbrev " >> declId >> optDeclSig >> declVal
-let (binders, type) := expandOptDeclSig (stx.getArg 2)
-let modifiers       := modifiers.addAttribute { name := `inline }
-let modifiers       := modifiers.addAttribute { name := `reducible }
-{ ref := stx, kind := DefKind.abbrev, modifiers := modifiers,
-  declId := stx.getArg 1, binders := binders, type? := type, value := stx.getArg 3 }
+  -- parser! "abbrev " >> declId >> optDeclSig >> declVal
+  let (binders, type) := expandOptDeclSig (stx.getArg 2)
+  let modifiers       := modifiers.addAttribute { name := `inline }
+  let modifiers       := modifiers.addAttribute { name := `reducible }
+  { ref := stx, kind := DefKind.abbrev, modifiers := modifiers,
+    declId := stx.getArg 1, binders := binders, type? := type, value := stx.getArg 3 }
 
 def mkDefViewOfDef (modifiers : Modifiers) (stx : Syntax) : DefView :=
--- parser! "def " >> declId >> optDeclSig >> declVal
-let (binders, type) := expandOptDeclSig (stx.getArg 2)
-{ ref := stx, kind := DefKind.def, modifiers := modifiers,
-  declId := stx.getArg 1, binders := binders, type? := type, value := stx.getArg 3 }
+  -- parser! "def " >> declId >> optDeclSig >> declVal
+  let (binders, type) := expandOptDeclSig (stx.getArg 2)
+  { ref := stx, kind := DefKind.def, modifiers := modifiers,
+    declId := stx.getArg 1, binders := binders, type? := type, value := stx.getArg 3 }
 
 def mkDefViewOfTheorem (modifiers : Modifiers) (stx : Syntax) : DefView :=
--- parser! "theorem " >> declId >> declSig >> declVal
-let (binders, type) := expandDeclSig (stx.getArg 2)
-{ ref := stx, kind := DefKind.theorem, modifiers := modifiers,
-  declId := stx.getArg 1, binders := binders, type? := some type, value := stx.getArg 3 }
+  -- parser! "theorem " >> declId >> declSig >> declVal
+  let (binders, type) := expandDeclSig (stx.getArg 2)
+  { ref := stx, kind := DefKind.theorem, modifiers := modifiers,
+    declId := stx.getArg 1, binders := binders, type? := some type, value := stx.getArg 3 }
 
 def mkFreshInstanceName : CommandElabM Name := do
-let s ← get
-let idx := s.nextInstIdx
-modify fun s => { s with nextInstIdx := s.nextInstIdx + 1 }
-return Lean.Elab.mkFreshInstanceName s.env idx
+  let s ← get
+  let idx := s.nextInstIdx
+  modify fun s => { s with nextInstIdx := s.nextInstIdx + 1 }
+  return Lean.Elab.mkFreshInstanceName s.env idx
 
 def mkDefViewOfConstant (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := do
--- parser! "constant " >> declId >> declSig >> optional declValSimple
-let (binders, type) := expandDeclSig (stx.getArg 2)
-let val ← match (stx.getArg 3).getOptional? with
-  | some val => pure val
-  | none     =>
-    let val ← `(arbitrary _)
-    pure $ Syntax.node `Lean.Parser.Command.declValSimple #[ mkAtomFrom stx ":=", val ]
-return {
-  ref := stx, kind := DefKind.opaque, modifiers := modifiers,
-  declId := stx.getArg 1, binders := binders, type? := some type, value := val
-}
+  -- parser! "constant " >> declId >> declSig >> optional declValSimple
+  let (binders, type) := expandDeclSig (stx.getArg 2)
+  let val ← match (stx.getArg 3).getOptional? with
+    | some val => pure val
+    | none     =>
+      let val ← `(arbitrary _)
+      pure $ Syntax.node `Lean.Parser.Command.declValSimple #[ mkAtomFrom stx ":=", val ]
+  return {
+    ref := stx, kind := DefKind.opaque, modifiers := modifiers,
+    declId := stx.getArg 1, binders := binders, type? := some type, value := val
+  }
 
 def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := do
--- parser! "instance " >> optional declId >> declSig >> declVal
-let (binders, type) := expandDeclSig (stx.getArg 2)
-let modifiers       := modifiers.addAttribute { name := `instance }
-let declId ← match (stx.getArg 1).getOptional? with
-  | some declId => pure declId
-  | none        =>
-    let id ← mkFreshInstanceName
-    pure $ Syntax.node `Lean.Parser.Command.declId #[mkIdentFrom stx id, mkNullNode]
-return {
-  ref := stx, kind := DefKind.def, modifiers := modifiers,
-  declId := declId, binders := binders, type? := type, value := stx.getArg 3
-}
+  -- parser! "instance " >> optional declId >> declSig >> declVal
+  let (binders, type) := expandDeclSig (stx.getArg 2)
+  let modifiers       := modifiers.addAttribute { name := `instance }
+  let declId ← match (stx.getArg 1).getOptional? with
+    | some declId => pure declId
+    | none        =>
+      let id ← mkFreshInstanceName
+      pure $ Syntax.node `Lean.Parser.Command.declId #[mkIdentFrom stx id, mkNullNode]
+  return {
+    ref := stx, kind := DefKind.def, modifiers := modifiers,
+    declId := declId, binders := binders, type? := type, value := stx.getArg 3
+  }
 
 def mkDefViewOfExample (modifiers : Modifiers) (stx : Syntax) : DefView :=
--- parser! "example " >> declSig >> declVal
-let (binders, type) := expandDeclSig (stx.getArg 1)
-let id              := mkIdentFrom stx `_example
-let declId          := Syntax.node `Lean.Parser.Command.declId #[id, mkNullNode]
-{ ref := stx, kind := DefKind.example, modifiers := modifiers,
-  declId := declId, binders := binders, type? := some type, value := stx.getArg 2 }
+  -- parser! "example " >> declSig >> declVal
+  let (binders, type) := expandDeclSig (stx.getArg 1)
+  let id              := mkIdentFrom stx `_example
+  let declId          := Syntax.node `Lean.Parser.Command.declId #[id, mkNullNode]
+  { ref := stx, kind := DefKind.example, modifiers := modifiers,
+    declId := declId, binders := binders, type? := some type, value := stx.getArg 2 }
 
 def isDefLike (stx : Syntax) : Bool :=
-let declKind := stx.getKind
-declKind == `Lean.Parser.Command.«abbrev» ||
-declKind == `Lean.Parser.Command.«def» ||
-declKind == `Lean.Parser.Command.«theorem» ||
-declKind == `Lean.Parser.Command.«constant» ||
-declKind == `Lean.Parser.Command.«instance» ||
-declKind == `Lean.Parser.Command.«example»
+  let declKind := stx.getKind
+  declKind == `Lean.Parser.Command.«abbrev» ||
+  declKind == `Lean.Parser.Command.«def» ||
+  declKind == `Lean.Parser.Command.«theorem» ||
+  declKind == `Lean.Parser.Command.«constant» ||
+  declKind == `Lean.Parser.Command.«instance» ||
+  declKind == `Lean.Parser.Command.«example»
 
 def mkDefView (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView :=
-let declKind := stx.getKind
-if declKind == `Lean.Parser.Command.«abbrev» then
-  pure $ mkDefViewOfAbbrev modifiers stx
-else if declKind == `Lean.Parser.Command.«def» then
-  pure $ mkDefViewOfDef modifiers stx
-else if declKind == `Lean.Parser.Command.«theorem» then
-  pure $ mkDefViewOfTheorem modifiers stx
-else if declKind == `Lean.Parser.Command.«constant» then
-  mkDefViewOfConstant modifiers stx
-else if declKind == `Lean.Parser.Command.«instance» then
-  mkDefViewOfInstance modifiers stx
-else if declKind == `Lean.Parser.Command.«example» then
-  pure $ mkDefViewOfExample modifiers stx
-else
-  throwError "unexpected kind of definition"
+  let declKind := stx.getKind
+  if declKind == `Lean.Parser.Command.«abbrev» then
+    pure $ mkDefViewOfAbbrev modifiers stx
+  else if declKind == `Lean.Parser.Command.«def» then
+    pure $ mkDefViewOfDef modifiers stx
+  else if declKind == `Lean.Parser.Command.«theorem» then
+    pure $ mkDefViewOfTheorem modifiers stx
+  else if declKind == `Lean.Parser.Command.«constant» then
+    mkDefViewOfConstant modifiers stx
+  else if declKind == `Lean.Parser.Command.«instance» then
+    mkDefViewOfInstance modifiers stx
+  else if declKind == `Lean.Parser.Command.«example» then
+    pure $ mkDefViewOfExample modifiers stx
+  else
+    throwError "unexpected kind of definition"
 
 builtin_initialize registerTraceClass `Elab.definition
 

src/Lean/Linter.lean

@@ -1,27 +0,0 @@
-#lang lean4
-/-
-Copyright (c) 2019 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Ullrich
--/
-import Lean.Attributes
-import Lean.Syntax
-import Lean.Message
-
-namespace Lean
-
-def Linter := Environment → Name → Syntax → IO MessageLog
-
-def mkLintersRef : IO (IO.Ref (Array Linter)) :=
-IO.mkRef #[]
-
-/- Linters should be loadable as plugins, so store in a global IO ref instead of an attribute managed by the
-    environment (which only contains `import`ed objects). -/
-@[builtinInit mkLintersRef, export lean_linters_ref]
-constant lintersRef : IO.Ref (Array Linter)
-
-def addLinter (l : Linter) : IO Unit := do
-let ls ← lintersRef.get
-lintersRef.set (ls.push l)
-
-end Lean

src/frontends/lean/definition_cmds.cpp

@@ -475,15 +475,6 @@ static environment elab_single_def(parser & p, decl_cmd_kind const & kind, cmd_m
         }
         new_env = meta.m_attrs.apply_after_comp(new_env, c_real_name);
 
-        // temporary code that should soon be removed together with the whole C++ frontend
-        object_ref r(st_ref_get(lean_linters_ref, io_mk_world()));
-        lean_assert(io_result_is_ok(r.raw()));
-        array_ref<object *> linters(io_result_get_value(r.raw()), true);
-        for (object * const & linter : linters) {
-            object * r2 = apply_4(linter, new_env.to_obj_arg(), local_name_p(fn).to_obj_arg(), lean_box(0) /* Syntax.missing */, io_mk_world());
-            consume_io_result(r2);
-        }
-
         return new_env;
     };
 

tests/plugin/SnakeLinter.lean

@@ -1,15 +1,18 @@
+#lang lean4
 import Lean
 
 open Lean
-
 def oh_no : Nat := 0
 
-def snakeLinter : Linter :=
-fun env n stx =>
-  -- TODO(Sebastian): return actual message with position from syntax tree
-  if n.toString.contains '_' then throw $ IO.userError "SNAKES!!"
-  else pure MessageLog.empty
+def snakeLinter : Linter := fun stx => do
+  if stx.getKind == `Lean.Parser.Command.declaration then
+    let decl := stx[1]
+    if decl.getKind == `Lean.Parser.Command.def then
+      let declId   := decl[1]
+      withRef declId do
+        let declName := declId[0].getId
+        if declName.eraseMacroScopes.toString.contains '_' then
+          -- TODO(Sebastian): return actual message with position from syntax tree
+          throwError "SNAKES!!"
 
-@[init]
-def registerSnakeLinter : IO Unit :=
-addLinter snakeLinter
+initialize addLinter snakeLinter