Best Practices for writing lean4 parsers.

Stream: lean4

[Andreas K.]

Hello, I am working on a research project, that tries to extend lean4 syntax to allow for more natuaral theorem proving language.
The end goal should be similar to PatrickMassout's lean-verbose for lean3.
I am very new to lean4 and I am struggling both with documentation (which can be aided by reading the manuals and browsing the source code) and to get the philosophy of lean4. (Typically I would think rewriting the source code of the language is a bad idea...)

My question is this: How do you write a lean4 parser while conforming to best practices?
How do you ensure usability (i.e. you can just import parser and there you go)?
What should I do and shouldn't do? (Rewriting the source code is a no-no, or it's ok if you follow xyz guidelines).

Another approach would be to write a program that takes a say .txt file as input and outputs a runnable .lean file. This can be done in other programming languages (and given my ignorance of lean4 appears to be more straight forward to me).
What would a lean4 expert say? What ressources should I check out? What requirements would a parser need to fulfill that you would consider using it?

Thank you so much :thanks:

[Jason Rute]

Best practice is not to write a Lean 4 parser. Lean 4 is very extensible. This makes it hard to parse if not impossible without using Lean itself. But it also makes it possible to extend Lean without changing it. I imagine could implement your ideas via this same extensibility. I think this is basically what Patrick did. So you wouldn't write a new Lean, but use Lean to add your own syntax ideas.

[Jason Rute]

Sorry, I mistook which project of Patrick you were talking about. I was thinking of a more recent project in Lean 4 (that I'm having trouble finding the repo for at the moment).

[Jason Rute]

Here is a video demo of the project of @Patrick Massot that I was referring to: https://www.youtube.com/watch?v=tp_h3vzkObo. (Edit: I might be mistaken about whether this project uses Lean macros. It does at the end with the Python example, but I don't know about the main talk. In particular, this is about outputting existing Lean proofs and not writing new Lean proofs.)

[Jason Rute]

Also see this video of @Sebastian Ullrich which shows the power of Lean's macros which let you implement custom DSLs in Lean: https://www.youtube.com/watch?v=n1Pd0GeHsAY

[Jason Rute]

I think the Lean metaprogramming book is a place to learn about this stuff, but it is probably better to start learning the basics of Lean as in Theorem Proving in Lean and maybe Functional Programming in Lean, if you don't know them already.

[Jason Rute]

You may also want to look a the natural number game for Lean 4 and in particular its code at https://github.com/leanprover-community/lean4game. This is another example of a special user interface built on top of Lean 4.

[Patrick Massot]

There two completely different project here. Informal Lean is all about the output format after parsing an existing regular Lean file. Verbose Lean is about the input format and is only a teaching tool (where the goal is to teach ordinary maths instead of maths in Lean). I made a tiny start at porting Verbose Lean to Lean 4 more than one year ago, but I should return to it. And indeed this involves no modification to core Lean. It simply uses the extensibility capabilities of Lean (and Lean 3 was already extensible enough for this).

[Andreas K.]

Wonderful, thank you very much for your quick responses! :)