lake build on Windows - C FFI - undefined reference

Stream: lean4

[František Silváši]

Anyone got the Socket Library running on windows? I tried lake build compiling the main example of the framework and ran into "undefined reference to __imp_F" for all native Functions defined in the library. Socket has two static libraries, both of which are being provided in leanc someArgs .../libSocket.a .../native.a automatically. Am I missing something in the lakefile package definition?

[Xubai Wang]

Sorry for that, but this library has not been tested on Windows (since I don't have one :D). I have opened an issue for this error.
And just to note that this library is a toy implementation. A higher level IO library like rust's mio and c's libuv can be much better, which I'm working on now.

[Xubai Wang]

@František Silváši Sorry for being too late, I was stuck by setting up Lean environment on Windows.

All examples in the repo should now be runnable on Windows, with #["-lWs2_32"] in the moreLinkArgs field.

[Xubai Wang]

Currently it's impossible to specify shared lib dependencies in library packages (static lib cannot be linked to shared lib) and every binary package depends on it has to specify shared lib dependency in their package config. (e.g. "ws2_32.dll" for every package that uses lean4-socket).

@Mac Can lake store linkage information and pass them when linking binaries? Maybe by a separate links field for native library dependencies like rust?

Specifying moreLinkArgs in every dependent package can be a temporal workaround, but not a nice solution.

[František Silváši]

It works indeed! Glorious, thank you kindly.

[Mac]

Xubai Wang said:

Mac Can lake store linkage information and pass them when linking binaries? Maybe by a separate links field for native library dependencies like rust?

You should be using moreLibTargets for this. For example:

package foo where
  moreLinkArgs := if Platform.isWindows then #[inputFileTarget "/path/to/Ws2_32.dll"] else #[]

additional lib targets will be automatically be carried upwards to dependent packages.