Dependency in external libraries

Stream: lean4

[Leni Aniva]

If a Lean library depends on an extern_lib, and the extern_lib links to other system libraries, how can I ensure the linker can link to these libraries? I have a setup like this:

extern_lib libmystery pkg := do
  let leanRoot := (← Lean.getBuildDir).toString
  proc {
    cmd := "cargo", args := #["build", "--release"],
    cwd := pkg.dir, env := #[("LEAN_ROOT", .some leanRoot)],
  }
  let name := nameToStaticLib "mystery"
  let srcPath := pkg.dir / "target" / "release" / name
  IO.FS.createDirAll pkg.staticLibDir
  let dstPath := pkg.staticLibDir / name
  IO.FS.writeBinFile dstPath (← IO.FS.readBinFile srcPath)
  return (pure dstPath)

@[default_target]
lean_exe mystery where
  root := `Main

and when I build this, it prints ld.lld: error: undefined symbol ... for the external libraries linked with libmystery.

[Gavin Zhao]

I think there are two ways to approach this:

1. I see you're using Rust. You can have a create that has type cdylib so that you're producing a dynamic library, then use lake's support for linking shared libraries and it should just work.
2. If all of the external library dependencies come from your crate dependencies, then it's very likely these crates have feature flags you can toggle on to build and link against a static library copy instead of linking against the dynamic library on your system.

[Leni Aniva]

Gavin Zhao said:

I think there are two ways to approach this:

1. I see you're using Rust. You can have a create that has type cdylib so that you're producing a dynamic library, then use lake's support for linking shared libraries and it should just work.
2. If all of the external library dependencies come from your crate dependencies, then it's very likely these crates have feature flags you can toggle on to build and link against a static library copy instead of linking against the dynamic library on your system.

so instead of pkg.staticLibDir I just use pkg.sharedLibDir?

[Gavin Zhao]

More than that. I assume you want to go with 1? Then, you also need to change your Rust crate type to cdylib to produce a shared library. Then, your snippet should become:

extern_lib libmystery pkg := do
  let leanRoot := (← Lean.getBuildDir).toString
  proc {
    cmd := "cargo", args := #["build", "--release"],
    cwd := pkg.dir, env := #[("LEAN_ROOT", .some leanRoot)],
  }
  let name := nameToSharedLib "mystery"
  let srcPath := pkg.dir / "target" / "release" / name -- check if this is actually the path
  IO.FS.createDirAll pkg.sharedLibDir
  let dstPath := pkg.sharedLibDir / name
  IO.FS.writeBinFile dstPath (← IO.FS.readBinFile srcPath)
  return (pure dstPath)

[Gavin Zhao]

This link is for a different context but should help you get started. Basically the problem you're solving is how to build a dynamic/shared library from Rust.

[Leni Aniva]

I changed crate-type = ["cdylib"] and staticLib to sharedLib and now it all works!

[Gavin Zhao]

If your crate is not for the sole purpose of interfacing with Lean, you might want to have crate-type = ["lib", "cdylib"] so people can also use your crate in Rust.