formatter

Stream: lean4

[Jakob von Raumer]

Is anyone working on building a formatter for Lean (i.e. producing "nice" Syntax from Syntax)? Maybe one that broadly follows the mathlib style guide?

[Patrick Massot]

There was a relevant talk during the Lean Together workshop last year.

[Patrick Massot]

See https://leanprover.zulipchat.com/#narrow/stream/419231-Lean-Together-2024/topic/A.20Pretty.20Expressive.20Printer.20-.20Sorawee.20Porncharoenwase/near/412181215

[Patrick Massot]

I know this doesn’t answer your question, but hopefully it is still relevant.

[Jakob von Raumer]

Thanks, that's at least a start. I think I've actually seen the talk and completely forgot about it :sweat_smile:

[Jakob von Raumer]

Would be cool to have such a thing written in Lean though

[Jakob von Raumer]

Are you still working on the topic, @Sorawee Porncharoenwase ?

[Patrick Massot]

It would be extremely useful, but it seems very non-trivial.

[Jakob von Raumer]

It doesn't have to be optimal in order to be useful though, something that works better than an elaboration + pretty printer roundtrip would already be an improvement

[Mario Carneiro]

yeah I don't think that paper is particularly relevant for making a formatter for lean code. All the complexity is elsewhere

[Jakob von Raumer]

My motivation for asking is that I have a tool that spits out less than perfect Lean code and it would be very cool if that could be reformatted by a function that already knows about precedences (to remove brackets) and preferences for breaks and indentations

[Henrik Böving]

Jakob von Raumer said:

Would be cool to have such a thing written in Lean though

I have an implementation of the algorithm on my github. Its "just" that someone has to write the formatter for each kind of syntax that can exist and then we are ready to go^^

[Mario Carneiro]

@Jakob von Raumer if that's all you need, lean's pretty printer is probably good enough. It was good enough for mathport

[Mario Carneiro]

The hard part of writing a formatter is making something that doesn't destroy code which has already been manually formatted (in a style approved way), like mathlib

[Eric Wieser]

The pretty printer also destroys -- comments, right?

[Mario Carneiro]

not lean's

[Mario Carneiro]

it's actually already been tuned quite a bit for this use case because it was needed for mathport

[Eric Wieser]

import Mathlib

open Lean Elab PrettyPrinter

elab "printme" cmd:command : command => do
  Lean.logInfo (← Lean.Elab.Command.liftCoreM <| Lean.PrettyPrinter.ppTerm ⟨cmd.raw⟩ )
  Lean.Elab.Command.elabCommandTopLevel cmd

printme
def ohno (n : ℕ) -- oops
  : n = 1 := sorry

gives

def ohno
    (n : ℕ)
      -- oops :
    n = 1 :=
  sorry

which is illegal syntax

[Henrik Böving]

Mario Carneiro said:

The hard part of writing a formatter is making something that doesn't destroy code which has already been manually formatted (in a style approved way), like mathlib

I'm not sure if thats a relevant criterion. In languages that use a formatter by default like e.g. go everyone just accepts the formatting or at worst turns it off for a specific code piece

[Eric Wieser]

(but you're right, the comment _is_ kept)

[Mario Carneiro]

@Henrik Böving it's true, but in that case the formatting needs to be really good so that people don't complain that the buggy formatting is not correctable because it will be reverted

[Mario Carneiro]

I don't think lean's formatter is at that level, it has trouble even making correct syntax in some cases

[Mario Carneiro]

(as eric shows)

[Mario Carneiro]

although to be fair lean's parser is turing complete so correct formatting is basically undecidable

[Edward van de Meent]

Wait what

[Edward van de Meent]

I suppose the fact that the language is extensible (and you get to define your own syntax) does make that likely I guess... I hadn't thought about it like that before

[Edward van de Meent]

Perhaps it would help to make it a bit more concrete as to what a formatter should fix... Indentation? Spacing? Use certain variants of characters (thinking of mapsto)? Remove redundant brackets?

[Jakob von Raumer]

Using certain variants of characters can be done with delaborators, removing redundant brackets is already done by the pretty printer, so I guess indentation and line breaks are the main points?

[Mario Carneiro]

yes, most of the mistakes in the pretty printer relate to using too many line breaks or getting indentation wrong (sometimes resulting in syntactically incorrect or invalidly parsed output)