Load plugin during build?

Stream: lean4

[Thomas Murrills]

I'm wondering if it is possible to load a plugin during lake build, so that e.g. a linter introduced by the plugin can run on all files during build, or so that the environment can record some information. I'd like to avoid adding any imports, while still injecting something during initialization for every file.

One approach is to simply recreate a frontend, call loadPlugin under withImporting, and run it on all files; but this can't easily handle "dependent" modifications, where what we want to record in the environment might depend on the environment (and thus on what we've recorded earlier for a given module's dependencies). It would be nice to take advantage of Lake's existing infrastructure for that.

I suspect it might be possible to make a lake target or facet that does this, but we need to intervene before building, and somehow pass a --plugin argument (or the internal equivalent) to the lean process. I'm not sure how to pass this along.

Context: making it easy to install library-scale modification tools. :)

[Mac Malone]

lean_lib has a plugins option which is an array of shared library targets Lake will cause Lean to load as plugins.

[Mac Malone]

One can, for example, pass the lib:shared facet of a lean_lib lib target as such a plugin.

[Thomas Murrills]

Oh, wow! I am so glad it's that easy. :D

[Mac Malone]

One future desire of mine is adding a lean_plugin target type that is more specifically focused on producing a plugin (instead of using the shared facet of a lean_lib, which is only incidentally a plugin).

[Thomas Murrills]

Follow-up: I know there's some comment somewhere about how we ought not to load the same symbol twice when using plugins. Does this mean not importing the library "normally" within the lean_lib using it as a plugin? I'm imagining a case where I want to use tools provided by the library-used-as-a-plugin in some meta code downstream (e.g. recordThisInPluginExt foo) but also want to take advantage of the plugin aspect. Would I need to take special care there?

[Kim Morrison]

@Thomas Murrills, @Mac Malone, I have no idea how to use this stuff, I don't even know what a lake plugin is. Could either of you produce an minimal example of injecting a linter without touching the source files?

[Thomas Murrills]

The primary example I'm working off of so far is the pkg/user_plugin/ test in lean core. :grinning_face_with_smiling_eyes: As far as I know a plugin is essentially a shared/dynamic(?) library that gets to initialize things at the start of the file without ever being imported by that file. (As such it's injected by e.g. lean --plugin=path/to/plugin foo, or by the plugins argument discussed here.)

In the tests at user_plugin, the builtin_initializes can be replaced with e.g. builtin_initialize addLinter fooLinter.

[Thomas Murrills]

There's a chance I'm getting this wrong, so take it with a grain of salt, as I'm still actively figuring out what's going on here myself.

[Mac Malone]

Thomas Murrills said:

Follow-up: I know there's some comment somewhere about how we ought not to load the same symbol twice when using plugins.

There are some comments in the code about this. However, I ended up investigating this more thoroughly ( a while back) and have come to the conclusion that this is not actually an issue on modern platforms. I am not quite sure why I (and others) previously thought this would be a problem (and thus cannot really disprove it), but it does not appear to be anymore.

[Thomas Murrills]

Mac Malone said:

One can, for example, pass the lib:shared facet of a lean_lib lib target as such a plugin.

Trying this out; what actually is the correct syntax? For example, if I have

lean_lib Foo where
  defaultFacets := #[LeanLib.sharedFacet]

lean_lib Bar where
  plugins := #[Foo]

it typechecks, but doesn't work.

