FFI External Object

Stream: general

[Schrodinger ZHU Yifan]

I have several questions regarding the external object:

1. where should I register for an external class? via an #[init] routine?
2. once an external object is returned from FFI, what type should I use to represent its handle inside lean?

For example, I want to have an external object representing aligned byte array:

image.png

[Tomas Skrivan]

You define an opaque type on lean level, have a look at this example which defines a new type S. And here it is defined on C++ level.

[Mac Malone]

And these lines show how the external class is initialized.

[Schrodinger ZHU Yifan]

cool, thanks a lot

[Schrodinger ZHU Yifan]

One thing I find interesting is that FBIP actually provides a canonical way to wrap imperative data structures to FP without having too much overhead or introducing ST monad. On each modification, one just check&ensure the exclusivity. As long as the user is using it linearly, it will not incur much overhead.

[Schrodinger ZHU Yifan]

I managed to make a proof of concept implementation of porting rust's hashbrown to lean directly via FFI. It seems to work. However, lean.h inlined several non-trivial functions which make the FFI in rust a little bit more harder to write. Is there any suggestion on improving this?

[Sebastian Ullrich]

There is https://crates.io/crates/lean-sys (unofficial)

[Mario Carneiro]

Speaking of which, I have an improved version of that crate and also some beginning work on a proper type-aware lean-FFI crate for rust (unreleased)

[Schrodinger ZHU Yifan]

For immutable FFI operations, is it recommended to use @& or to manage the refcount myself? I think they are similar performance-wise?

[Mario Carneiro]

@& is better if you don't actually need to consume a reference

[Schrodinger ZHU Yifan]

Ok. And, is there a thing of @& inside a closure? lean_apply_X(f, args..) seems to always assume that f will consume args.

[Mario Carneiro]

yes, that's right

[Mario Carneiro]

uniform-ABI function calls consume all their arguments

[Mario Carneiro]

only extern function calls and non-_boxed functions can use @&

[Schrodinger ZHU Yifan]

I see. That clarifies things. Thanks a lot!

[Schrodinger ZHU Yifan]

Sebastian Ullrich said:

There is https://crates.io/crates/lean-sys (unofficial)

I really appreciate this work but there are some problems with such crate: the unsafe marker is not correct in rust perspective; the build script scans for .so without respecting the OS it runs on. Hope this will help to improve it.

[Henrik Böving]

Schrodinger ZHU Yifan said:

Sebastian Ullrich said:

There is https://crates.io/crates/lean-sys (unofficial)

I really appreciate this work but there are some problems with such crate: the unsafe marker is not correct in rust perspective; the build script scans for .so without respecting the OS it runs on. Hope this will help to improve it.

Why would the unsafe marker not be okay? Unsafe means memory unsafety in rust and doing an FFI call is her inherently memory unsafe, especially if it is to C. The entire point of these crates is that someone writes a second crate above it that ensures they are only called safely

[Schrodinger ZHU Yifan]

sorry for the confusion. I mean there are some functions without unsafe but actually they are unsafe. For example, lean_dec should also be unsafe -- although it checks lean_is_scalar, it is up to the user to make sure the pointer passed in points to either a boxed scalar or a valid lean_object. You can write lean_dec(RANDOM_VALUE as _) in safe rust, and it leads to UB/SEGVFAULT. Therefore, in rust's perspective, calling such function without care is unsafe :)

[Schrodinger ZHU Yifan]

The implementation is a little bit strange:

#[inline]
pub fn lean_inc(o: *mut lean_object) {
    if !lean_is_scalar(o) {
        lean_inc(o)
    }
}

Won't this lead to infinite recursion? I thought it should be lean_inc_ref inside the if body.

[Schrodinger ZHU Yifan]

I am really looking forward to it. I got some ideas on providing a rust2lean feature that supports easy conversion from rust type to lean functionalities. I think we can also have something like automatically generating FFI files from rust to lean (or the reverse way?) that reduce human errors.

