FFI

Stream: general

[Conor Bergin]

Is it possible return a lean string from a cpp function without wrapping it in an IO monad? Every thing I try produces errors to do with symbols not being found. This works :

extern "C" lean_obj_res my_string() {
    return lean_io_result_mk_ok(lean_mk_string("hello"));
}

with:

@[extern "my_string"] opaque myString : IO String

Can I just return a string?

[Marcus Rossel]

You should be able to just use lean_mk_string and remove the IO. What errors are you getting?

[Tomas Skrivan]

I think the issue is that @[extern "my_string"] opaque myString : String does not have any arguments. Compiler considers it to be a constant that is supposed to be set during initialization and that does not seem to play well with FFI.

If you call lean myString.lean -c myString.c on
myString.lean

@[extern "my_string"]
opaque myString : String

It generates

code

// Lean compiler output
// Module: myString
// Imports: Init
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
#pragma clang diagnostic ignored "-Wunused-label"
#elif defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wunused-parameter"
#pragma GCC diagnostic ignored "-Wunused-label"
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
#ifdef __cplusplus
extern "C" {
#endif
extern lean_object* my_string;
lean_object* initialize_Init(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_myString(uint8_t builtin, lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_initialized = true;
res = initialize_Init(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_myString = _init_l_myString();
lean_mark_persistent(l_myString);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus
}
#endif

You can see that it is trying to initialize myString with

l_myString = _init_l_myString();
lean_mark_persistent(l_myString);

When you write

@[extern "my_string"] opaque myString : BaseIO String

Then for the compiler the function is effectively Unit → String×Unit and it won't try to initialize it as a constant.

I would consider this as a bug. A solution to it would be to define your function as:

@[extern "my_string_thunk"] opaque myStringThunk (_ : Unit) : String

def myString := myStringThunk ()

and on C side

lean_object* my_string_thunk(lean_object*){
  return lean_mk_string("hello");
}

(I didn't test this fully so there might be a detail I missed)

[Solomon]

I'm not sure if this should go in a new thread, but I'm trying to use the C FFI to callout to libcurl. pkg-config is showing the library in scope:

➜ pkg-config --list-all | grep libcurl
libcurl         libcurl - Library to transfer files with ftp, http, etc.

But its not getting picked up by Lean:

libc++abi: terminating due to uncaught exception of type lean::exception: error loading library, ./.lake/build/lib/libleanffi.so: undefined symbol: curl_global_cleanup

Any help would be appreciated.

EDIT:

Looks like I just needed to add moreLinkArgs := #["-lcurl"] to my package declaration.

[Jürgen Bergmann]

@Solomon , please look at my Lean bindings package to libcurl https://github.com/bergmannjg/leanCurl

[Solomon]

Jürgen Bergmann said:

Solomon , please look at my Lean bindings package to libcurl https://github.com/bergmannjg/leanCurl

Oh this looks great. Why don't you have it listed on https://reservoir.lean-lang.org/ ?

[Tomas Skrivan]

There is lower bound on starts to be listed on reservoir. Two stars might not be enough and there might be other necessary metric.

[Jürgen Bergmann]

The metric is a root lakefile.lean, 2 stars and a OSI approved licence How Reservoir boosts your Lean packages