mwe: plugin?

Stream: lean4

[Daniel Selsam]

does anybody have a simple working example of two different projects in different directories in the same repository, one importing the other as a plugin only?

[Christian Pehle]

I've tried to create one based on the nice work by @Mac on papyrus here. Unfortunately right now I still get could not find native implementation of external declaration 'Example.funA' (symbols 'l_Example_funA___boxed' or 'l_Example_funA'), even though the plugin library has this symbol nm -D -C plugin/build/ExamplePlugin.dll | grep l_Example_funA___boxed.

[Christian Pehle]

Any pointers how to fix this minimal example would be appreciated :smile: .

[Mac]

@Christian Pehle are you building by just running make test? Because that works on my machine.

[Mac]

Also are you on a Windows or Unix box?

[Sebastian Ullrich]

Hmm, we may be missing RTLD_GLOBAL in load_plugin

[Sebastian Ullrich]

       RTLD_DEFAULT
              Find  the  first  occurrence  of the desired symbol using the default shared object search order.
              The search will include global symbols in the executable and its dependencies, as well as symbols
              in shared objects that were dynamically loaded with the RTLD_GLOBAL flag.

[Christian Pehle]

I am building on a Unix box (some Ubuntu).

[Mac]

Ah, @Christian Pehle , then shouldn't you build a .so rather than a .dll?

[Christian Pehle]

Sebastian Ullrich said:

Hmm, we may be missing RTLD_GLOBAL in load_plugin

Yes, that is also my suspicion, because at the place the symbol is looked up the plugin is not explicitly referenced.

[Christian Pehle]

Mac said:

Ah, Christian Pehle , then shouldn't you build a .so rather than a .dll?

I've added a c++ only test to check the postfix doesn't matter (my dynamic linker knowledge is limited :)).

[Mac]

@Christian Pehle as is mine :laughing:

[Mac]

For example, I only hardcoded building a .dll in the original plugin Makefile because I don't know how to determine within it what the preferred extension of the platform should be.

[Mac]

(and not providing an extension caused all sorts of errors)

[Sebastian Ullrich]

Sebastian Ullrich said:

Hmm, we may be missing RTLD_GLOBAL in load_plugin

It depends of course on what the --plugin flag ultimately is supposed to be used for; for something like linters, the current implementation should be fine and perhaps even preferable. For loading native code, have you tried simply putting it in LD_PRELOAD?

[Christian Pehle]

using LD_PRELOAD works :smile: (didn't test that so thanks)

[Christian Pehle]

I think the behaviour should be consistent across platforms at least.

[Christian Pehle]

in a slightly more complicated plugin I get "undefined symbol: l_instInhabitedUInt64", which can be solved by also preloading libleanshared.so

[Christian Pehle]

Mac said:

For example, I only hardcoded building a .dll in the original plugin Makefile because I don't know how to determine within it what the preferred extension of the platform should be.

Apparently the linux linker does not care about the extension... :smile:

[Mac]

@Christian Pehle I just posted an issue to lean4-plugin-example (#1) noting that using leanWithPlugin.sh as the Lean executable does not work on Windows.

I also recently got a cross-platform (Ubuntu, MacOS, and Windows) GitHub Actions workflow working to build and test Papyrus. I could PR a similar one to the repo (or you could copy from mine) if you want.

[Mac]

Regarding #1, @Gabriel Ebner , when you get a chance, could you publish a new version of vscode-lean4 to the marketplace? The server arguments commit is really key for Lean packages using plugins.

[Christian Pehle]

Mac said:

Christian Pehle I just posted an issue to lean4-plugin-example (#1) noting that using leanWithPlugin.sh as the Lean executable does not work on Windows.

I also recently got a cross-platform (Ubuntu, MacOS, and Windows) GitHub Actions workflow working to build and test Papyrus. I could PR a similar one to the repo (or you could copy from mine) if you want.

I suspected that just prepending LD_PRELOAD would lead trouble on Windows, but reading the issue it actually is a different problem. A pull request for the Github actions workflow would be very welcome, all credit for this example should really go to you anyways.

[Ramon Fernandez Mir]

I've tried to replicate lean4-plugin-example but VSCode seems to be ignoring the executablePath option. I suspect it has something to do with this issue: https://github.com/leanprover/vscode-lean4/issues/79 Any idea how I can force VSCode to use leanWithPlugin.sh??