include lean.h

Stream: lean4

[Floris van Doorn]

Another stupid question: How do I compile and run code? I can compile a file using lake env lean ... -c ....
If I just stupidly compile this C file, I get an error that lean/lean.h is not found (at line 4: #include <lean/lean.h>).
How do I compile this C file correctly?

[Henrik Böving]

There is an FFI example over here https://github.com/leanprover/lake/blob/master/examples/ffi/lakefile.lean that shows how to marry C and Lean 4 code.

[Floris van Doorn]

I see, that is useful. Can I somehow use this to compile tactics/programs from a single file in the mathlib4 repository (which, by default doesn't compile its files)?

[Arthur Paulino]

@Floris van Doorn more specifically, this part tells the compiler where the lean/lean.h header is:
#["-I", (← getLeanIncludeDir).toString]

[Arthur Paulino]

Floris van Doorn said:

I see, that is useful. Can I somehow use this to compile tactics/programs from a single file in the mathlib4 repository (which, by default doesn't compile its files)?

What do you mean? Do you want to define a function in Mathlib4 that runs C code?

[Sebastian Ullrich]

@Floris van Doorn AFAIK, Lake can only build a single library or executable per package right now. But you can change binRoot to temporarily point at an appropriate module and then use lake build :bin.

[Floris van Doorn]

Ok, let me take a step back.

I am trying to collect all declarations in the environment and do some operations on them. When doing this with #eval inside Lean, these operations are starting to become really expensive, and I was wondering if using compiled code instead of interpreted code would help here.

So if I understand the comments correctly, I now have to write a function
def main (strs : List String) : IO UInt32 := ...
then use lake build with the appropriate configuration to run the code after compiling it?
Or can I do the compilation from Lean itself (using compileO?)

Also, how do I pass (data computed from) the current environment to the compiled function (if the function I compile lives in IO)?

[Gabriel Ebner]

What operations are you trying to do? The interpreter isn't that slow, and mathlib4+lean is pretty small.

[Patrick Massot]

Maybe he is operating on binport output?

[Floris van Doorn]

I was also a bit surprised that it would already slow down. I might have some inefficient code.
I'm trying to do a kind of page rank on the declarations. So it mostly involves mapping functions over arrays and Float operations.

[Floris van Doorn]

I am currently just doing it on mathlib4+Lean, but the idea is to later do it on the binport output. Unfortunately the former is already slow.

[Floris van Doorn]

The (very messy) file is here: https://github.com/leanprover-community/mathlib4/blob/fpvandoorn/graph/Personal/Graph.lean

[Sebastian Ullrich]

If you're on Linux, you can get a rough idea of what it is spending time on by running perf top in parallel

[Floris van Doorn]

A majority of the computation time seems to be spent on a quicksort:

def sortRevByWeight (g : Array NameNode) : Array NameNode :=
g.qsort λ nn1 nn2 => nn1.weight > nn2.weight

Here nni.weight are Floats

[Floris van Doorn]

and the array is about 27k entries long.

[Sebastian Ullrich]

Ah, makes sense. qsort will be specialized to the comparison function, so it cannot use any precompiled version. And LLVM will make a much better job of the resulting code than the interpreter.

[Floris van Doorn]

If interesting, these are the top entries of sudo perf top

  18.93%  libleanshared.so              [.] lean_inc_ref_cold
  18.42%  libleanshared.so              [.] lean_dec_ref_cold
  11.17%  libleanshared.so              [.] lean::ir::interpreter::eval_body
  11.14%  libleanshared.so              [.] lean::rb_map<lean::name, lean::ir::interpreter::symbol_cache_entry, lean::name_quick_cmp>::find
   9.00%  libleanshared.so              [.] lean::ir::interpreter::call
   7.86%  libleanshared.so              [.] lean_name_eq
   3.53%  libleanshared.so              [.] lean_inc
   3.04%  libleanshared.so              [.] lean::ir::interpreter::pop_frame
   2.72%  libleanshared.so              [.] lean::ir::interpreter::lookup_symbol
   2.36%  libleanshared.so              [.] lean::ir::interpreter::eval_expr
   2.28%  libleanshared.so              [.] lean::ir::interpreter::stub_m
   1.06%  libleanshared.so              [.] std::__1::vector<lean::ir::value, std::__1::allocator<lean::ir::value> >::__append
   0.85%  libleanshared.so              [.] lean::ir::interpreter::stub_m_aux
   0.71%  libleanshared.so              [.] lean::mk_pair<lean::name, lean::ir::interpreter::symbol_cache_entry>
   0.52%  libleanshared.so              [.] lean::rb_map<lean::name, lean::ir::interpreter::constant_cache_entry, lean::name_quick_cmp>::find

[Sebastian Ullrich]

That definitely looks like the interpreter :)

[Sebastian Ullrich]

Floris van Doorn said:

So if I understand the comments correctly, I now have to write a function
def main (strs : List String) : IO UInt32 := ...
then use lake build with the appropriate configuration to run the code after compiling it?

Yes, I think that is the simplest way currently.

Also, how do I pass (data computed from) the current environment to the compiled function (if the function I compile lives in IO)?

You can't directly. You can get an Environment in the compiled program by running importModules, in which case you should run the binary inside lake env so that LEAN_PATH is set correctly.

[Henrik Böving]

I implemented this over here: https://github.com/hargoniX/doc-gen4/blob/main/DocGen4/Load.lean if you want some place you can copy paste from :P (its largely adapted from the compiler and language server though)

[Floris van Doorn]

Sebastian Ullrich said:

You can't directly. You can get an Environment in the compiled program by running importModules, in which case you should run the binary inside lake env so that LEAN_PATH is set correctly.

Thanks! So something like this?

def main (strs : List String) : IO UInt32 := do
  let env ← importModules [{module := `Mathlib}] {}
  let u ← EIO.toIO (λ _ => "error") (CoreM.run' test {} {env := env})
  return 0

[Floris van Doorn]

Henrik Böving said:

I implemented this over here: https://github.com/hargoniX/doc-gen4/blob/main/DocGen4/Load.lean if you want some place you can copy paste from :P (its largely adapted from the compiler and language server though)

Thanks, I'll take a look

[Sebastian Ullrich]

Ah, you also need to run

initSearchPath (← Lean.findSysroot?) ["build/lib"]

before importModules. Then you don't even need lake env if you run the executable from the project root.

[Floris van Doorn]

@Sebastian Ullrich I think I'm getting closer. I now have the following files:

-- Mathlib/Graph.lean
[...]

def main (strs : List String) : IO UInt32 := do
  initSearchPath (← Lean.findSysroot?) ["build/lib"]
  let env ← importModules [{module := `Mathlib}] {}
  let u ← CoreM.toIO test {} {env := env}
  return 0

and

-- lakefile.lean
import Lake

open Lake DSL

package mathlib { binRoot := `Mathlib.Graph }

I can compile the file fine with lake build. However, running ./build/bin/mathlib gives me

uncaught exception: could not find native implementation of external declaration 'UInt64.ofNatCore' (symbols 'l_UInt64_ofNatCore___boxed' or 'l_UInt64_ofNatCore')

Searching on Zulip gives me similar errors using leanpkg where the solution is to add the option LINK_OPTS=-rdynamic. Do I have to do something similar with lake?

[Sebastian Ullrich]

Ah, you can use supportInterpreter := true in the lakefile for that

[Arthur Paulino]

@Floris van Doorn This helped me when I got that error:
add supportInterpreter := true to the package in the lakefile

[Floris van Doorn]

Thanks, that works!

[Floris van Doorn]

The qsort which was the bottleneck when interpreted is ~100 times faster now :-)