## Stream: lean4

### Topic: Compile Lean code to a neat little executable

#### Huỳnh Trần Khanh (Jan 25 2021 at 12:55):

How do I compile Lean code to a neat little executable? I know how to compile the Lean code into C but I have no idea how to compile the C code into an executable, it seems that the C code depends on some runtime library (<lean/lean.h>).

#### Reid Barton (Jan 25 2021 at 12:57):

If you have a project set up properly, then leanmake bin should do it

#### Kevin Buzzard (Jan 25 2021 at 13:15):

This stream :-) It was only released three weeks ago! Leo has given a bunch of talks about it. You know about the LT2021 talks I guess but Leo has certainly given other talks

#### Kevin Buzzard (Jan 25 2021 at 14:00):

@Huỳnh Trần Khanh it occurs to me that you might also like to look at Reid Barton's solutions to advent of code 2020: https://github.com/rwbarton/advent-of-lean-4 . It might be interesting to port them to the release version of Lean 4, for example.

#### Huỳnh Trần Khanh (Jan 25 2021 at 16:21):

It seems that the AoC solutions only use Lean as a functional programming language, not as a theorem prover. So this is not quite what I'm looking for.

#### Huỳnh Trần Khanh (Jan 25 2021 at 16:22):

Anyways, thanks!

Last updated: May 07 2021 at 13:21 UTC