Running lean function from c++

Stream: lean4

[Tomas Skrivan]

I would like to generate some C code with Lean and then call it from C++. Here is an attempt in a minimal example, but running it causes segmentation fault.

// main.cpp

#include <iostream>
#include <lean/lean.h>

#include "main.h"

int main(){

  auto obj = test_string(42.0);
  auto str = lean_to_string(obj);

  std::cout << str->m_data << std::endl;

  lean_dec(obj);

  return 0;
}

// main.lean

@[export test_string]
def test_string : Float → String := λ x => "Hello World " ++ x.toString

I compile and run this with lean -c main.h main.lean && leanc -x c++ main.cpp -o main && ./main Unfortunately, this causes segmentation fault.

When generating main function from lean, the C code looks like:

  int main(int argc, char ** argv) {

    lean_object* in; lean_object* res;
    lean_initialize_runtime_module();
    res = initialize_main(lean_io_mk_world());
    lean_io_mark_end_initialization();
    if (lean_io_result_is_ok(res)) {
      lean_dec_ref(res);
      lean_init_task_manager();
      res = _lean_main(lean_io_mk_world());
    }
    if (lean_io_result_is_ok(res)) {
      int ret = lean_unbox(lean_io_result_get_value(res));
      lean_dec_ref(res);
      return ret;
    } else {
      lean_io_result_show_error(res);
      lean_dec_ref(res);
      return 1;
    }
  }

The crucial part seems to be lean_initialize_runtime_module() the rest seems to be error handling and IO monad. After some digging I have found lean/init_module.h containing lean::initialize_runtime_module and lean::finalize_runtime_module but running these does not fix the problem.

[Sebastian Ullrich]

You have to call initialize_main as well. There is no header for that, but you can copy the signature from the generated code and declare it as extern "C".

[Tomas Skrivan]

But what object am I supposed to pass to initialize_main ? There is lean_io_mk_world() in the generated code, but what if I'm not interested in IO?

[Tomas Skrivan]

Ok I did extern "C" lean_object* initialize_main(lean_object* w) and then initialize_main(nullptr). It works but looks sketchy.

[Sebastian Ullrich]

Initializing a Lean module is inherently IO. The actual value of the parameter doesn't matter, but please just use lean_io_mk_world.

[Tomas Skrivan]

Cool, it works :)

[Sebastian Ullrich]

Technically you should also check the result (though in this case, initialization cannot fail) and free it

    lean_io_mark_end_initialization();
    if (lean_io_result_is_ok(res)) {
      lean_dec_ref(res);
      lean_init_task_manager();
    } else {
      lean_io_result_show_error(res);
      lean_dec_ref(res);
      throw ...;
    }

We might want to supply a helper function for doing that at some point.