Checking symbols in the current binary

Stream: lean4

[Eric Wieser]

Is this expected to work?

@[extern "l_Int_div___boxed"]
opaque call_int_div : Int → Int → Int

#eval call_int_div 1 2

It seems to crash the server for me.

[Eric Wieser]

(#xy: can I inspect from within Lean whether a name `foo has a native implementation available?)

[Henrik Böving]

If by native you mean any native code associated then no not currently but if we were to make this function part of our API: https://github.com/leanprover/lean4/blob/master/src/library/compiler/ir_interpreter.cpp#L298 then yes.

If you mean extern, yes that's easy its just an attribute

[Eric Wieser]

I mean the former

[Eric Wieser]

Do you have a feeling for why my example above doesn't work?

[Mario Carneiro]

I think this is because the relevant function is not marked LEAN_EXPORT, because they used to be and this was busting the DLL exported symbols budget on windows

[Eric Wieser]

If I objdump -T my lean binary on linux, I see the symbol is there

[Eric Wieser]

I guess I'll attach lldb and see what's going on

[Mac Malone]

@[extern] definitions are not direct calls of the specified symbol. Instead, the symbol is wrapped within another C definition produced by the Lean compiler. That wrapper is the native symbol invoked by the interpreter. Thus, an @[extern] can never be evaluated in the module in which it is declared (as the native symbol for the wrapper will not have been compiled yet). Even in core, such native symbols are drawn from the previous stage, not the one currently being compiled.