Parsing external file with Lean `syntax` parsers

Stream: Is there code for X?

[Ayhon]

One can extend Lean's parser with syntax commands. I wonder if there is a function that would allow us to run these parsers defined through syntax on external files, so if for instance I embed a DSL in Lean, I'm able to use this same parser to parse external files.

[Kyle Miller]

Yes, it's possible to run parsers on files or strings.

It's easiest to do at compile time (e.g. define a command that loads an external file and parses it, creating some top-level declarations that you can make use of later in the file).

It's possible to create compiled executables that parse at run time too, but then you need a way to make all the parser descriptions be available. One way is to embed Lean and load your module to create an environment object with all the loaded parsers. Another approach is to turn those parsers into equivalent compiled code; for that see @Mac Malone's Partax library. I haven't used it myself, but it's a solid concept.

[Ayhon]

I talked today with Ulrich in the Lean Office Hours and he recommended I look into
testParseFile and importModules to generate an environment where the parsers are loaded. He did also mention some other library going on a different direction, but I didn't get a name, so thank you for sending it my way! So far I don't need anything too professional, so just having a way to actually parse at runtime file would suffice. I'll look into Partax though, it seems interesting

[Kyle Miller]

Just to check, what does "at run time" mean to you? In a compiled application? Or while compiling a Lean file? The second one is the easier one, what I called "at compile time".

[Ayhon]

At run time to me means that I can give the parsing function a variable with a file path, instead of using a string literal. That is, a compiled application is able to use the function to parse an arbitrary file

[Jakub Nowak]

There's also Lean.Parser.runParserCategory if you want to read from a string, and you can even specify syntax category.

[Jakub Nowak]

But you still need to create Environment which I didn't find out how to do.

[Jakub Nowak]

Or you can run it inside macro, in which case you just get access to current environment. But it means that the input will be parsed in you current environment with all the declarations. Depending on what you want to do, maybe it's not a problem though.

[Kyle Miller]

@Jakub Nowak Getting an environment is indeed the tricky part if the goal is creating a compiled executable. You need the executable to include Lean itself, then build an environment by importing the appropriate modules. This is what Ayhon is going for.

Your suggestions would work for things done at compile time (i.e. running parsers while evaluating commands while Lean is compiling a file).

[Ayhon]

Jakub Nowak said:

But you still need to create Environment which I didn't find out how to do.

This was answered to me by Sebastian Ulrich, he said there's an importModules function which I could use. I haven't figure out how to use it yet, but it seems like it's implementation is in the C++ side of Lean, according to GitHub code search. I need to spend some time into it

[Ayhon]

Otherwise, Partax may be a good replacement, looking at the README it seems promising and not difficult to use.

[Kyle Miller]

You could try taking something like https://github.com/leanprover-community/repl and stripping out everything you don't need. I mention it because it's an example of a compiled program that imports modules and manipulates an environment. Make sure to take note of supportInterpreter in the lakefile.

If Partax works, then that's simpler, since you can create a self-contained executable. No need to distribute your executable with compiled oleans, etc.

[Asei Inoue]

Is this related to #Is there code for X? > get Parser from Lean ?
Partax is what I need?