Precompile modules on Windows

Stream: lean4

[Tomas Skrivan]

I'm trying to build SciLean on Windows but I'm having issues with precompileModules option and I'm getting linker errors undefined symbol ....

---

Here is mwe

lakefile.lean

import Lake
open Lake DSL System

package foo

lean_lib Foo where
  roots := #[`Foo]
  precompileModules := true

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

Foo/Basic.lean

@[extern "hello_impl"]
opaque hello (name : String) : String

Foo/Impl.lean

@[export hello_impl]
def helloImpl (name : String) := s!"hello {name}"

Foo.lean

import Foo.Basic
import Foo.Impl

Main.lean

import Foo

def main : IO Unit :=
  IO.println s!"Hello, {hello "John"}!"

---

Running lake build produces error

Γ£û [8/16] Building Foo.Basic:dynlib
trace: .> c:\Users\skriv\.elan\toolchains\leanprover--lean4---stable\bin\leanc.exe -shared -o .\.\.lake\build\lib\Foo-Basic-1.dll .\.\.lake\build\ir\Foo\Basic.c.o.export -L.\.\.lake\build\lib
info: stderr:
ld.lld: error: undefined symbol: hello_impl
>>> referenced by .\.\.lake\build\ir\Foo\Basic.c.o.export:(l_hello___boxed)
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command 'c:\Users\skriv\.elan\toolchains\leanprover--lean4---stable\bin\leanc.exe' exited with code 1
Some required builds logged failures:
- Foo.Basic:dynlib
error: build failed

Looks like that the call to leanc is missing -lFoo-Impl-1. So manually calling

c:\Users\skriv\.elan\toolchains\leanprover--lean4---stable\bin\leanc.exe -shared -o .\.\.lake\build\lib\Foo-Basic-1.dll .\.\.lake\build\ir\Foo\Basic.c.o.export -L.\.\.lake\build\lib -lFoo-Impl-1

does not fail anymore and produces desired Foo-Basic-1.dll.

Now we have Foo-Basic-1.dll lets try resume build and call lake build again. It fails with

Γ£û [10/16] Building Foo
trace: .> LEAN_PATH=.\.\.lake\build\lib PATH c:\Users\skriv\.elan\toolchains\leanprover--lean4---stable\bin\lean.exe .\.\.\.\Foo.lean -R .\.\.\. -o .\.\.lake\build\lib\Foo.olean -i .\.\.lake\build\lib\Foo.ilean -c .\.\.lake\build\ir\Foo.c --load-dynlib=.\.\.lake\build\lib\Foo-Basic-1.dll --load-dynlib=.\.\.lake\build\lib\Foo-Impl-1.dll --json
info: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading library .\.\.lake\build\lib\Foo-Basic-1.dll: 126
error: Lean exited with code 3221226505
Some required builds logged failures:
- Foo
error: build failed

I have not been successful in modifying this command to make it succeed.

---

Is this a bug in lake? @Mac Malone Or what am I doing wrong?

[Sebastian Ullrich]

Oh wow, we definitely didn't design it with such extern/export cross-edges in mind

[Tomas Skrivan]

Uhh what do you mean? I'm just recreating what is done with simp/simpImp, whnf, isDefEq etc.

[Tomas Skrivan]

Maybe I'm not doing it right but it works on Linux. (I didn't test this particular mwe on Linux as I'm on Windows right now but in SciLean I'm doing something identical)

[Tomas Skrivan]

How am I supposed to write a recursive tactic like simp using extern/export and use it in my project? I need `precompileModules, right?

The above mwe compiled fine if I remove precompileModules but then I can't #eval main in Main.lean as I get server error

libc++abi: terminating due to uncaught exception of type lean::exception: Could not find native implementation of external declaration 'hello' (symbols 'l_hello___boxed' or 'l_hello').

[Sebastian Ullrich]

Just because core does it doesn't mean it's the best solution for user code. If it's infeasible to contain the recursion in one mutual, you could for example store the function for recursive use in an IO.Ref, kind of the userspace equivalent of export+extern

[Tomas Skrivan]

I see, I will keep that in mind. However right now I have a fork of simp and redesigning to that would probably be quite some work.

[Sebastian Ullrich]

The IO.Ref should be a simple change

[Tomas Skrivan]

Do I understand it correctly that I it should look something like this:

Init.lean

initialize factorialRef : IO.Ref (Nat → IO Nat) ← IO.mkRef (fun x => return x)

def factorial (n : Nat) : IO Nat := do
  let ref ← factorialRef.get
  return (← ref n)

Impl.lean

def factorialImpl (n : Nat) : IO Nat := do
  match n with
  | 0 => return 1
  | n + 1 => return (n+1)* (← factorial n)

initialize factorialRef.set factorialImpl

#eval factorial 4

[Tomas Skrivan]

In that case the change should be easy, thanks for the help!

[Tomas Skrivan]

Great, fixing SciLean was just six lines and now it compiles on Windows.

[Sebastian Ullrich]

FYI, what probably happened here is that Linux allows undefined symbols in shared libraries as long as they are defined at load time, and Windows doesn't. So this is a correct cross-platform solution.

[Yakov Pechersky]

This is also the case for Macs, as I've learned recently. Where the solution is -Wl,-undefined,dynamic_lookup: https://blog.tim-smith.us/2015/09/python-extension-modules-os-x/