## Stream: general

### Topic: Lean kernel

#### Albert ten Napel (Jul 06 2020 at 12:45):

Hi everyone, where can I read up on the exact details of the Lean kernel?

#### Johan Commelin (Jul 06 2020 at 12:51):

Mario's master thesis is a good read. After that: the source code.

#### Johan Commelin (Jul 06 2020 at 12:51):

https://github.com/digama0/lean-type-theory/tags

#### Johan Commelin (Jul 06 2020 at 12:52):

Note that Mario's thesis is really about the type theory, not about nitty gritty implementation details. Not sure what you're after.

#### Albert ten Napel (Jul 06 2020 at 12:53):

Thanks! This thesis is exactly what I was looking for :)

#### Carl Friedrich Bolz-Tereick (Jul 06 2020 at 13:38):

Out of curiosity, is there something about the nitty gritty implementation details?

#### Simon Hudon (Jul 06 2020 at 13:44):

If you look at the code, there are comments and references to papers that different parts are based on but that's pretty much it

Thanks

#### Carl Friedrich Bolz-Tereick (Jul 06 2020 at 13:46):

I suppose I should just start reading the C++ code

#### Simon Hudon (Jul 06 2020 at 13:48):

Are you looking for any particular information?

#### Carl Friedrich Bolz-Tereick (Jul 06 2020 at 13:49):

No, mostly curious (I've worked on various more traditional VMs)

#### Simon Hudon (Jul 06 2020 at 13:58):

But the kernel and the VM are not the same things

#### Chris B (Jul 07 2020 at 12:16):

@Carl Friedrich Bolz-Tereick
There are also implementations of the kernel in Haskell, Scala, and Rust in the form of reference type checkers if you're more familiar with any of those. The Scala one is the most concise, but AFAIK the Rust one is the only one that's been updated to match the kernel changes from Lean 3 to Lean 4. I'm almost done with a specification of the kernel that was written in Lean just for the sake of convenience; I'll post it in the program verification channel probably at the end of the week. IIRC the only thing that isn't in the Rust one yet from Lean 4 is the new reduction procedure for mutual inductives.

#### Patrick Massot (Jul 07 2020 at 12:20):

If this is useful information for people interested in what the Lean kernel actually does then I don't understand why you want to post it to an obscure stream instead of here.

#### Gabriel Ebner (Jul 07 2020 at 12:23):

I didn't know that nanoda already supports the mutual inductives. (Are there other relevant changes? At some point there was talk about number literals in the kernel.) Is there an export tool for Lean 4?

#### Chris B (Jul 07 2020 at 12:23):

@Patrick Massot I dunno man it just seemed to fit. I'll put it in general if that's more agreeable.

#### Chris B (Jul 07 2020 at 12:29):

There's no export tool yet no, but the changes are backwards compatible with a couple of small adjustments like keeping the distinction between dependent/non-dependent recursors and adding the new reduction procedure for recursors and quotients. The C++ one has support for number literals and I think now string literals last time I checked, there are two new declaration types (Theorem and Opaque), a couple of other changes. I can put a summary of the changes in a gist or something if you'd like.

#### Gun Pinyo (Apr 10 2021 at 04:02):

Chris B said:

Carl Friedrich Bolz-Tereick
There are also implementations of the kernel in Haskell, Scala, and Rust in the form of reference type checkers if you're more familiar with any of those. The Scala one is the most concise, but AFAIK the Rust one is the only one that's been updated to match the kernel changes from Lean 3 to Lean 4. I'm almost done with a specification of the kernel that was written in Lean just for the sake of convenience; I'll post it in the program verification channel probably at the end of the week. IIRC the only thing that isn't in the Rust one yet from Lean 4 is the new reduction procedure for mutual inductives.

@Chris B Could you give me some reference to the source code of the rust implementation of Lean 4?

Sorry for digging the old post. But I start to curious about the kernel of Lean 4, in particular, using Rust instead of C++ to implement the kernel. I try not to duplicate any topic by searching old topics then found out that you said there is indeed a Rust version of Lean4.

#### Mario Carneiro (Apr 10 2021 at 06:06):

@Gun Pinyo https://github.com/ammkrn/nanoda_lib

#### Mario Carneiro (Apr 10 2021 at 06:08):

I don't know that you could call it a "Rust version of lean 4" so much as an external typechecker for lean 4 kernel terms, similar to the external typecheckers trepplein, tc, and leanchecker for lean 3. These programs don't read lean source files, they read the "export format" which consists of pre-digested proof terms

#### Chris B (Apr 10 2021 at 09:24):

@Gun Pinyo
It's sort of in limbo right now since I'd like it to be able to work with Lean 3 export files and Lean 4 is still rapidly evolving.

The changes from 3 to 4 that I can think of off the top of my head are as follows; the items that have been realized in the one Mario linked are starred:

• support for mutual inductives
support for nested inductive reduction

• support for mutual definitions

• removal of reduction rules
• direct inductive reduction
• direct quotient reduction
• theorem/opaque declaration types
• abbrev/opaque transparency levels
Proj exprs
convert local to fvar (I may or may not end up doing this one)

There's also the native bool/nat/string reduction which I is a more nuanced issue but isn't breaking with respect to basic functionality. The Rust one that uses arenas isn't the most pleasant to read, but feel free to reach out if you have any questions. The spec I mentioned in that post exists in the trace branch, but it models the Rust executable with inductive relations so isn't much better to read. For what it's worth I am very serious about doing a Lean in Lean executable as soon as well-founded recursion lands in Lean 4. If the experts in the community help refine it I think we'll end up with a really nice learning resource.

#### Jason Rute (Apr 10 2021 at 13:37):

As far as the Lean in Lean executable, I'm curious how realistic it would be to write a verified Lean kernel checker in Lean. And by verified, I guess I mean there is a theorem which says that this Lean kernel checker is sound and complete for Lean's logic. (Although, I guess it depends how we encode "Lean's logic" here. If we just encode it as the implementation of our kernel checker, then the proof is trivial. :smile:) (Of course for an added bonus, one could prove that Lean's logic, as we encode it, is consistent so that our checker never accepts a proof of false. For this I assume one would need to assume a certain number of inaccessible cardinals or some such construct to get around Gödel's 2nd incompleteness theorem.)

#### Jason Rute (Apr 10 2021 at 13:39):

Oh, if we want to prove something about the implementation it must be implemented with total functions which probably means at least for definitional equality that we need some proof of normalization (or whatever the correct term is). I wonder how hard that is to prove (and if it requires a proof that Lean is consistent or not).

#### Chris B (Apr 10 2021 at 14:07):

I probably should have clarified (and I'm not suggesting you read this in what I wrote, only that your comment made me think of it) that the idea would just be to have an interesting thing people can play around with rather than trying to do any verification or demonstrate any particular result.

Last updated: May 13 2021 at 18:26 UTC