Zulip Chat Archive

Stream: new members

Topic: Lean formatter

Huỳnh Trần Khanh (Feb 11 2021 at 07:01):

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 (Feb 11 2021 at 07:01):

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

Huỳnh Trần Khanh (Feb 11 2021 at 07:02):

or forbid non terminal simp

Johan Commelin (Feb 11 2021 at 07:05):

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

Johan Commelin (Feb 11 2021 at 07:05):

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

Kevin Buzzard (Feb 11 2021 at 08:38):

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 (Feb 11 2021 at 11:48):

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 (Feb 11 2021 at 11:48):

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

Bryan Gin-ge Chen (Feb 11 2021 at 15:17):

This should be doable in Lean 4, though!

Josiah Eldon Bills (Sep 17 2022 at 03:23):

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 (Sep 17 2022 at 15:26):

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.

Last updated: Dec 20 2023 at 11:08 UTC