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)

[Willem vanhulle]

Hi I have discovered the script/reformat.lean file in the Lean4 repo. I salvaged it and made it type checking again.

However there is a runtime exception for any non-trivial piece of input Lean4 source code.

Is anyone working on this? I could start work on it but I assume someone must already have thought about realising a production ready formatter?

[Zixiao Wang]

do you mean sth like an auto formatter? I also run into the same question today, seems like vscode has no LEAN4 auto formatter right now...

[Henrik Böving]

reformat.lean should not be used as an autoformatter. There has been some basic investigation into this matter and there is going to be work done on this as part of the FRO roadmap at some point.

[Willem vanhulle]

Henrik Böving zei:

reformat.lean should not be used as an autoformatter. There has been some basic investigation into this matter and there is going to be work done on this as part of the FRO roadmap at some point.

Yes, reformat.lean does not really seems functional.

What do you mean by "part of the FRO roadmap"? Can you estimate how many months in the future that would be?

I could try to start work on a formatter, but I am fairly new to Lean and I assume other people have already tried this. It seems like it would be quite hard because there is a lot of custom syntax and notation.

[Henrik Böving]

There has been quite some discussion on this matter that you can find on this Zulip and it is indeed a very non trivial task . If you are new to Lean this is not a project I would recommend as it requires quite some understanding of the Lean meta programming facilities. I cannot give a concrete estimation for when exactly the FRO is going to pick up on this right now unfortunately.