Zulip Chat Archive

Stream: new members

Topic: Documentation of Lean's architecture


view this post on Zulip Horatiu Cheval (Feb 12 2021 at 14:10):

I've seen people discussing various components such as the kernel, the VM or the elaborator, but I don't have a clear picture of what everything does and how it fits together. Is there a place where I can learn about these things?

view this post on Zulip Bryan Gin-ge Chen (Feb 12 2021 at 16:04):

I don't know that there's a single good place to read about this, but there are a bunch of papers and presentations on the official Lean website. The more detailed papers "The Lean Theorem Prover" and "Elaboration in Dependent Type Theory" are quite out-of-date since they describe Lean 2 but might still be helpful.

view this post on Zulip Horatiu Cheval (Feb 13 2021 at 08:30):

Thanks, I checked the papers, they explained pretty much what I wanted to know. I suppose the general notions carry over from Lean 2 to the newer versions.


Last updated: May 14 2021 at 04:22 UTC