Zulip Chat Archive

Stream: new members

Topic: Lean formatter


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Huỳnh Trần Khanh (Feb 11 2021 at 07:02):

or forbid non terminal simp

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Feb 11 2021 at 07:05):

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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Anne Baanen (Feb 11 2021 at 11:48):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 11 2021 at 15:17):

This should be doable in Lean 4, though!


Last updated: May 17 2021 at 21:12 UTC