Reservoir

xubaiw/lean-problem-dynamic-link

None Description

GitHub Link Documentation

Pick a version!

TODO: should show a time axes that allows the users to view, filter and click copy the lakefile config.

README

Problems with Lean Dynamic Link

How to reproduce the error

$ cd bar1
$ lake build
...
$ cd ../bar2
$ lake build
...
$ ./build/bin/bar2  -- running the program produce the error
dyld[66116]: Library not loaded: ./build/lib/libbar1.dylib
  Referenced from: /Users/xubaiw/bar/bar2/build/bin/bar2
  Reason: tried: './build/lib/libbar1.dylib' (no such file), '/usr/local/lib/libbar1.dylib' (no such file), '/usr/lib/libbar1.dylib' (no such file), '/Users/xubaiw/bar/bar2/build/lib/libbar1.dylib' (no such file), '/usr/local/lib/libbar1.dylib' (no such file), '/usr/lib/libbar1.dylib' (no such file)
zsh: abort      ./build/bin/bar2

Details

In this repo we have two lean packages: bar1 and bar2.

In bar1 there is:

@[export bar1_greet]
def greet (name : String) := s!"Hello, {name}!"

Then bar1 is compiled to a sharedLib. In order to use the definition, in bar2 we have:

@[extern "bar1_greet"]
constant greet : String → String

def main : IO Unit :=
  IO.println <| greet "Lean Programmers"

Both moreLibTargets and moreLinkArgs is used in bar2:

package bar2 (pkgDir) (args) do
  let current ← IO.currentDir
  let dylibDir := current / ".." / "bar1" / "build" / "lib" 
  let dylib := dylibDir / s!"libbar1.{sharedLibExt}"
  IO.println s!"link to {dylib}"
  return {
    name := `bar2
    moreLibTargets := #[
      inputFileTarget dylib
    ]
    moreLinkArgs := #["-l", "bar1", "-L", dylibDir.toString]
  }