Compile to DLL

Stream: general

[Robert Maxton]

I'm considering using Lean for a general purpose programming project. The project as a whole requires too much GUI etc functionality for Lean to be a good fit at the moment, but there is a core "kernel" that is well-suited to being implemented in Lean. As such, I'd like to write something in Lean and compile it to a DLL I can link to from another language.

Lake has documentation for making Lean libraries, and complete standalone executables, but I don't see anything for DLLs. Please advise?

[Daniel Weber]

I think you want to use FFI: https://lean-lang.org/lean4/doc/dev/ffi.html. I'm not sure about the details, though. See https://github.com/leanprover/lean4/tree/master/src/lake/examples/reverse-ffi for an example

[Utensil Song]

You'll need reverse FFI if your GUI is in other languages and calls the "kernel" in Lean. In that case, https://github.com/lecopivo/ReverseFFIwithMathlib is a great reference by @Tomas Skrivan . It overcomes many subtle issues.

[Robert Maxton]

Excellent, thanks to you both!