Lint without compiling to .so

Stream: lean4

[Yuri de Wit]

I was intrigued by the Linter API in the compiler and decided to give it a shot. And the SnakeLinter.lean gave me a good starting point.

I do see that Lean.Elab.Command has a runLinters, but how do I get a Syntax to test my Linter without having to compile to a shared library, etc?

[Sebastian Ullrich]

If you are okay with explicitly importing your linter, calling addLinter in initialize should work I think. The reason for the .so is of course that you shouldn't need to import linters, they should be optional parts you "side-load" into your development environment. The build system should ideally make it trivial to produce such .sos, about which I had an entire talk :laughing: .

[Yuri de Wit]

Here is a #MWE:

import Lean.Elab.Command

set_option trace.Meta.debug true

open Lean

def test : Nat := 0

def testLinter : Linter := fun stx => do
  trace[Meta.debug] "Test linter"

initialize addLinter testLinter

#eval Elab.Command.runLinters <| quote test  -- <== ERROR

-- #eval Elab.Command.elabCommandTopLevel <| quote test

And this is where I am stuck:

expression
  Elab.Command.runLinters (quote test)
has type
  Elab.Command.CommandElabM Unit
but instance
  MetaEval (Elab.Command.CommandElabM Unit)
failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.MetaEval` class

How can I test a test a linter without having to rely on building and packaging?

[Yuri de Wit]

Sebastian Ullrich said:

If you are okay with explicitly importing your linter, calling addLinter in initialize should work I think. The reason for the .so is of course that you shouldn't need to import linters, they should be optional parts you "side-load" into your development environment. The build system should ideally make it trivial to produce such .sos, about which I had an entire talk :laughing: .

The design makes sense. It is just counter productive for experimentation, learning or unit testing.

[Yuri de Wit]

This is as far as a got at this point:

set_option trace.Meta.debug true

def formatLinter : Linter := fun stx => do
  trace[Meta.debug] s!"TBD: {stx}"

initialize addLinter formatLinter

syntax "#lint" term : command
elab_rules : command
| `(#lint $t:term) => formatLinter t

#lint `(def test:Nat :=0)

I am able to call the linter using some piece of syntax but it does not seem to have source info, which I guess is expected.