Zulip Chat Archive

Stream: general

Topic: Lean's components


Johan Commelin (Nov 01 2022 at 15:31):

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 (Nov 01 2022 at 22:09):

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 (Nov 01 2022 at 22:16):

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

Johan Commelin (Nov 02 2022 at 06:14):

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

Sebastian Ullrich (Nov 02 2022 at 08:43):

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

Johan Commelin (Nov 02 2022 at 09:38):

Thanks! That's helpful!


Last updated: Dec 20 2023 at 11:08 UTC