reusing the Lean compiler in my program?

Stream: lean4

[Jason Gross]

How much of the lean compiler can I reuse in a Lean program? Like, suppose I want to open a file from disk, run it through lean, and get:

• the list of lines
• the list of error messages and their associated row:col ranges
• a structured representation of the document where I have nodes for each namespace, section, command, etc, and where I can walk the AST and get source ranges for each node

Is this mostly straightforward by using the right stdlib functions, or do I have to rewrite some of it myself?

(I'm getting sufficiently tired of minimizing examples by hand that I'd like to start porting my Coq bug minimizer to Lean for auto-minimizing test cases.)

[Sebastian Ullrich]

Yes, this is absolutely possible and how the language server works. The server is a bit complicated by asynchronicity etc, so it's probably better to look at the noninteractive top level function: https://github.com/leanprover/lean4/blob/54405c4543dab3d3c537d0c26965e186e9ce42c4/src/Lean/Elab/Frontend.lean#L92-L99
You can see how it prints the error messages, and s.commands : Array Syntax gives you access to the file's concrete syntax tree

[Jason Gross]

Thanks!