minimal lean-to-olean compiler

Stream: lean4

[alpharee]

Hey, I'm not that familiar with the Lean 4 codebase yet, so I thought I’d ask here before spending days digging around.

I’m looking to build a minimal standalone tool that takes a .lean file and compiles it into a .olean file - no project setup, no imports, just a single file in, compiled output out.
Basically, I want the smallest possible program that replicates what Lean does when it compiles .lean files, but stripped down to just that core functionality. For research reasons, I’d like to keep it as minimal and self-contained as possible.

Is there something like this already, or could it be easily extracted from Lean itself? I couldn't find much documentation about this part of the toolchain, so any pointers would be really appreciated.

Thanks!

[Johan Commelin]

I think this is a really hard problem. Lean is extremely extensible. There is a folklore theorem that says "to parse Lean you have to be Lean". (Note that this only talks about parsing!)

[metakuntyyy]

Maybe interesting for me as well but what would your use cases for .olean files be? Do you have stuff that you'd like to do with them?

[Kyle Miller]

I think that you need most of Lean for this.

There are some parts that can be stripped out for batch compilation though: the LSP server, possibly the pretty printer, the incremental compilation system, and maybe a small handful of others. Everything else is somehow part of the language.