Running `extern` declarations

Stream: lean4

[Mac]

Given the file Context.lean:

namespace Papyrus
constant ContextRef : Type := Unit
@[extern "papyrus_context_new"] constant ContextRef.new : IO ContextRef
end Papyrus

def testNew : IO PUnit := do
  discard <| Papyrus.ContextRef.new

#eval testNew

Running it with

lean --run Context.lean

Gives:

could not find native implementation of external declaration 'Papyrus.ContextRef.new' (symbols 'l_Papyrus_ContextRef_new___boxed' or 'l_Papyrus_ContextRef_new')

Why is Lean looking for l_Papyrus_ContextRef_new instead of papyrus_context_new?

[Mac]

Furthemore, since the functionl_Papyrus_ContextRef_new is part of the compiled c file for Context.lean, I would assume that the existence of such an external symbol would actually clash with the definition.

[Mac]

Thus I am wondering whether this is a bug and thus if I should submit an issue.

[Mac]

Also, I should note the same error appears if ContextRef.new is defined in a import rather than the main file.

[Sebastian Ullrich]

This is all as intended. The interpreter looks for the boxed Lean definition as it has a homogeneous ABI. Extern declarations must be compiled to be executable.

[Mac]

Ah so you have to have the external Lean symbol within the plugin (not just the external symbol). Okay, thanks for the info.