Built-in Lean formatter

Stream: Editors & UIs

[Willem vanhulle]

Hi I have been using a fork of Lean4 repo with a built in Lean code formatter for a week. Seems to work relatively reliable. It uses the pretty term formatter of Lean for code and some simple conventions for top level items https://github.com/wvhulle/lean4

[Willem vanhulle]

Let me know if anyone is interested in up streaming parts of this. :)

[Lua Viana Reis]

While it is not upstreamed, could it live in an external server plugin? This way, it could be run on top of normal lean versions. I wrote a small external LSP plugin once and it was reasonably simple (but I don't know about this case), it was possible to add additional LSP methods with builtin_initalize and registerLspRequestHandler.

[Willem vanhulle]

Lua Viana Reis said:

While it is not upstreamed, could it live in an external server plugin? This way, it could be run on top of normal lean versions. I wrote a small external LSP plugin once and it was reasonably simple (but I don't know about this case), it was possible to add additional LSP methods with builtin_initalize and registerLspRequestHandler.

I don’t think formatting is possible in user space. The lean4 repo only exposes certain lsp capabilities

[Willem vanhulle]

It can give it another try to make a seperate extension but the lsp capabilities are kind of hard wired in the server module in lean4 repository

[Anthony Wang]

Willem vanhulle said:

Hi I have been using a fork of Lean4 repo with a built in Lean code formatter for a week. Seems to work relatively reliable. It uses the pretty term formatter of Lean for code and some simple conventions for top level items https://github.com/wvhulle/lean4

Cool! I've been planning on writing a Lean formatter for a while, but looks like you beat me to it. :smile:

I tried it out on some of my Lean files and it seems to work great. Also, is there some way to run the formatter as a command-line tool rather than using the "Format Document" option is VSCode?

[Patrick Massot]

Are you both aware that the Lean FRO is very actively working on writing a Lean code formatter?

[Willem vanhulle]

I have seen that message several times over the past years on the Lean FRO blog post and yearly goals, but have not been able to find it. Could I offer any help?

[Patrick Massot]

Are you sure you’ve seen that? The roadmaps are all about stuff they would like to do, not about stuff they are very actively working on.

[Willem vanhulle]

Ah maybe it was on the roadmap that I saw it a while ago. Apologies.

But it seems like everything is ready. The pretty formatter is there. Just need to add the capability to the lsp server and format the things not covered by the pretty formatted like comments. I’ve done that at my fork.

Anything we can do to avoid double work? On which branch is the rest working?

[Anthony Wang]

@Willem vanhulle I think I found a bug in your formatter when formatting multiline strings, for instance:

#eval "Hello
world"

gets formatted into

#eval
  "Hello
    world"

which is already wrong, but if you keep formatting the file, it adds four more spaces each time before world.

[Anthony Wang]

Also, is it intentional that the formatter adds an extra newline after comments?

[Willem vanhulle]

Anthony Wang said:

Willem vanhulle I think I found a bug in your formatter when formatting multiline strings, for instance:

#eval "Hello
world"

gets formatted into

#eval
  "Hello
    world"

which is already wrong, but if you keep formatting the file, it adds four more spaces each time before world.

Will fix that

[Willem vanhulle]

It is a problem with the exiting formatter of strings in main (outside of the code i added).

[Willem vanhulle]

@Anthony Wang Fixed it by removing the problematic behaviour where Lean formatter would add an indent tab to multiline strings