Why is tree-sitter-lean exist if lean has it's own parser?

[brando90]

Why is tree-sitter-lean exist if lean has it's own parser? Why not use that + lean is an extensible PL which means the syntax can be extended at any time -- no?

[Julian]

(This parser essentially is paused for development, so in some sense it doesn't really exist.)

But essentially:

• to be able to interact with the tree-sitter ecosystem, which has lots of nice tools for general programming languages, so why not Lean
• to be able to parse Lean without a running server
• yes syntax is extensible but 1) most of the time people are using some fixed modern tool given the way Lean's ecosystem works and 2) tree-sitter itself has some dynamic capabilities

So yeah, this isn't very useful in its current state, but some day I suspect it will be if we can get tree-sitter to behave with Lean's grammar.

[brando90]

awesome! thank you. So if I want to parse lean and manipulate it in python for example what do you recommend?

[brando90]

related: https://proofassistants.stackexchange.com/questions/5020/why-use-tree-sitter-lean-or-pypantograph-to-extract-lean-4-constructs-like-eval