how to use Frontend.processCommand when command uses FFI?

Stream: lean4

[David Renshaw]

I want to use tryAtEachStep to run LeanCopilot's search_proof tactic at every tactic step in a Lean file.

When I attempt to do so, I get this error:

.libc++abi: terminating due to uncaught exception of type lean::exception: Could not find native implementation of external declaration 'LeanCopilot.FFI.isGeneratorInitialized' (symbols 'l_LeanCopilot_FFI_isGeneratorInitialized___boxed' or 'l_LeanCopilot_FFI_isGeneratorInitialized').
For declarations from `Init` or `Lean`, you need to set `supportInterpreter := true` in the relevant `lean_exe` statement in your `lakefile.lean`.

I believe that I'm already setting supportInterpreted := true in every place that I can.

tryAtEachStep works by calling Frontend.processCommand on each command in the input Lean file, to re-elaborate everything. How can i make that work in the presence of FFI?

[David Renshaw]

My code is at compfiles/lean-copilot.

$ lake exe cache get
$ lake exe LeanCopilot/download
$ lake build
$ lake exe tryAtEachStep --imports LeanCopilot search_proof Compfiles/Imo1992P2.lean

info: [1/4] Building tryAtEachStep
info: [3/4] Compiling tryAtEachStep
info: [4/4] Linking tryAtEachStep
.libc++abi: terminating due to uncaught exception of type lean::exception: Could not find native implementation of external declaration 'LeanCopilot.FFI.isGeneratorInitialized' (symbols 'l_LeanCopilot_FFI_isGeneratorInitialized___boxed' or 'l_LeanCopilot_FFI_isGeneratorInitialized').
For declarations from `Init` or `Lean`, you need to set `supportInterpreter := true` in the relevant `lean_exe` statement in your `lakefile.lean`.

[Mario Carneiro]

I assume you tested that it works in the editor?

[David Renshaw]

Yes, it works interactively in emacs.

[David Renshaw]

If I manually type in search_proof, it successfully executes the tactic.

[Mario Carneiro]

I notice that you have some funny link args

[Mario Carneiro]

you may need to pass those link args to the executable (i.e. tryAtEachStep)

[David Renshaw]

linker args

[David Renshaw]

^ this are what LeanCopilot's README instructs me to add

[Mario Carneiro]

right, that makes lean able to find the necessary function

[Mario Carneiro]

but now you need to make tryAtEachStep also find the function

[Mario Carneiro]

so you need to link tryAtEachStep with those arguments

[Mario Carneiro]

(I'm aware this is a layering violation but try it anyway to see if this is the issue)

[David Renshaw]

I don't know how to pass in such information

[David Renshaw]

setting LD_LIBRARY_PATH does not seem to help

[Mario Carneiro]

try adding moreLinkArgs to the lakefile of tryAtEachStep

[David Renshaw]

ah, okay. Yeah, layering violation indeed...

[David Renshaw]

I vendored tryEachStepLean into compfiles/scripts and then added this to the compfiles lakefile.lean:

@[default_target]
lean_exe tryAtEachStepVendored where
  root := `scripts.tryAtEachStep
  supportInterpreter := true
  moreLinkArgs := #[
    "-L./.lake/packages/LeanCopilot/.lake/build/lib",
    "-lctranslate2"
  ]

[David Renshaw]

... and got the same error when running lake exe tryAtEachStepVendored ...

[David Renshaw]

hm... actually it seems that the error is not coming from Frontend.processCommand

[David Renshaw]

it's coming from here: https://github.com/dwrensha/tryAtEachStep/blob/6d1dcdf8c28c005fa3e1795cbac773870109d80d/tryAtEachStep.lean#L75-L78

[David Renshaw]

where I try to run the search_proof tactic, using the snapshotted MetaM state that I extracted from Frontend.processCommand.

[Sebastian Ullrich]

Does ldd list the shared lib in question on your new executable?

[Sebastian Ullrich]

LD_PRELOAD not LD_LIBRARY_PATH is the correct env var to smuggle a solib into an executable that does not require the lib btw

[David Renshaw]

$ ldd .lake/build/bin/tryAtEachStepVendored
    linux-vdso.so.1 (0x00007ffd59f7c000)
    libctranslate2.so.4 => not found
    libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007ee817319000)
    libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x00007ee81b37d000)
    libpthread.so.0 => /lib/x86_64-linux-gnu/libpthread.so.0 (0x00007ee81b378000)
    libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007ee817000000)
    librt.so.1 => /lib/x86_64-linux-gnu/librt.so.1 (0x00007ee81b371000)
    /lib64/ld-linux-x86-64.so.2 (0x00007ee81b3a0000)

[David Renshaw]

David Renshaw said:

hm... actually it seems that the error is not coming from Frontend.processCommand

Indeed, when I add search_proof to a proof in the Lean file and then try tryAtEachStep exact?, it succeeds. So Frontend.processCommand is able to run the search_proof tactic. The problem is that my later injected tactic execution is not able to run the search_proof tactic.

[David Renshaw]

So now I'm trying to figure out where Frontend.processCommand is getting its linker state, and how I can make sure to pass that on to my own TermElabM...

[Mario Carneiro]

well "linker state" isn't really a thing, the linking state (such as it is) is global and is not passed around

[David Renshaw]

Oops -- I was using an invocation of search_proof that succeeded before it needed to run FFI code.
So, correction : Frontend.processCommand does fail, and with the same error "Could not find native implementation of external declaration"

[David Renshaw]

So my question is: why does the LSP FileWorker process succeed at linking (it successfully executes the search_proof tactic) while my tryAtEachStep program fails?

[Eric Wieser]

The fileworker isn't linking, I don't think? It's perhaps using the lean -dynlib flag to load the search_proof library into the lean runtime, but it's not linking anything against it

[David Renshaw]

Aha! This seems to be working (with my vendored tryAtEachStep):

$ LD_LIBRARY_PATH=./.lake/packages/std/.lake/build/lib:./.lake/packages/aesop/.lake/build/lib:./.lake/packages/mathlib/.lake/build/lib:./.lake/packages/LeanCopilot/.lake/build/lib:./.lake/build/lib:/home/dwrensha/.elan/toolchains/leanprover--lean4---v4.7.0/lib/lean:/home/dwrensha/.elan/toolchains/leanprover--lean4---v4.7.0/lib  LD_PRELOAD=.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Tactics-1.so  lake exe tryAtEachStepVendored --imports LeanCopilot search_proof Compfiles/Imo1992P2.lean

[David Renshaw]

That LD_LIBRARY_PATH was stolen from a fileworker.

[David Renshaw]

And then I just started trying random things with LD_PRELOAD.

[David Renshaw]

Here's where FileWorker loads dynlibs: https://github.com/leanprover/lean4/blob/75e68e7565708361e117c5f56b66fdbe013de667/src/Lean/Server/FileWorker/SetupFile.lean#L125

[David Renshaw]

lake setup-file seems relevant...