// A wrapper to `lean_object` that holds reference counting.
// On clone, it calls `lean_inc`; on drop it calls `lean_dec`;
// One can create `LeanObjectRef` from this without increasing refcnt.
#[repr(transparent)]
struct LeanObject(*mut lean_object);

// A wrapper to `lean_object` that does not hold reference counting.
// On clone, it calls `lean_inc`; on drop it does not call `lean_dec`.
// One can get a `LeanObject` from this while increasing refcnt.
#[repr(transparent)]
struct LeanObjectRef(*mut lean_object);

trait ExternalObject : Clone {
  type LeanObjIter<'a> : Iterator<Item = LeanObjectRef>;
  fn inner_obj_iter(&self) -> Self::LeanObjIter;
}

struct ExternalObjectFactory<T> {
  class: *mut lean_extern_class
  _tag: PhantomData<T>
}

#[repr(transparent)]
struct RustObject<T> (LeanObject, PhantomData<T>);

#[repr(transparent)]
struct RustObjectRef<T> (LeanObjectRef, PhantomData<T>);

impl<T> RustObject<T> {
  fn mutate<F : FnOnce(&mut T)>(mut self, factory: &ExternalObjectFactory<T>, func: F) -> Self {
    if self.0.is_exlusive() {
      func(&mut *self.get_data());
      self
    } else {
      let new_obj = factory.create((*self.get_data()).clone());
      // no need to `lean_inc` inner objects, if user stores `LeanObject`, it is handled automatically.
      func(&mut *new_obj.get_data());
      new_obj
    }
  }
}

impl<T> ExternalObjectFactory<T>
  where T : ExternalObject
{
  fn new() -> Self {
    extern "C" unsafe fn finalize(obj: *mut c_void) {
      let mut obj = Box::from_raw(obj as *mut T);
      // no need to `lean_dec`, if user stores `LeanObject`, it is handled automatically
    }
    extern "C" unsafe fn foreach(obj: *mut c_void, closure: *mut lean_object) {
      for i in (*obj).inner_obj_iter() {
        lean_inc(closure);
        lean_inc(i.0);
        lean_apply_1(closure, i.as_raw());
      }
    }
    Self {
      class: lean_register_external_class(Some(finalize), Some(foreach));
      _tag: Default::default()
    }
  }

  fn create(&self, value : T) -> RustObject {
    let data = Box::into_raw(Box::new(value)) as *mut c_void;
    RustObject(unsafe {LeanObject::from_raw(lean_alloc_external_object(self.class, data))}, Default::default())
  }
}

[Bhakti Shah]

Sebastian Ullrich said:

There is https://crates.io/crates/lean-sys (unofficial)

not sure if this is maintained anymore (doesn’t look like it) but there’s a really minor typo that makes the entire thing unusable on mac, so if you are to advertise it you may want to advertise a patched version (I made a pr to their repo a week ago, but it’s just a one word change from mac to macos)

[Bhakti Shah]

Mario Carneiro said:

Speaking of which, I have an improved version of that crate and also some beginning work on a proper type-aware lean-FFI crate for rust (unreleased)

That sounds awesome! Is the improved version also unreleased, and do you have an approximate timeline for release, if any?

[Mario Carneiro]

well I can put it on github but I'm not going to make any particular promises about it. But I did fix a handful of issues in the original

[Mario Carneiro]

@Bhakti Shah Okay, the new lean-sys is available at https://github.com/digama0/lean-sys and the (very experimental) work towards a higher level set of bindings is at https://github.com/digama0/lean-rs

[Mario Carneiro]

@Schrodinger ZHU Yifan we should collaborate, it sounds like you are implementing something similar to lean-rs. At least, the object wrapping is straightforward enough, but there is more to be done in a build.rs file to autogenerate Rust types by reading the lean expressions, i.e. a lean version of bindgen

[Bhakti Shah]

Thank you @Mario Carneiro ! Will take a look

[Mario Carneiro]

speaking of which, it would be great if someone who understands lean linking could take a look at the setup, because I'm currently getting link errors about undefined references to symbols from libstdc++

[Mario Carneiro]

