Implementing independent kernel

Stream: lean4 dev

[Saul Shanabrook]

Hello! I attended @Leonardo de Moura's great talk yesterday on Lean 4 and in it he mentioned how there are multiple independent implementations of the lean kernel. I assume he meant for lean 3? I am curious if there are any independent implementations of the lean4 kernel?

I am asking because I am wondering if trying my hand at implementing my own version of the lean 4 kernel could be a good learning exercise, to get a practice dependent type theory with a clear scope.

I see that the current kernel is here: https://github.com/leanprover/lean4/tree/master/src/kernel and I saw elsewhere that lean communicates with this over FFI.

So if I say wrote my own kernel in another language, could I hook it up to lean 4 to get it to use it to try it? Also, is the kernel language/API specified somewhere?

Thanks!

[Sebastian Ullrich]

Hi Saul! As far as I know, there are no independent type checkers for Lean 4 yet, no; I believe https://github.com/ammkrn/nanoda had/has some partial support.

Contributing a checker would be very welcome and could be an interesting exercise if you are already familiar with using type theory and want to learn about the minute details of implementing one. Note that this will invariably consist of consulting the C++ code as well as #leantt and my thesis on Lean 4 tell you about the rules of the type system, but not how to implement them.

Independent checkers in Lean 3 made use of a simple text format that could be exported by Lean. I have a tool for doing this in Lean 4 as well: https://github.com/Kha/lean4export. There is also code in mathlib4 for this but I don't know how they compare.

[Arthur Paulino]

We built a Lean 4 typechecker in Lean 4, but it typechecks content-addressed versions of definitions, theorems etc. It might serve as a reference.

https://github.com/lurk-lab/yatima/tree/main/Yatima/Typechecker

[Sebastian Ullrich]

Adapting a Lean 3 checker is also a possibility. 90+% of the code should be unaffected.

[Saul Shanabrook]

Thank you for all of the pointers!

Independent checkers in Lean 3 made use of a simple text format that could be exported by Lean. I have a tool for doing this in Lean 4 as well: https://github.com/Kha/lean4export. There is also code in mathlib4 for this but I don't know how they compare.

I see the one that was added in mathlib4: https://github.com/leanprover-community/mathlib4/commit/8f76c3bafc98c3362b2dd1c6af3a7c0f3050fb4f @Mario Carneiro do you know how it compares to lean4export?

We built a Lean 4 typechecker in Lean 4, but it typechecks content-addressed versions of definitions, theorems etc.

When you say its content-addressed versions, you mean each one has a unique ID to reference it? And this makes the kernel different to implement?

[Arthur Paulino]

It's content-addressed and name-agnostic, to be more precise.

def foo := Nat.zero and def goo := Nat.zero are hashed to the same hash. There are further consequences of this design choice though.

[Saul Shanabrook]

Ah I see how that could affect the structure of the checker.

[Mario Carneiro]

Saul Shanabrook said:

Thank you for all of the pointers!

Independent checkers in Lean 3 made use of a simple text format that could be exported by Lean. I have a tool for doing this in Lean 4 as well: https://github.com/Kha/lean4export. There is also code in mathlib4 for this but I don't know how they compare.

I see the one that was added in mathlib4: https://github.com/leanprover-community/mathlib4/commit/8f76c3bafc98c3362b2dd1c6af3a7c0f3050fb4f Mario Carneiro do you know how it compares to lean4export?

We built a Lean 4 typechecker in Lean 4, but it typechecks content-addressed versions of definitions, theorems etc.

When you say its content-addressed versions, you mean each one has a unique ID to reference it? And this makes the kernel different to implement?

I actually forgot about both lean4export and this old Util.Export implementation. It's probably worth making them compatible with each other, and maybe upstreaming it to Std