Damiano Testa: An introduction to linters

Stream: Lean Together 2025

[Jireh Loreaux]

A thread for discussion about this talk.

[Rob Lewis]

Back in the day we used the term "semantic linter" approximately for what Damiano is calling an environment linter but I never completely convinced myself it was the right name. There are interesting edge cases.

[Rob Lewis]

The unused variable linter, for one. It's local, can run per-declaration, is seen in languages that only have syntax linters... but at the same time it doesn't operate only on the surface syntax of the declaration.

[Rob Lewis]

So I think Damiano's distinction is a better one!

[Eric Wieser]

Are you referring to the linter.unusedVariables syntax linter or the unusedArguments environment linter, @Rob Lewis?

[Rob Lewis]

In the Lean 3 days we only had unusedArguments

[Michael Rothgang]

Great talk, thanks! Let me ask my question here, in case the answer is useful more permanently:
If I like working on linters and want to help out, are there any particular places which need help?

[Ruben Van de Velde]

linters all the way down

[Jeremy Avigad]

Is it hard to describe the trick for allowing linters to persist information? I am just curious.

[Edward van de Meent]

how was the syntaxtree visualisation made?

[Violeta Hernández]

I imagine Lean linters are written in Lean; is deep knowledge of the language required or does general knowledge on functional-style languages suffice?

[Eric Wieser]

Jeremy Avigad said:

Is it hard to describe the trick for allowing linters to persist information? I am just curious.

I assume it's "Use IO.Ref", which means that the state is global and not preserved with the usual mental model of progress in the file.

[Jesse Alama]

is there a tool to dump a parse tree in e.g. XML or JSON format, or does one need to write a custom linter akin to the ones talked about here?

[Damiano Testa]

Linter talk slides

[Damiano Testa]

Michael Rothgang said:

Great talk, thanks! Let me ask my question here, in case the answer is useful more permanently:
If I like working on linters and want to help out, are there any particular places which need help?

I know that I am not very good at writing fast code: if you know how to write code efficiently and do not know about linters, maybe a good way to learn might be to try to streamline existing code.

[Damiano Testa]

As with formalization, a great way of learning is to choose a goal of something to lint and try to write the linter yourself!

[Damiano Testa]

Rob Lewis said:

So I think Damiano's distinction is a better one!

I thought that this was a standard name: I have been using for a while, but I think that I heard it from someone else...

[Damiano Testa]

Jeremy Avigad said:

Is it hard to describe the trick for allowing linters to persist information? I am just curious.

What Eric said is correct: there is an IO.Ref that stores the "current" imports. This IO.Ref is accessed by the linter after each command: if the commands are parsed linearly, then what each command sees is the effect of having modified the IO.Ref with all the previous commands.

[Damiano Testa]

If, instead, the file is not parsed linearly, then you do not know how modified it before you access it and everything becomes confused.

[Damiano Testa]

Edward van de Meent said:

how was the syntaxtree visualisation made?

I have a custom function that displays Syntax and Expr trees.

[Damiano Testa]

Violeta Hernández said:

I imagine Lean linters are written in Lean; is deep knowledge of the language required or does general knowledge on functional-style languages suffice?

They are written in Lean, indeed. The fact that the language is the same, means that everything is familiar. If you have done some meta-programming, a linter is simply a function from Syntax that runs in the CommandElabM monad.

[Damiano Testa]

Jesse Alama said:

is there a tool to dump a parse tree in e.g. XML or JSON format, or does one need to write a custom linter akin to the ones talked about here?

I played around with a flexible linter that you can activate with a piece of syntax and then flags those uses.

[Damiano Testa]

It worked reasonably well, but it was never PRed to mathlib.

[Jesse Alama]

Damiano Testa said:

Violeta Hernández said:

I imagine Lean linters are written in Lean; is deep knowledge of the language required or does general knowledge on functional-style languages suffice?

They are written in Lean, indeed. The fact that the language is the same, means that everything is familiar. If you have done some meta-programming, a linter is simply a function from Syntax that runs in the CommandElabM monad.

Perhaps one could make a custom linter that emits the syntax tree in a format I have in mind. (In other words, just to repeat the earlier comment about linters all the way down, we need a linter to enable more linting!)

[Bolton Bailey]

Michael Rothgang said:

Great talk, thanks! Let me ask my question here, in case the answer is useful more permanently:
If I like working on linters and want to help out, are there any particular places which need help?

Probably different people have different opinions about what's most important, but I made #7217 as a tracking issue for desired linters, based both on the mathlib style guide and zulip conversations/my own thoughts. People should feel free to use that issue as inspiration or edit things into the list there if they'd like.

[Thomas Murrills]

Jesse Alama said:

is there a tool to dump a parse tree in e.g. XML or JSON format, or does one need to write a custom linter akin to the ones talked about here?