I did get it to work some weeks ago, but I'm not certain I could export the arrangement off my computer and it seems to have since broken (this was pre-Lake-in-lean4-repo)

[Bhakti Shah]

probably not the same thing but I had undefined references to symbols from libstdc++ when I explicitly linked to multiple copies of libLean and libC or something along those lines (it seems just linking to “libleanshared.dylib” is enough) (thank you @Mac Malone)

[Mario Carneiro]

yes, if you are dynamic linking, but I'm trying to set things up to statically link, same as what lake build does to make an exe

[Mac Malone]

@Mario Carneiro / @Bhakti Shah If you do not wish to link leanshared, then you need to link Lean, Init, leancpp, leanrt, and stc++ along with other platform libs (take a look at leanc --print-ldflags for an example). leanshared is specifically composed of Init, Lean, leancpp, libleanrt_inital-exec, and stdc++ plus the stuff from leanc.sh

[Bhakti Shah]

Ah I tried to figure out the static linking for the same reason but for everything I added I got more undefined symbols so I eventually gave up. I’ll give it another shot after looking at that though

[Mario Carneiro]

here's the relevant build.rs code:

        println!("cargo:rustc-link-search={}/lib/lean", lean_dir.display());
        for libs in [["Lean", "leancpp"], ["Init", "leanrt"]] {
            println!("cargo:rustc-link-arg=-Wl,--start-group");
            for lib in libs {
                println!("cargo:rustc-link-lib=static={lib}");
            }
            println!("cargo:rustc-link-arg=-Wl,--end-group");
        }
        println!("cargo:rustc-link-lib=static=Lake");
        for lib in ["stdc++", "m", "dl", "gmp"] {
            println!("cargo:rustc-link-lib=dylib={lib}");
        }

AFAICT this is a reasonable translation of what I can see on the result of LEAN_CC=echo lake build:

-I /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-08-05/include
-fstack-clash-protection
-fPIC
-fvisibility=hidden
-c
-o ./build/ir/Test.o
./build/ir/Test.c
-O3
-DNDEBUG
-L /home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-08-05/lib/lean
-Wl,--start-group
-lleancpp
-lLean
-Wl,--end-group
-Wl,--start-group
-lInit
-lleanrt
-Wl,--end-group
-lLake
-Wl,-Bstatic
-lc++
-lc++abi
-Wl,-Bdynamic
-Wl,--as-needed
-lgmp
-Wl,--no-as-needed
-lm
-ldl
-pthread
-Wno-unused-command-line-argument

[Mac Malone]

@Mario Carneiro note that there are number of special LEANC_INTERNAL_LINKER_FLAGS that will not appear there (as they are not included when LEAN_CC is set).

[Mario Carneiro]

actually that doesn't include -Wl,-Bstatic, and the lake invocation includes -lc++ and -lc++abi instead of -lstdc++

[Mario Carneiro]

geez, why do you have to make things so complicated

[Mario Carneiro]

this, I guess?

-L ROOT/lib
-L ROOT/lib/glibc
ROOT/lib/glibc/libc_nonshared.a
-Wl,--as-needed
-static-libgcc
-Wl,-Bstatic
-lgmp
-lunwind
-Wl,-Bdynamic
-Wl,--no-as-needed
-fuse-ld=lld

[Mac Malone]

@Mario Carneiro I should note that I had no control over how leanc works and had a lot of fun encounter this problems myself when working on Lake :wink:

[Mario Carneiro]

oh I know, I feel your pain

[Mario Carneiro]

what even is that ROOT/lib/glibc/libc_nonshared.a argument? It's not a flag

[Mac Malone]

@Mario Carneiro some special libc code for the custom clang build Lean uses I presume

[Mario Carneiro]

I don't think lean uses a custom clang build

[Mario Carneiro]

certainly I've never needed to build clang to run stuff in the lean4 repo

[Mac Malone]

It does: https://github.com/leanprover/lean-llvm

[Mac Malone]

The release Lean comes with the custom clang, the source build does not use it.

[Mario Carneiro]

:sob: unraveling this is a nightmare

