Using result from foreign function in a tactic

Stream: lean4

[Ramon Fernandez Mir]

I've been playing around with the extern command and I was wondering how to use a foreign function in a tactic. Say that I have a C++ function that returns 5, and I want a tactic that tries to close the goal with 5. I've followed https://github.com/leanprover/lean4/tree/master/tests/compiler/foreign to write the Makefile and the C++ code. Here's what I have so far:

/* MyFunction.cpp */

#include <lean/object.h>
#include <lean/io.h>

extern "C" lean_object * my_function(lean_object /* w */) {
  return lean_io_result_mk_ok(lean_int_to_int(5));
}

-- MyFunction.lean

import Lean.Elab.Tactic.Basic

@[extern "my_function"]
constant myFunction : IO Int

open Lean Meta Elab Tactic

syntax (name := Lean.Parser.Tactic.five) "five" : tactic

@[tactic five] def five : Tactic := fun stx => do
  let x ← myFunction
  assignExprMVar (← getMainGoal).1 (toExpr x.toNat)
  let (mvarId :: mvarIds') ← getGoals | throwError "Error"
  modify fun s => { s with goals := mvarIds' }

--def myFive : Nat := by five
--#eval myFive

def main : IO Unit := do
  let x ← myFunction
  IO.println x

If I leanmake it as it is, it works fine and prints 5 as expected, however as soon as I try to use this five tactic, I get could not find native implementation of external declaration 'myFunction'.

I've tried to split the code in different ways and tried to package the tactic as a plugin and then link it but with no success. What is the right way to make the implementation of myFunction visible to the tactic?

[Mac]

@Ramon Fernandez Mir In order to use foreign functions in interpreted contexts (e.g., files run directly with the lean binary; editing in the editor, interactive theorem proving, etc.) you need to build your library with -shared and pass it to lean as a plugin (with --plugin path/to/built/shared/library.[dll|so]). To provide such a plugin to the lean server that an VSCode uses you will need a new version of the extension that allows you pass the --plugin argument to server. This feature is already in the master branch (disclaimer: I was the one who added it), but you will need to wait until @Gabriel Ebner releases a new version to get it by the ordinary distribution channels.

[Ramon Fernandez Mir]

I see. What about simply using the plugin from lean --run? I thought that creating the shared object like this leanc -shared -x none build/cpp/MyFunction.o -o build/cpp/MyFunction.so and then running lean --run FileUsingMyFunction.lean --plugin=build/cpp/MyFunction.so would do the trick. But I get the following error :.../MyFunction.so does not seem to contain a module 'MyFunction.Default'. What does that mean?