Parsing Lean4

Stream: lean4

[Daniel Donnelly]

What is the easiest way to parse Lean4 into an expression tree? For example toplevel: a folder, subsequent: files / folers, within each file: and expression tree of the various Lean4 constructs. Everything OOP preferably. I think the Lean4 kernel (C++) would already do this, is that correct?

[Max Nowak 🐉]

Not sure if I understood the question, but... the best way to parse lean is using the lean compiler itself, since you can extend lean's syntax in lean and have custom elaborators etc. So if you want to build some tooling for lean, you'd probably just add that functionality to the lean compiler itself, I think? (I'm not a lean dev, I just hacked a few things on my own)

[Max Nowak 🐉]

What are you trying to accomplish?

[Daniel Donnelly]

Max Nowak 🐺 said:

What are you trying to accomplish?

First, we're making a Quiver-based editor (a single-page calculator basically) site that converts your diagram into some Lean code. It would be nice in the future if this communication were two way, and the only way I can see to do that faithfully / robustly would be to parse Lean.

[Daniel Donnelly]

For example, they can functor a diagram into a new diagram, that will have its own data in the lean code

[Daniel Donnelly]

Any suggestions ?

[Daniel Donnelly]

I already am aware of the CD widget, but it doesn't do everything (yet)

[Daniel Donnelly]

@Max Nowak 🐺 I guess another way to do this would be the same as widget's approach: there are some specialized lean objects that communicate with the widget side. So that means we could probably code everything in Lean4 itself without messing with the kernel. These objects need to support editing though of their properties from the widget.

[Daniel Donnelly]

I'll start here:
https://code.visualstudio.com/api/get-started/your-first-extension

[Daniel Donnelly]

I guess what we want to do is get the Quiver js app to run inside of VsCode.

[Daniel Donnelly]

I'll also reverse engineer how the current widgets api works

[Scott Morrison]

Yes, the only way to parse Lean is with Lean. If you try anything else you will end up unhappy. :-)

If you'd like an example of using the Lean Frontend, see https://github.com/semorrison/lean-training-data/blob/master/TrainingData/Frontend.lean, which includes functions to process a file, returning a String, a Syntax, and an Environment for each declaration in the file (along with error messages and info trees!)

[Scott Morrison]

Sorry this isn't a nicely document tutorial, but it's a starting point. :-)