[Mac Malone]

@Mario Carneiro which is why I would suggest linking libleanshared.

[Mario Carneiro]

that's fine, but that's only one setting, the lib is supposed to support both

[Mario Carneiro]

also, lean-llvm doesn't have any code changes in it, I think it's just setting build options that ship with LLVM

[Mac Malone]

I think getting static linking working will require some help from @Sebastian Ullrich. @Henrik Böving might also be able to help given his familiarity with the compilation process (and having to tweak these things to support an LLVM backend).

[Mac Malone]

Mario Carneiro said:

also, lean-llvm doesn't have any code changes in it, I think it's just setting build options that ship with LLVM

lean-llvm is like lean4-nightly -- it hosts the bundled releases for the build generated from the CI. The scripts to build the lean4 releases that use it the are prepare-llvm-* files in the script directory of the lean4 repository.

[Mario Carneiro]

I think that's still true then, I read the LEANC_INTERNAL_LINKER_FLAGS out of that file, but there are no changes to C++ files or CLI parsing in that script

[Mario Carneiro]

actually, now I remember why I don't like the libleanshared approach: when you try to build it it works but then you can't easily run it, I want cargo run to just work and it complains about not finding libleanshared.so

[Mario Carneiro]

TBH I'm not sure how one is even supposed to ship files like that, is the user of the executable supposed to learn this linking stuff and set LD_LIBRARY_PATH correctly every time?

[Mac Malone]

@Mario Carneiro Upon further investigation, libc_nonshared is actually just part of glibc. See this StackOverflow post about it.

[Mac Malone]

Mario Carneiro said:

TBH I'm not sure how one is even supposed to ship files like that, is the user of the executable supposed to learn this linking stuff and set LD_LIBRARY_PATH correctly every time?

You are suppose to run the executables with libleanshared in the library path. On Windows, this amounts to sticking the library next to the executable and shipping them together (which is also possible on Linux and macOS).

[Mac Malone]

It is worth noting that even the release lean and lake don't run on Windows without a proper library path setup (namely one including the MSYS2 libraries).

[Mario Carneiro]

in this case we can assume the user has a lean installation provided by elan, but it's not on the library path and I don't know how to make it so

[Mac Malone]

@Mario Carneiro lake env?

[Mario Carneiro]

lake env cargo run doesn't work because there isn't a lakefile.lean :upside_down:

[Mac Malone]

@Mario Carneiro I could potentially get lake env to work without lakefile.lean (i.e., just setting up a Lean environment) if you make an issue for it.

[Mac Malone]

In the meantime, you can give lake env cargo run a try with a bare lakefile (i.e., with just a package).

[Mario Carneiro]

still no dice

[Mario Carneiro]

calling lake env target/debug/lean-rs directly also doesn't work

[Mac Malone]

What is the error?

[Mario Carneiro]

target/debug/lean-rs: error while loading shared libraries: libleanshared.so: cannot open shared object file: No such file or directory

[Mario Carneiro]

env LD_LIBRARY_PATH=(lean --print-prefix)/lib/lean target/debug/lean-rs works

[Mac Malone]

@Mario Carneiro That sounds like there may be bug in Lake. What does lake env env show?

[Mac Malone]

In particular, what is LD_LIBRARY_PATH set to?

[Mario Carneiro]

LD_LIBRARY_PATH=./build/lib

[Mario Carneiro]

LEAN_PATH=./build/lib:/home/mario/.elan/toolchains/leanprover--lean4---nightly-2023-08-05/lib/lean

[Mac Malone]

Oh, yeah, I guess Lake does not add the lean libraries to the library path only the package ones.

[Mac Malone]

That can be changed as part of lake#179.

[Bhakti Shah]

yeah I’ve had to set it manually every time. adding something to the search path in your build script is theoretically supposed to add it to the library path env variable too but that hasn’t been working for me; perhaps because of a mac specific configuration in lean-sys? From what I saw in the rust build script docs it sets DYLD_FALLOUT_LIBRARY_PATH and I had to set DYLD_LIBRARY_PATH

