Bootstrapping

Stream: lean4

[Hanting Zhang]

I'm looking through the Lean source code for Expr and I'm confused by how Lean in defining itself. Before Expr is defined, are Lean binaries elaborating Lean code into some kind of Exprs? If that question even makes any sense. I guess in general, how is Lean bootstrapping itself?

[Sebastian Ullrich]

It's no different from other bootstrapping compilers. The Expr that is compiled into the binary is completely independent from the Expr that is eventually elaborated in the stdlib and finally compiled into the next stage's binary.

[Hanting Zhang]

Oh wait, I see. I was confusing myself thinking the binaries and Expr were working together in some way

[Sebastian Ullrich]

That would be true for elaborators etc. run in the interpreter, but all elaborators in the stdlib are built-in, i.e. not executed before being compiled into the next stage's binary

[Sebastian Ullrich]

We do run some other programs such as parsers in the interpreter though, which is when you get to the fun bootstrapping issues described in https://leanprover.github.io/lean4/doc/dev/bootstrap.html#further-bootstrapping-complications