Compile Lean code to a neat little executable

Stream: lean4

[Huỳnh Trần Khanh]

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]

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

[Huỳnh Trần Khanh]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

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]

Anyways, thanks!

[Yaël Dillies]

Hello from the future, how do I create an executable from my super slow Lean code?

[Yaël Dillies]

I am running lake build on my project with a lakefile that looks like

import Lake
open Lake DSL

package Catam

@[default_target]
lean_lib Catam

lean_exe catam where
  root := `Catam

require mathlib from git "https://github.com/leanprover-community/mathlib4"@"master"

(note that I don't have bleeding edge lake, but I'm not managing to update it). And Catam.lean contains def main : IO Unit := .... When running lake build, I would expect to find my executable as build.bin.Catam.exe, but nothing!

[Yaël Dillies]

Am I doing something wrong?

[Sebastian Ullrich]

build builds the default targets. Use build catam or apply [default_target] to it.

[Yaël Dillies]

What does

@[default_target]
lean_lib Catam

if not applying {default_target] to Catam.lean?

[Henrik Böving]

it compiles Catam.lean as a library (i.e. a set of .olean files) not as an executable (i.e. a set of .c files that get turned into .o files that get turned into a binary)

[Yaël Dillies]

Aaah, you mean I should make the executable a default target?

[Henrik Böving]

yes

[Yaël Dillies]

Okay, now I get a bunch more exciting errors :grinning:

[Henrik Böving]

Also note that just because our compiler is pretty cool :tm: doesn't mean that it will magically make everythign fast :P

[Yaël Dillies]

I know that the complexity of my algorithm must be through the roof, but at least I can let an executable run overnight. The examiners don't have to know

[Yaël Dillies]

Here are the new errors. Does that smell like I should update lake, or is it something different?

$ lake build Catam
Building Std.Linter.UnreachableTactic
Building Std.Linter.UnnecessarySeqFocus
error: > LEAN_PATH=.• PATH c:⋃ -DwarningAsError=true -Dlinter.missingDocs=true .· -R .· -o .· -i .· -c .· error: stdout:
.· error: invalid {...} notation, expected type is not of the form (C ...)
  Linter
error: external command `c:⋃ exited with code 1
error: > LEAN_PATH=.• PATH c:⋃ -DwarningAsError=true -Dlinter.missingDocs=true .· -R .· -o .· -i .· -c .

[Sebastian Ullrich]

It works in your editor?

[Yaël Dillies]

The file compiles in my editor, I have the infoview, yada yada

[Sebastian Ullrich]

But it fails on a file of your project, not on Std?

[Yaël Dillies]

Nevermind, I restarted the server and everything broke :sad:

[Sebastian Ullrich]

And it's from the [default_target] change? It looks more like a Lean version conflict between Std and your project.

[Yaël Dillies]

I think it's because I tried to update lake (and god knows what commands I ran), so you're right and it's a version mismatch. How do I get out of version hell?

[Sebastian Ullrich]

and god knows what commands I ran

That does sound like a problem

[Sebastian Ullrich]

Usually you shouldn't touch any more than lean-toolchain for that

[Yaël Dillies]

I tried elan update lake, elan update.

[Mauricio Collares]

Manually edit your lean-toolchain file to point to the 2023-04-20 nightly

[Henrik Böving]

Yaël Dillies said:

I know that the complexity of my algorithm must be through the roof, but at least I can let an executable run overnight. The examiners don't have to know

what are you doing? :eyes:

[Yaël Dillies]

Finding matchings in bipartite graphs. Can't be that hard :grinning:

[Henrik Böving]

The good matching algorithms are pretty good complexity wise right?

[Yaël Dillies]

You're overestimating the chair-keyboard interface

[Reid Barton]

The bad algorithms are also pretty bad.