Building shared library with lake

Stream: lean4

[Tomas Skrivan]

How do I properly build and use shared library with lake? I have set defaultFacet := PackageFacet.sharedLib this creates Package.so.

I then try to load Package.so using dlopen in another program, but I'm getting undefined symbol: l_Lean_instInhabitedExpr. Clearly it does not load libleanshared.so properly where this symbol is. Is Package.so linked against libleanshared.so by default or do I have to specify that?

My LD_LIBRARY_PATH points to the directory where libleanshared.so is, so it should not be a problem that the program can't find it.

[Sebastian Ullrich]

If ldd Package.so doesn't list libleanshared.so, you can try adding -lleanshared as a linker flag.

[Tomas Skrivan]

Yes, adding

moreLinkArgs := #["-L~/.elan/toolchains/leanprover--lean4---nightly-2022-01-12/lib/lean", "-lleanshared"],

solved the problem.

[Tomas Skrivan]

Now I'm facing different error:

uncaught exception: invalid environment extension, 'ext' has already been used

[Tomas Skrivan]

The problem seems to be that I'm loading and executing the shared library in a loop.

On the first run the library gets loaded and executed correctly. However, on the second load, running:

initialize_Package(lean_io_mk_world());

fails. I'm probably not correctly cleaning up after the first run. How do I do that?

[Sebastian Ullrich]

Module initializers should be idempotent. But... why are you loading the same library in a loop?

[Tomas Skrivan]

I want to use Lean as a scripting language in a different program. I should reload the library only when to code changes, but for now I reload it on every execution.

[Tomas Skrivan]

Also I'm confused about lean_initialize() and lean_initialize_runtime_module() the first one does not work, the second one does.

[Sebastian Ullrich]

It sounds like you didn't unload libleanshared.so

[Tomas Skrivan]

Ohh how do I do that?

[Tomas Skrivan]

I'm not loading it manually.

[Tomas Skrivan]

I should be calling dlclose ...

[Tomas Skrivan]

The problem might be that I'm writing a plugin Plugin.so to one program that loads Package.so. Both Plugin.so and Package.so needs libleanshared.so as the plugin calls initalization of lean, lean_io_mk_world, etc.

Thus when I unload Package.so it does not unload libleanshared.so as it is still needed by Plugin.so.

[Tomas Skrivan]

Yes it was indeed the problem. Unfortunately, to create Plugin.so I can't link against lean static libraries because they are not compiled with -fPIC, so when I want to use any function from lean.h I have to dynamically load it.

[Tomas Skrivan]

Dynamically loaded lean_dec_ref causes crash, so I can't clean up any lean_object and my program leaks memory :/

[Sebastian Ullrich]

Tomas Skrivan said:

The problem might be that I'm writing a plugin Plugin.so to one program that loads Package.so. Both Plugin.so and Package.so needs libleanshared.so as the plugin calls initalization of lean, lean_io_mk_world, etc.

Thus when I unload Package.so it does not unload libleanshared.so as it is still needed by Plugin.so.

Then I think you're stuck. There is no way to undo the mutable changes loading Package.so did to the data in libleanshared.so if you cannot unload them both. You should never link the same library both dynamically and statically.

[Sebastian Ullrich]

But I still don't know where the error actually stems from. Do you initialize an environment extension in Package.so?

[Tomas Skrivan]

What does "initialize environment extension" mean? Is it the call initialize_Package?

[Sebastian Ullrich]

No, it would need to be a call to register*EnvExtension. I hope we don't actually have one named ext (and if we did, it shouldn't be loaded twice if it's part of libleanshared.so).

[Gabriel Ebner]

Note that mathlib4 has an ext extension.

[Sebastian Ullrich]

Ah yes, a different meaning of "ext" :) . Disabling builtin_initialize via https://github.com/leanprover/lean4/pull/959 might be of interest then. I guess it's not a builtin then.

