Zulip Chat Archive

Stream: Program verification

Topic: executables

Christopher Upshaw (Apr 20 2021 at 02:40):

It is possible to make an executable file with lean, right? Do I have to call some other compiler? Am I just missing an obvious option?

Joe Hendrix (Apr 20 2021 at 04:12):

@Christopher Upshaw With Lean 4 you can, but not with Lean 3.

Christopher Upshaw (Apr 20 2021 at 05:28):

Okay that explains things. Thank you!

Mario Carneiro (Apr 20 2021 at 19:47):

I think leanpkg is a shell script that does lean --run leanpkg.lean, so you can do that sort of thing for lean 3 programs

Johan Commelin (Apr 20 2021 at 19:49):

Probably relevant: https://agentultra.github.io/lean-for-hackers/

James King (Jun 12 2021 at 19:26):

Should I do one for Lean 4? :thinking:

Kevin Buzzard (Jun 12 2021 at 19:30):

Given that there is very little out there for lean 4 I would imagine that it would be a popular post!

Agnishom Chattopadhyay (Oct 03 2022 at 20:07):

That would be great indeed. Lean 4 seems to have a number of cool things built into its design (like /Functional But In Place/) and I would be very interested in building binaries with it

Henrik Böving (Oct 03 2022 at 20:36):

You can start right away :P

Adam Topaz (Oct 03 2022 at 22:16):

In case it wasn't clear from the above: https://agentultra.github.io/lean-4-hackers/

Last updated: Dec 20 2023 at 11:08 UTC