Tips for VS Code

Stream: new members

[Martin C. Martin]

When developing in VS Code, double clicking sorry just shows an error message, but single clicking on it shows the tactic state. Replacing sorry with _ also shows the tactic state.

What other tips and tricks are useful to know when using Lean in VS Code?

[Martin C. Martin]

Is there a way to set up automatic indenting?

[Martin C. Martin]

Is there a pretty printer for Lean, along the lines of clang-format (C++) or black (Python)?

[Patrick Massot]

Not yet. In will come in Lean 4 (but not very soon).

[Martin C. Martin]

It seems it should be straight forward to write one, as long as Lean 3 is straight forward to parse. I've only seen a little of the language, but it seems easy to parse so far.

What would be the best language to write the pretty printer in? Lean itself, or is it unsuited to writing tools like that?

[Martin C. Martin]

What is Lean itself written in? OCaml? Self-hosted?

[Henrik Böving]

Lean 4 is self hosted (for the most part a tiny bit of C++ is there still but not because it has to be but rather because the devs are busy with other stuff than removing it right now) and compiles to C, Lean 3 is written in C++ and a bytecode language.

[Henrik Böving]

Furthermore parsing Lean 4 in general is highly non trivial because users can extend the syntax in any way they desire, however Lean 4 also has large meta programming faciliities that allow you to access basically all information the compiler has about the code so you could use it to write a formatter

[Martin C. Martin]

That's cool, I've often wanted extensible syntax and great meta programming facilities. For a few years I programmed professionally in Common Lisp and since then always wanted a language where the meta language was the language itself.

Sorry I wasn't clear, I was asking about how easy / hard it is to parse Lean 3, to make a pretty printer for Lean 3. Is the C++ parser for Lean 3 reasonably separable? Does it keep things like line and column information and whitespace, or does it toss them?

[Henrik Böving]

Not a question I am qualified to answer, for Lean 4 the answer is no, comments and whitespaces are discarded as far as I know (although you can make your custom syntax extensions sensitive to them)

[Alex J. Best]

The tools written to help port lean 3 to lean 4 (https://github.com/leanprover-community/mathport) might be useful for writing a parser.
One ingredient of the above is that you can run lean --ast file.lean to get an AST representation of what lean sees, which could certainly be helpful in writing a formatter. But this would still need a lot of work to get something acceptable out I believe, so maybe not really worth the effort.

[Martin C. Martin]

Thanks to both of you.