I noticed some syntax of the form `@pkg/tgt:facet, which seems promising (e.g. `@mypackage/Foo:shared)! Is that the expected way to interact with things here? (I'm wondering if there's a more "typesafe" way to do this, because there doesn't seem to be any compile-time resolution of `@ syntax.)

[Thomas Murrills]

I'm also hitting an error of the form

error loading library, dlopen(<path-to-.dylib>, 0x0009): symbol not found in flat namespace '_l_Lean_Name_transitivelyUsedConstants___boxed'

I'm not really sure how to start debugging that... :sweat_smile: Would certainly appreciate any hints/thoughts! :)

[Thomas Murrills]

Note: I'm experimenting by modifying Mathlib to use some plugins by adding a shared lean_lib to Mathlib's lakefile then loading it as a plugin for mathlib. transitivelyUsedConstants is used in some files I copied to the shared lib, and it seems to come from the ImportGraph dependency, if that's a clue...

[Thomas Murrills]

(This error appears when attempting to build a file with only core imports in Mathlib; the shared library itself builds successfully.)

[Thomas Murrills]

Hmm, I'm struggling to get anything working when the plugin/shared library has any imports, even if they're not used. Here's a zip file of an example package for which lake build fails:
OutletPkg.zip
However, go into LocalPluginPkg.lean and comment out import Batteries, and lake build works (and demonstrates the plugins working). Otherwise, on windows, I get the error

OutletPkg/Basic.lean:1:0: error loading library c:\Users\Notoc\Coding\Lean\PluginTest\OutletPkg\.lake\build\lib\LocalPluginPkg.dll: 126

(I get a similar error on mac.)

Are plugins simply disallowed from having imports, or am I doing something wrong? Or is this a bug?

(I've tried things like adding needs = ["batteries/Batteries:shared"] to the plugin's lean_lib, but to no avail.)

[Anne Baanen]

I managed to make it build successfully by changing the lakefile to:

 name = "OutletPkg"
 version = "0.1.0"
 defaultTargets = ["OutletPkg"]

 [[require]]
 name = "batteries"
 git = "https://github.com/leanprover-community/batteries"
 rev = "main"

 [[lean_lib]]
 name = "LocalPluginPkg"
 defaultFacets = ["shared"]
 leanOptions = { experimental.module = true }

 [[lean_lib]]
 name = "OutletPkg"
 needs = ["OutletPkg/LocalPluginPkg"]
 plugins = ["OutletPkg/LocalPluginPkg:shared"]
+dynlibs = ["batteries/Batteries:shared"]
 leanOptions = { experimental.module = true }

[Anne Baanen]

Aha! What if we do a static link instead:

 name = "OutletPkg"
 version = "0.1.0"
 defaultTargets = ["OutletPkg"]

 [[require]]
 name = "batteries"
 git = "https://github.com/leanprover-community/batteries"
 rev = "main"

 [[lean_lib]]
 name = "LocalPluginPkg"
 defaultFacets = ["shared"]
 leanOptions = { experimental.module = true }
+moreLinkObjs = ["batteries/Batteries:static"]

 [[lean_lib]]
 name = "OutletPkg"
 needs = ["OutletPkg/LocalPluginPkg"]
 plugins = ["OutletPkg/LocalPluginPkg:shared"]
 leanOptions = { experimental.module = true }

[Mac Malone]

The needs should be unnecessary. The main issue here is was that Lake does not, by default, link a shared library to its dependent shared libraries. Thus, users need to make those dependents available to Lean manually so that the plugin can load successfully. Anne presents a couple of ways to do this (thanks!), and the existence of multiple solutions is partly why Lake does not currently do this automatically. However, I do hope to provide a cleaner solution in the future (e.g., lean_plugin with some customization options) when I have more time to devote to this aspect of Lake.

[Thomas Murrills]

Nice! I do think it would be great if Lake linked everything automatically here even just when building shared facets, before the lean_plugin solution, though; it took some time to figure out these solutions on a call together, and it doesn’t seem like the kind of thing that should be done manually anyway (plugin aside), right?

I can imagine that the sensible default for most users here is statically linking the dependency libraries when building shared libraries; otherwise, every time you add a dependency, you need to update the lakefile, which makes maintaining shared facets harder. Perhaps there could be a way to opt out of this behavior for users who don’t want static linking instead of having to opt in? Otherwise, the default state for using shared facets is a non-working state. :sweat_smile:

[Mac Malone]

@Thomas Murrills The idea with a shared facet is that shared library of lean_lib works like the shared library of normal C lib. In C space, it is normal to link a library and its dependencies separately rather than bundled them all together (e.g., libraries like Lean's gmp, pthread, m are common depedencies of C code, but are not usually statically linked to it -- sometimes, like with gmp, due to licensing restrictions).

[Thomas Murrills]

Hmm, okay—but doesn't this introduce a high maintainability cost for plugins? I understand the analogy, but I'm not sure Lean users should be thought of as C users, after all—most will not be familiar with that ecosystem. :) For them, this does mean that the default state is non-working, when, to my mind, this could be handled automatically—and would be the correct thing in most cases, right? Otherwise, to load a plugin with dependencies, you need to look at documentation for that module's dependencies and load them as dynlibs, and the error messages are quite obscure. :sweat_smile:

[Mac Malone]

@Thomas Murrills For plugins, yes. The shared facet was not originally designed with plugins in mind (and that is still not really its primary purpose). That is why I want to introduce a proper lean_plugin that more cleanly targets that use case.

[Mac Malone]

To elaborate a bit on shared's purpose. It was initially intended for use with Lean FFI / Reverse FFI with languages like C and Rust (hence the similar approach to code organization). It is also used internally by Lake in precompileModules setups (where Lake knows its dependencies and can load them alongside).

[Thomas Murrills]

Okay, I see! Thanks for elaborating—that was going to be my next question! :)

It's rather low-prio, then (especially if lean_plugin will exist), but it would be nice if one day the error messages were friendlier; maybe e.g. when building the shared facet lake demands that a flag is explicitly set in the config which specifies whether you are going to link it dynamically or statically, and the lack of this flag becomes a chance to explain the situation to the user in the resulting error message. But, of course, I know you're busy, and there are likely bigger fish to fry... :)

[Thomas Murrills]

One question I have about a future lean_plugin, though—sometimes we will want to load the plugin library via import downstream to extend it. What are the tradeoffs with having e.g. a LeanLib.pluginFacet facet for a lean_lib? (Maybe plugins demand different config options?) Would an example usage be to have e.g. both lean_lib and lean_plugin, or would lean_plugin imply lean_lib? (I understand if these questions and tradeoffs are still being figured out, of course... :grinning_face_with_smiling_eyes:)