Call Function in Shared Library

Stream: lean4

[Cole Shepherd]

How can I call a function in a shared library from Lean? I have the following Lean code in Main.lean (and more I'm omitting):

@[extern "SDL_Init"]
opaque SDL_Init : (flags: Uint32) -> IO (Int32)

And the following lakefile:

import Lake
open Lake DSL

package «lean-sdl-pong» {
  -- add package configuration options here
}

lean_lib LeanSdlPong {
  -- add library configuration options here
}

@[default_target]
lean_exe «lean-sdl-pong» {
  root := `Main
}

The SDL_Init extern is defined in SDL2.dll. SDL2.dll is in the same directory as my source code currently. When I compile the project with lake build I get errors like:

ld.lld: error: undefined symbol: SDL_Init
>>> referenced by .\build\ir\LeanSdlPong.o:(l_SDL__Init___boxed)

How can I tell the linker to link against SDL2.dll?

[James Gallicchio]

I'm not sure how exactly linking dlls works compared to shared objects in linux, but you can add arguments to the linker via the moreLinkArgs argument of the package declaration. See examples here, here

[James Gallicchio]

We still haven't really figured out the best way to handle linking non-Lean dependencies into Lean executables, so you will almost definitely encounter bugs or confusing/inconsistent behavior. If you get something working, let us know so we can add it to the list of examples that work :joy:

[Cole Shepherd]

Yeah, it looks to me like you need to write a shim library in C to call non-Lean dependencies unfortunately

[James Gallicchio]

It's pretty rare to have a function signature that doesn't need a shim library anyways; like, in your example, IO Int32 doesn't correspond to C's int32_t, so you need the shim library anyways to handle the IO boxing stuff. (you could make it return just Int32, which I think is sound, but you're probably right that it should be in IO).

You should be able to link against stuff directly (without a C shim) if the names aren't mangled in some way.