[Sebastian Ullrich]

Then a better answer is that the attribute registration should only happen in a "compile time" phase while you are only interested in running the plugin in a "run time" phase. Some day I hope Lean will be able to express that...

[Tomas Skrivan]

I have made a mock up of my situation, unfortunately I was unable to recreate the invalid environment extension error. But I still have problems with memory leaks:

https://github.com/lecopivo/leanPluginTest

Build and run instructions are in the readme.

This example has a main application main that loads a plugin plugin and the plugin loads package made with Lean. The main function of the package is called over and over in an infinite loop.

There are two versions, main and main2

1. main is where plugin does not link libleanshared to avoid the problems I had. However, I have problems calling lean_dec_ref to clean up memory. Running ./main causes segmentation fault after a moment.
2. main2 is where plugin2 links libleanshared. This should be the case where I had the problem with environment extension. However, I'm unable to reproduce it here, as Gabriel pointed out it might be a problem with Mathlib(I will test that). This version does not cause segmentation fault but leaks memory.

[Tomas Skrivan]

And yes I'm using mathlib4 in my real code. The environment extension error might be connected to that.

[Tomas Skrivan]

A simple inclusion of mathlib4, https://github.com/lecopivo/leanPluginTest/tree/mathlib . I'm getting ../lib/Package.so: undefined symbol: initialize_Mathlib_Data_UInt not sure what is going wrong. Definitely not reproducing the old error.

[Sebastian Ullrich]

Tomas Skrivan said:

A simple inclusion of mathlib4, https://github.com/lecopivo/leanPluginTest/tree/mathlib . I'm getting ../lib/Package.so: undefined symbol: initialize_Mathlib_Data_UInt not sure what is going wrong. Definitely not reproducing the old error.

That sounds like a bug in Lake

[Sebastian Ullrich]

Tomas Skrivan said:

This version does not cause segmentation fault but leaks memory.

Hmm yes, I probably should have thought of this sooner. Lean shared libraries are simply not made to ever be unloaded. Perhaps they could be, but right now they aren't.

[Tomas Skrivan]

I would really love to use Lean as a scripting language in an another program. I can probably load each new version of a script as a different library, not ideal but should work. Maybe I can use Lean's interpreter, but then I'm not sure how could I wrap the program's C++ API into Lean functions.

[Tomas Skrivan]

Ok I'm not sure what is going on but now I can reproduce the invalid environment extension error

git clone --branch mathlib https://github.com/lecopivo/leanPluginTest.git
cd leanPluginTest
lake build
export LD_LIBRARY_PATH=~/.elan/toolchains/leanprover--lean4---nightly/lib/lean
cd build; mkdir debug; cd debug
cmake ../..
make -j
./main2

Running ./main works fine until it seg faults.

[Tomas Skrivan]

And when you remove import Mathlib from Package.lean then main2 works 'fine'(well it leaks memory)

[Sebastian Ullrich]

Yes, if you load mathlib twice without unloading libleanshared, that is expected

[Tomas Skrivan]

How important is it to run lean_io_mark_end_initialization, lean_init_task_manager or lean_finalize_task_manager I have no clue what any one of these is doing.

[Tomas Skrivan]

As I have to load every function from lean.h dynamically, the only way to get lean_dec_ref was to dynamically load lean_dec_ref_cold then then defined my lean_dec_ref with:

    auto lean_dec_ref = [&](lean_object * o) {
      if (LEAN_LIKELY(o->m_rc > 1)) {
        o->m_rc--;
      } else if (o->m_rc != 0) {
        lean_dec_ref_cold(o);
      }
    };

[Tomas Skrivan]

I have updated the repository with working lean_dec_ref, this way I have more or less reproduced main function that gets generated by lean. However running main still segfaults after a while, I have no clue what to do now to fix that.

[Tomas Skrivan]

And it segfaults after 1024 iterations what a coincidence :D