the internals of lean4 compiler

Stream: lean4

[Keith]

I am compiler engineer but new to lean4 compiler, and I wanna study it in details. Therefore, I wonder if there is any documents or resources about the internals of lean4 compiler or so. Any help would be appreciated. :thank_you:

[Utensil Song]

For one, An Extensible Theorem Proving Frontend, probably the best source besides lean4-metaprogramming-book, #leantt , source code (lean4 and lean4lean), and Zulip. Some interesting details can also be found in another thesis User interfaces for computer-assisted mathematics.

These are all about the frontend part of the lean4 compiler, the backend is LLVM (Clang), using C as IR.

lean4-alloy makes use of many lean 4 frontend features and worth studying, and it has also potential for C++ code generation etc. lean4-partax is a library of tools for manipulating Lean syntax and parser definitions. There is also Megaparsec in this area. (Lean 4 also has a Parsec in its own code base.)

LeanGccBackend has some interesting work based on GccJit . thread.

[Keith]

cool, thx. I will check out what you mentioned. :thank_you: