search

alexf91 / lean4-ctypes

FFI for Lean 4
Apache License 2.0
3 stars 0 forks source link

Possible bug in garbage collection with `dlclose()` #8

Closed alexf91 closed 8 months ago

alexf91 commented 8 months ago

Objects might get garbage collected by Lean when they go out of scope but are still required to be loaded. This is mainly a problem for Library objects because dlclose() is called and the pointer to the function might become invalid.

Pointers created with Library.symbol already take care of this by adding a dependency on the Library to the pointer, but if the pointer is created manually (e.g. with pointer arithmetic), then there is no dependency. In this case we don't have a dependency chain from the Function to the Library.

A simple fix could be to avoid dlclose(), either automatically or with an additional flag for Library.mk. Python's ctypes doesn't call dlclose() automatically.

alexf91 commented 8 months ago

The library is designed to do unsafe things, so restricting the user doesn't make much sense. dlclose() has to be called manually.