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 (
Reid Barton (Jan 25 2021 at 12:57):
If you have a project set up properly, then
leanmake bin should do it
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.
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
Patrick Massot (Jan 25 2021 at 13:43):
See also https://leanprover.github.io/publications/ for papers and 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):
Last updated: May 07 2021 at 13:21 UTC