Compile package as plugin

Stream: lean4

[Jannis Limperg]

Does anyone know how to compile a Lean 4 package into a .so that Lean can load with lean --plugin? There are some previous conversations about this on Zulip and there's the test case in the Lean repo, but I'm still unable to figure this out. (My ignorance of C may have something to do with that.)

[Wojciech Nawrocki]

It seems leanmake does not support plugins. I guess we'll have this in Lake. You could try this Makefile in the meantime

CFLAGS = -O3 -fPIC

%.olean : %.lean
        LEAN_PATH=${HOME}/mathlib4/build/ lean -o $@ $<

%.c : %.lean
        LEAN_PATH=${HOME}/mathlib4/build/ lean -c $@ $<

%.o : %.c
        leanc -c $< -o $@ $(CFLAGS)

%.so : %.o
        leanc -shared -x none $< -L${HOME}/mathlib4/build/lib/ -lMathlib -o $@ $(CFLAGS)

And then make MyPlugin.so.

[Wojciech Nawrocki]

(Btw, that links against Mathlib. If you don't need Mathlib4, remove the LEAN_PATH=..mathlib and -L..mathlib.. and -lMathlib.

[Mac]

@Wojciech Nawrocki Do you know if this works on Windows yet? if I recall correctly, plugins with Lean code need to link to the Lean binary, and this does not work properly on the Windows MSYS2 build of Lean.

[Wojciech Nawrocki]

I would not expect that to work on MSYS2 Windows, no :/ I use WSL.

[Sebastian Ullrich]

It's kind of weird that even that works given that the stdlib is not yet compiled with fPIC

[Sebastian Ullrich]

If anyone wants to debug https://github.com/leanprover/lean4/pull/555 on Windows, please do

[Jannis Limperg]

@Wojciech Nawrocki Your recipe works (thanks!), but apparently not with plugins that use initialize. Full MWE:

Plugin.lean:

import Lean

open Lean
open Lean.Elab.Tactic

initialize opt : Lean.Option Bool <-
  Option.register `opt { defValue := true, group := "", descr := "" }

syntax (name := aesop) &"aesop" : tactic

@[tactic aesop]
def evalAesop : Tactic := λ _ => do evalTactic (<- `(tactic| assumption))

Client.lean:

import Plugin

example (h : α) : α := by aesop

Makefile:

CFLAGS = -O3 -fPIC

Client.olean : Client.lean Plugin.so Plugin.olean
    env LEAN_PATH="." lean --plugin=Plugin.so -o Client.olean Client.lean

%.olean : %.lean
    lean -o $@ $<

%.c : %.lean
    lean -c $@ $<

%.o : %.c
    leanc -c $< -o $@ $(CFLAGS)

%.so : %.o
    leanc -shared -x none $< -o $@ $(CFLAGS)

.PHONY: clean
clean:
    rm -rf Plugin.olean Plugin.so Plugin.c Plugin.so Client.olean

make Client.olean fails with

Client.lean:1:0: error: invalid option declaration 'opt', option already exists

When I remove the initialize block from Plugin.lean, the same command succeeds.

[Wojciech Nawrocki]

Note that the current version (commit a230fe2) runs initialize blocks on import, so if you just want the custom option you don't need a plugin. The error you're seeing is because Lean tries to run your initialize twice -- once from the --plugin and once because you import Plugin.

[Mario Carneiro]

How does the plugin option impact the environment? Is it as though you had import Plugin in every file?

[Jannis Limperg]

Wojciech Nawrocki said:

Note that the current version (commit a230fe2) runs initialize blocks on import, so if you just want the custom option you don't need a plugin. The error you're seeing is because Lean tries to run your initialize twice -- once from the --plugin and once because you import Plugin.

Yeah, everything works fine without the --plugin. I'm writing a search tactic that would benefit from being compiled. But this is not urgent, so I'll just wait until initialize works in plugins. I could also split the library into an initialize part and a compiled part; that might be okay.

[Wojciech Nawrocki]

Mario Carneiro said:

How does the plugin option impact the environment? Is it as though you had import Plugin in every file?

AFAIK it shouldn't impact the environment at all. Using --plugin will run the initialize blocks and that's it. So you can register custom linters, options, and so on. But for the defs, you need a manual import.

[Mario Carneiro]

Doesn't that mean that it is problematic to import something that is also --plugin'd? Since you will have to somehow dodge the initialize but do everything else

[Wojciech Nawrocki]

Yeah, I suppose it does. You could have a do-once mechanism with an IO.Ref Bool. This part of the system still seems a bit in flux.

[Wojciech Nawrocki]

Or maybe Lean could auto-insert those. The semantics of initialize are not very clear (to me, at least).

[Sebastian Ullrich]

Yes, it's not expected to also import a plugin, though we should probably make sure it still works since you might not be able to avoid it in case of some shared module. I'm not sure initialize being run in a plugin is even intended, usually builtin* means "run when native code is loaded, register into some global IO.Ref" and non-builtin means "run when imported, register into the environment".

[Mac]

To clarify @Sebastian Ullrich's point @Jannis Limperg, you should use builtin_initialize if you are planning to use the module via a --plugin and initialize only if you are planning to use the module via import.