Although probably of general interest and definitely useful for some task, my instinct would be to #xy this in any specific case: I'd guess that working within Lean would be the nicest way to interact with syntax trees!

[Joachim Breitner]

I had to run after the first 10mins, so sorry if this was answered during the talk: Why are the environments linters not automatically run at the end of the file (as if every file ended with #lint)?

[Eric Wieser]

I think the answer is "environment linters aren't part of Lean itself, they're just a program that lives in Batteries". I don't believe there is any way to run something at the end of a file, in general?

[Jannis Limperg]

I believe this has been discussed before, but I would love linters that suggest a fix rather than just saying "there's a problem here". We have all the infrastructure (linters and code actions); we just need to teach Lean not to kill code actions when it resets the environment after a linter has been run.

[Eric Wieser]

yes, there is an open issue about that (edit: thanks, lean4#4363)

[Ayhon]

The issue in question:
https://github.com/leanprover/lean4/issues/4363https://github.com/leanprover/lean4/issues/4363

[Joachim Breitner]

Eric Wieser said:

I don't believe there is any way to run something at the end of a file, in general?

Maybe worth a feature request? It would be great if mathlib contributers would have to wait for CI to come back to be reminded to lint their files.

[Damiano Testa]

You could have a syntax linter that, on reaching the end of a file runs #lint and reports the outcome if there are errors.

[Sebastian Ullrich]

I believe there are some environment linters like simp theorems that require a project-wide view, they would get weaker when run at the end of each file

[Michael Rothgang]

Your #20750 even does that :racecar:

[Damiano Testa]

Indeed, this is not the "final" word on environment linters, but it would catch quite a few issues early, I think.

[Sebastian Ullrich]

Clearly there are declaration linters, module linters, and library linters

[Damiano Testa]

Anyway, I wrote it just as a proof of concept: the fact that it can be done like this, does not mean that this is how is should be done!

[Michael Rothgang]

Having the docBlame linter nudge me early seems certainly nice to have. (Perhaps it should just run #lint only docBlame? Or opt out of certain linters, like the simpNF one?)

[Pietro Monticone]

:video_camera: Video recording: https://youtu.be/734jMwgjkkM

[Eric Wieser]

Michael Rothgang said:

Your #20750 even does that :racecar:

Does Parser.isTerminalCommand really fire on the end of a file? Or only on #exit?

[Damiano Testa]

It fires on #exit, the end of the file and at imports.

[Damiano Testa]

The firing at the end of file is prevented by setting the linter option.

[Damiano Testa]

The firing at import is not relevant for the linter, since linters do not actually run after import commands.

[Damiano Testa]

The implementation of isTerminal is simply

def isTerminalCommand (s : Syntax) : Bool :=
  s.isOfKind ``Command.exit || s.isOfKind ``Command.import || s.isOfKind ``Command.eoi

[Damiano Testa]

When lean parses a file, it adds a "fictitious" eoi node to "close off" the file and the linter latches onto that. I made the linter work also on #exit since otherwise testing it is hard.

[Damiano Testa]

However, this linter is another one that would require a nolints file and I am not too convinced that it is better to have it as a syntax linter, than simply running it in CI.

[Eric Wieser]

I did not expect linters to be run against eoi!

[Damiano Testa]

Already the long file linter does that. And maybe also the minImports linter.

[Damiano Testa]

In fact, the longFile linter takes the position information of eoi and decides what to do.

[Damiano Testa]

(This is the linter that is a pain to test and having a file with multiple #exit is very convenient for testing the various settings.)

[Damiano Testa]

In fact, given how linters run, eoi is the only "anchor" that they have to some absolute information about a file. Everything else is little more than heuristic.

[nrs]

I enjoyed the talk very much! I was wondering if code was available for the linters mentioned in the slide about in-progress/prototype linters? In particular I'm currently working on a connected declarations linter to find not only minimal imports but also minimal Name references in each declaration. In any case, very interested to see future work in this area, is there anything you would recommend following to keep up to date with this?

[Damiano Testa]

The development of code for finding connected declarations is partly on hold, since this comment.

[nrs]

Oh that topic is directly relevant to what I'm trying to do, thank you! Thanks again for the talk, have begun digging through the source of some linters you mention

[Damiano Testa]

As for available code: I think that I linked most available PRs. A lot of the tools that should go into finding connected declarations have in fact become independent tools that are mostly merged.

[Damiano Testa]

Useful functions are getUsedConstants and friends, but they only give Expr information: to get a file that actually builds, I had developed the code that became the minImports linter, accessing syntax and tactic information.

[Damiano Testa]

After that, to get which variables in scope are needed, I have been developing tools to work with that, which is partly how the unusedVariable linter (#17715) came about (this still requires work).

[nrs]

Ah I see! Thanks for taking the time, will be going through the references you mention today

[Damiano Testa]

No problem! If you see a specific missing reference, let me know and I will try to dig it out, but not everything is really "available".