Zulip Chat Archive

Stream: lean4

Topic: Compile Lean code to a neat little executable


view this post on Zulip 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>).

view this post on Zulip Reid Barton (Jan 25 2021 at 12:57):

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

view this post on Zulip Huỳnh Trần Khanh (Jan 25 2021 at 13:11):

Awesome! Where can I learn more about Lean 4 aside from the official docs? Some talks could be helpful.

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jan 25 2021 at 13:43):

See also https://leanprover.github.io/publications/ for papers and talks.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Huỳnh Trần Khanh (Jan 25 2021 at 16:22):

Anyways, thanks!


Last updated: May 07 2021 at 13:21 UTC