Compiling Lean to binary

Stream: new members

[Jesse Vogel]

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]

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

[Jesse Vogel]

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]

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]

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

[Mario Carneiro]

@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.