[Schrodinger ZHU Yifan]

libc_noshared.a is glibc‘s component to provide some special symbols like atexit_XXX. these symbols are not defined in .so

[Bhakti Shah]

@Mario Carneiro this line println!("cargo:rustc-link-lib=static=Lake"); errors out for me, and I don't see a lake search path in the build script. Perhaps you need to add a search path (although I only see an executable for lake on my device, no compiled lib, so I'm not sure what this is looking for)

[Mario Carneiro]

Lake was moved into the core distribution about a month ago, update your lean nightly to the latest

[Bhakti Shah]

ah. thank you

[Matheus C. França]

Hi everyone! :wave:
I've recently been playing with the lean4 language using ffi with ziglang.

However, there's still an issue with the MacOS CI/CD when trying to run reverse-ffi and :check: on Linux .

src: https://github.com/kassane/lean4-zig

Although zig translate-c had been used, it needed to manually handle some failures during the alignment of the lean_object, because zig doesn't recognize C bitfields and de-references errors (from: o.* to o.?.* [optional ptr]).

Is it possible to get a static link from lean4?

[Schrodinger ZHU Yifan]

I think the build script in the lean-sys repo by @Mario Carneiro can be helpful when seeking a way to do the static linking. However, I think the duplicated main symbol in libLake.a is not yet addressed yet.

[Mario Carneiro]

@Matheus C. França It looks like the issue is that you are dynamically linking with leanlibshared.dylib. This should work, but you need to pass the path to lean in the DYLD_LIBRARY_PATH when actually running the built executable. If you run the program through lake env it should set this up

[Mario Carneiro]

Does lean.h have bitfields? I don't see any bitfield declarations in lean.h

[Mario Carneiro]

I thought one of the selling points of zig was that you could just import C headers unmodified, why do you have to translate it to zig?

[Matheus C. França]

Mario Carneiro said:

Does lean.h have bitfields? I don't see any bitfield declarations in lean.h

lean_object struct: https://github.com/leanprover/lean4/blob/a7efe5b60e86b26fefd4795b46d66af369b97329/src/include/lean/lean.h#L112-L117

[Matheus C. França]

Mario Carneiro said:

I thought one of the selling points of zig was that you could just import C headers unmodified, why do you have to translate it to zig?

zig translate-c|@cImport(@cInclude("lean.h")), get some errors on atomic (c11) and C bitfields [align(u1)] (*anyopaque== void* align)

// vendor/lean.h:114:14: warning: struct demoted to opaque type - has bitfield
pub const lean_object = opaque{}; // before

// zig `opaque{}` types not have fields. another problem.

pub const lean_obj_arg = ?*lean_object;
pub const b_lean_obj_arg = ?*lean_object;
pub const u_lean_obj_arg = ?*lean_object;
pub const lean_obj_res = ?*lean_object;
pub const b_lean_obj_res = ?*lean_object;

My manual fix:

// manual fix
pub const lean_object = extern struct {  // align to C ABI != packed struct
    m_rc: c_int,
    m_cs_sz: u16,
    m_other: u8,
    m_tag: u8,
};

[Mario Carneiro]

yeah that seems fine

[Mario Carneiro]

the other issue I see is the atomics, I can send you a patch later

[Matheus C. França]

Great! I'm available for any suggestions and improvements to the project.
Since version 0.11.0 is currently in use, I want to test the new zig package manager (WiP) on it too.

[Schrodinger ZHU Yifan]

Any idea on why I am getting this error now?
image.png

[Henrik Böving]

Schrodinger ZHU Yifan said:

Any idea on why I am getting this error now?
image.png

Can't reproduce this on my local Lean. Can you give a #mwe in text form and your lean version?

[Schrodinger ZHU Yifan]

Henrik Böving said:

Schrodinger ZHU Yifan said:

Any idea on why I am getting this error now?
image.png

Can't reproduce this on my local Lean. Can you give a #mwe in text form and your lean version?

Unfortunately, I just run elan install nightly again (also deleted the toolchain file inside the project) and the problem disappeared.