does leans ffi only work on Linux?

Stream: new members

[Srayan Jana]

Looking at the official example, it seems to only work with shared .o files and not .dll
https://github.com/leanprover/lean4/blob/master/src/lake/examples/ffi/lib/lakefile.lean
I haven’t tested to see if it would work statically linked but it’s a shame dynamic linking seems to not be a thing

[Sebastian Ullrich]

It should work as expected on all supported platforms, it is run by our CI on all of them. .o object files are what comes before static/shared archives.

[Srayan Jana]

Gotcha, I’ll try it out again

[Chase Norman]

Canonical has dynamic linking working on Mac, Windows, and Linux.

[Julian Berman]

I got it working fairly painlessly as well for rpylean, though I probably never tested on Windows. https://github.com/Julian/rpylean/blob/main/rpylean/leanffi.py

[Eric Taucher]

(deleted)

[Srayan Jana]

I should mention that I eventually got the FFI working on both Linux and Windows, but there has been a lot of complications
https://github.com/ValorZard/LeanDoomed/tree/main
Right now, I can build it from source, but I can't create a distributable executable

Really the worst part has been interfacing with the C Compiler and trying to figure out the right combinations of build flags to get LLVM and GCC to work properly

[Eric Taucher]

(deleted)

[Eric Taucher]

(deleted)

[Eric Taucher]

(deleted)

[Srayan Jana]

@Eric Taucher if you want, I'd love if you could get the repo I linked to run on your computer. It SHOULD, but idk. I wrote instructions in the README to help you out