Plugin Support

[Kha]

This PR adds a --plugin= option to lean that loads the specified library and initializes its Default module, which is assumed to exist and to cause side effects like registering linters. A super-simple linter framework and test linter are provided that should be extended vigorously in the new frontend.

[leodemoura]

Assuming this is WIP.

[Kha]

Yes, I will need a few more rounds of CI to get it working on all platforms

[Kha]

Goodness gracious, I can't believe it's finally working on all three platforms. It took me quite a while to figure out how a plugin should exactly be linked, so here it is:

A plugin is a shared library that uses symbols from the lean binary to influence its behavior, but is not actually linked against it (yes, you can in fact link against executables, but the point holds just as well if we were to link against e.g. leanshared instead). This is important because if you actually link against lean, the plugin will try to look up the executable file in the search paths when loaded, even though the lean image is already loaded! This will usually fail unless we point LD_LIBRARY_PATH at the Lean binary dir; if instead we simply don't link against lean, it just works.

So how do you use symbols of an object without linking against it?

• On Linux, this is actually allowed by default when linking shared libraries.
• On macOS, you have to encourage the linker a bit using -undefined dynamic_lookup (which leanc now does for you).
• On Windows, you have to at least create and link against an import library, which is a static library that contains the desired symbols but no definitions. It can be created automatically by mingw ld using --out-implib. leanc will now link objects against it automatically when given -shared.

[leodemoura]

but is not actually linked against it (yes, you can in fact link against executables, but the point holds just as well if we were to link against e.g. leanshared instead).

This is awesome. I didn't know this was possible in all major platforms.
I thought we would have to use leanshared to build the lean executable. That is, the executable would be just the main function + loader. This is much better.

[leodemoura]

It seems every plugin must define initialize_Default. Is this a problem?
https://stackoverflow.com/questions/6538501/linking-two-shared-libraries-with-some-of-the-same-symbols
I am assuming it should work since you are using dlsym.

[Kha]

Yes, objects loaded by dlsym are independent by default.

      RTLD_LOCAL
              This is the converse of RTLD_GLOBAL, and the default if neither flag is specified.  Symbols  defined  in  this
              shared object are not made available to resolve references in subsequently loaded shared objects.

As far as I could find out, this is actually the only behavior supported on Windows, so we should be fine.

Btw, note that if we ever do prefix import paths with the package name as we once discussed, this would be initialize_SnakeLinter_Default anyway (which --plugin should derive from the library filename).

[ratmice]

Should this try calling dlopen with RTLD_NOLOAD (if available) first, to check if the shared library is actually loaded already,
to avoid opening the same library twice?

[Kha]

If the same shared object is opened again with dlopen(), the same object handle is returned. And Lean initializers are idempotent.

[ratmice]

Thanks I had missed the section describing that in the docs, needed to read further.

[leodemoura]

We should move this function to a different folder since we need it to implement the import plugin <plugin-name> command

[leodemoura]

merged.