Zulip Chat Archive

Stream: lean4

Topic: Self hosted kernel

Anders Christiansen Sørby (Dec 22 2021 at 08:36):

How far along is the self hosted lean kernel? Is there any attempt to reimplement the cpp kernel kode in lean?

Marcus Rossel (Dec 22 2021 at 08:49):

There was some thread recently where Leo talked about this. IIRC there's more important things to get done first (like the Mathlib port) so the path to a self hosted kernel could be started in a year at best.

Marcus Rossel (Dec 22 2021 at 08:51):

E7EB65E8-2156-49DE-BE6A-4F27694FA8D5.png

Sebastian Ullrich (Dec 22 2021 at 08:52):

@Marcus Rossel You're probably thinking of the compiler backend - https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Lean4.20Debugger/near/264244446. Rewriting the kernel is even (far) lower priority than that, I'd say.

Mario Carneiro (Dec 22 2021 at 08:52):

That said I don't think there is any reason not to try your own hand at this. If you think of it as an external verifier then it's a moderate size project to do in lean 4, probably well within its current capabilities

Sebastian Ullrich (Dec 22 2021 at 08:53):

Just maybe skip reduceBool in the first version :laughing:

Last updated: Dec 20 2023 at 11:08 UTC