Lean formatter

Stream: new members

[Huỳnh Trần Khanh]

in JavaScript there is this pretty tool called prettier that prettifies my code. is there an equivalent tool for Lean? and also is there a Lean linter to catch some style errors?

[Huỳnh Trần Khanh]

for example i want to ban all uses of theorem in my Lean code because theorem sounds pompous

[Huỳnh Trần Khanh]

or forbid non terminal simp

[Johan Commelin]

We don't have a code formatter. There are a bunch of linters in mathlib, but not for non-terminal simp.

[Johan Commelin]

They do catch unused hypotheses or bad simp lemmas, and things like that

[Kevin Buzzard]

I don't understand enough about linters to know whether they would be capable of checking for nonterminal simps. Isn't there some sort of limitation as to what they can do? Some nonterminal simps are ok, eg I think simp, ring is ok for closing a goal because even if simpgets smarter it's highly unlikely to break a ring proof which worked before

[Anne Baanen]

It has been a while so this may have been fixed, but my understanding is that linters can only access the output of a tactic, not the tactic script itself. So finding nonterminal simps is basically undoable (in Lean 3).

[Anne Baanen]

Writing a Lean formatter in Lean will be difficult too for the same reason.

[Bryan Gin-ge Chen]

This should be doable in Lean 4, though!

[Josiah Eldon Bills]

There is an old thread about how there isn't a formatter for Lean. Is this still true? If not, does the Lean parser produce a parse tree (sometimes called a concrete syntax tree) with whitespace still present that could be used to make one?

[Henrik Böving]

We are working on this for Lean 4, the plan is that eventually the standard Lean 4 PrettyPrinter will be able to print our a standartized, formatted version of any Lean code there is, but right now that is still quite a bit away from what it can do.