parsing text with lean

Stream: lean4

[Petar Maymounkov]

I’d like to write a parser combinator library in lean to evaluate how it fits this task relative to other languages. Is there any documentation of OS practicalities (effectful operations) like: how does reading a file work? making directories? network calls, etc? executing processes?

[Reid Barton]

There is https://github.com/leanprover/lean4/blob/master/src/Lean/Data/Parsec.lean in the standard library

[Henrik Böving]

Documentation is not perfect yet, you can try digging through the Init Module here https://leanprover-community.github.io/mathlib4_docs/ which contains the majority of IO related stuff, especially Init.System (https://leanprover-community.github.io/mathlib4_docs/Init/System/IO.html) , that one should cover file and process related things.

Networking is not in the repo this documentation was generated for but there does exist a package over here https://github.com/xubaiw/lean4-socket by @Xubai Wang although it might not compile anymore since it's been quite a bit since the last update so maybe compiler changes have broken stuff.

Apart from that there are a few other libraries related to OS stuff you can find by looking around on Github or in the chat log mostly, as Reid pointed out there is this basic parser combinator library already as well, docs for that would be here https://leanprover-community.github.io/mathlib4_docs/Lean/Data/Parsec.html

@Petar Maymounkov

[Henrik Böving]

If there is OS related stuff you are missing you can also add that yourself in a library if you want...I wouldn't say that it's "easy" but definitely not too complicated either once you understood how the FFI mechanism works (feel free to ask for help if you need some of course^^).

[Gabriel DORIATH DÖHLER]

It might be possible to reuse part of the lean parser code to build a parsing library. https://github.com/leanprover/lean4/blob/master/src/Lean/Parser/Basic.lean seems to be useful. I didn't manage to create an example but I would be interested if someone can.

[Anders Christiansen Sørby]

I have partially extended the Parsec library here https://github.com/Anderssorby/Nix.lean with better error messages and with a more compositional approach. If it helps.