Zulip Chat Archive

@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: Dec 20 2023 at 11:08 UTC