parsing

Stream: general

[Zaz Brown]

Hello all! I'm brand new to Zulip and Lean. I'm interested in bijective parsing and welcome any pointers. Specifically, what is the advantage of the external lean4-parser library over the built-in Lean.Parser?

[Zaz Brown]

Also, what is parsing efficiency like in Lean? And would Lean be a good language to develop a bijective parser and prove it correct? Would it be fairly easy to develop a simple proof-of-concept or are there hurdles I'm missing here?

[Edward van de Meent]

Zaz Brown said:

Specifically, what is the advantage of the external lean4-parser library over the built-in Lean.Parser?

the difference between these is in their scope: lean4-parser is a library for parser combinators, meaning it gives a FP definition of a parser and how to run it. Lean.Parser instead is used for extending leans language itself, define custom notation to use in the same file, etc.

[Edward van de Meent]

which is to say, a Lean.Parser can get called by the compiler to parse (parts of) lean files.

[Zaz Brown]

@Edward van de Meent Thank you! Isn't Parser.Lean also a library for parser combinators? The docs seem to describe it as such.

I understand the intended use of Lean.Parser is to extend the language itself, but is there anything that restricts it from parsing any arbitrary (well-behaved) language? I.e. is Lean.Parser not a general-purpose parser-combinator library with some added features to make it integrate with Lean itself?

Or is it somehow specialized in a way that makes implementing arbitrary languages hard?

[Zaz Brown]

@François G. Dorais @Arthur Paulino

[Arthur Paulino]

Not exactly sure why I was ping'd here. But our team developed a parsing library called Megaparsec.lean 3 years ago.

A word of caution: we haven't had the time to perform any perf analysis for this lib yet.

[François G. Dorais]

Lean.Parser and lean4-parser, Megaparsec.lean, Std.Internal.Parsec are completely different conceptually. You can use Lean.Parser to parse just about anything text-based. See https://github.com/leanprover/verso for example.

[Zaz Brown]

Thank you both for your quick responses!

[Zaz Brown]

Arthur, sorry to disturb, I just pinged you because I saw your Megaparsec library and you invited people there to contact you on Zulip. I thought you might have some insight into the differences between the different parsing libraries.

[Zaz Brown]

@François G. Dorais Could you elaborate? When would it make sense to use lean4-parser instead of Std.Internal.Parsec?

[Zaz Brown]

I don't really understand the differences and have yet to find good documentation on them.

[Edward van de Meent]

(always, since Std.Internal.Parsec is internal)

[Zaz Brown]

@Edward van de Meent Thanks. What is the issue with that? It seems the Lean JSON parser and XML parser both use Std.Internal.Parsec.

[Markus Himmel]

See my message here. Basically, you should expect that important features are missing and that the API will change between versions without warning.

[Zaz Brown]

Ahh, okay. Thank you!

[Arthur Paulino]

Zaz Brown said:

Arthur, sorry to disturb, I just pinged you because I saw your Megaparsec library and you invited people there to contact you on Zulip. I thought you might have some insight into the differences between the different parsing libraries.

Oh, I see. It's been a while :sweat_smile: