Zulip Chat Archive

Stream: new members

Topic: Compiling Lean to binary

Jesse Vogel (Sep 22 2021 at 09:49):

Hi everyone! I'm a bit new to lean, did some proofs, and I'm thinking of using lean for some programming project. Is it possible to program in lean and compile it as a binary? That is, similar to Haskell's main function. I think I heard lean4 could do such things, is it also possible with lean3?

Johan Commelin (Sep 22 2021 at 10:10):

@Jesse Vogel does https://github.com/agentultra/lean-for-hackers help?

Jesse Vogel (Sep 22 2021 at 12:26):

Thank you! That definitely helps in setting up the main function. Am I then correct that it is only possible to run such programs via lean --run and not possible to compile them?

Johan Commelin (Sep 22 2021 at 12:31):

I'm not sure. I've never tried. But for such use cases, it's probably better to try out Lean 4 already.

Johan Commelin (Sep 22 2021 at 12:31):

It is (and certainly will be) much better suited for programmy stuff.

Mario Carneiro (Sep 22 2021 at 19:13):

@Jesse Vogel That's correct. Lean 3 is an interpreter, like python, so you have to invoke it to run lean 3 programs. Lean 4 is a compiler, so it will generate standalone executables.

Last updated: Dec 20 2023 at 11:08 UTC