Lean's components

Stream: general

[Johan Commelin]

I think I saw a presentation by Johannes Hölzl several years ago, where he had a diagram that showed how all Lean's components interacted: parser, elaborator (including tactic framework, type class resolution), kernel, virtual machine, etc...

Does someone know hot to get

• that diagram, or
• an equivalent diagram, or
• a textual representation of something like that?

[Jason Rute]

In early versions of the Lean 4 presentations given by @Sebastian Ullrich there were such diagrams for Lean 3 and Lean 4. For example: http://leanprover.github.io/talks/vu2019.pdf

[Jason Rute]

Also try this image search: https://www.google.com/search?q=lean+prover+kernel&tbm=isch&oq=lean+prover+kernel

[Johan Commelin]

Thanks! That's exactly the kind of diagram I'm looking for!

[Sebastian Ullrich]

For the backend, there's also http://leanprover.github.io/talks/WITS2022.pdf#page=6

[Johan Commelin]

Thanks! That's helpful!