Trouble resolving extern code

Stream: lean4

[Mario Carneiro]

I am trying to load an environment by importing .olean files. I am calling initSearchPath and seem to be finding the .oleans, but the import gives me an error about an external declaration. Is there an additional path/env variable I need to set?

import Lean
open Lean

unsafe def main : IO Unit := do
  Lean.initSearchPath "/home/mario/.elan/toolchains/leanprover--lean4---nightly/lib/lean/"
  withImportModules [{ module := `Init }] (opts := {}) (trustLevel := 0) $ λ env => do
    println! "success"

$ leanpkg build bin
configuring test 0.1
> sh -c "/home/mario/.elan/toolchains/leanprover--lean4---nightly/bin/leanmake" PKG=Test LEAN_OPTS="" LEAN_PATH="././build" bin MORE_DEPS+="leanpkg.toml" >&2    # in directory .
lean  -o "build/Test.olean" --c="build/temp/Test.c.tmp" Test.lean
mv "build/temp/Test.c.tmp" "build/temp/Test.c"
leanc -c -o build/temp/Test.o build/temp/Test.c -O3 -DNDEBUG
leanc -o "build/bin/Test" build/temp/Test.o

$ build/bin/Test
uncaught exception: could not find native implementation of external declaration 'Nat.div' (symbols 'l_Nat_div___boxed' or 'l_Nat_div')

[Sebastian Ullrich]

Probably the ol' -rdynamic

[Mario Carneiro]

where do I put that?

[Sebastian Ullrich]

(The MORE_DEPS+="leanpkg.toml" is a nice touch)

[Mario Carneiro]

that did the trick. So much cursed knowledge...

[Daniel Selsam]

Sebastian Ullrich said:

Probably the ol' -rdynamic

Thanks! This explains why I couldn't reproduce in my setup -- I have been copy-pasting a Makefile to every new project for over a year, and it luckily includes -rdynamic already.