Cross Compiling Lean executabel for windows from linux

Stream: new members

[Srayan Jana]

Hi! I'm currently using WSL, and im able to compile a linux executable just fine. However, I'd like to build a native windows application, but im not sure how to go about it. Any ideas?
For context, still messing around with this: https://github.com/DSLstandard/Lean4-FFI-Programming-Tutorial-GLFW

[Srayan Jana]

Doing a little digging and I think I have an idea. There is an environmental variable for lean called LEAN_CC that sets the c compiler used for lean
https://lean-lang.org/doc/reference/latest/Build-Tools-and-Distribution/Lake/#LEAN_CC

Additionally, mingw is available on Linux to compile for windows: https://stackoverflow.com/questions/2033997/how-to-compile-for-windows-on-linux-with-gcc-g

https://www.mingw-w64.org/downloads/

https://www.mingw-w64.org/getting-started/debian/

[Srayan Jana]

Okay did a bit of work, and I was able to make this command execute
sraya@Penelope:~/Lean4-FFI-Programming-Tutorial-GLFW$ LEAN_CC=x86_64-w64-mingw32-gcc lake build Build completed successfully. sraya@Penelope:~/Lean4-FFI-Programming-Tutorial-GLFW$
however, i don't think it actually worked

[Srayan Jana]

Okay so, update:
https://github.com/DSLstandard/Lean4-FFI-Programming-Tutorial-GLFW/issues/3#issuecomment-3225223987
TL;DR this miiiiight be impossible for now