cross compiling lean

Stream: general

[Srayan Jana]

Hi! This is a sequel to the previous thread I made about this, but I figured it makes more sense to put this here
Me and @DSLstandard on GitHub did a bunch of research on how to cross compile lean for Windows, and he came up with this solution
https://github.com/DSLstandard/Lean4-FFI-Programming-Tutorial-GLFW/issues/3#issuecomment-3234008693

However this isn’t … ideal.

I’d be willing to contribute a PR to lake to try to make this less annoying. Would the lean developers be interested in such a PR?

[Kim Morrison]

You'd have to talk to Mac Malone about PRs to Lake.

[Srayan Jana]

@Mac Malone would you mind if I DM you with more information?

[Mac Malone]

@Srayan Jana I read through the issue, and it is not clear to me what you are prosposing to PR. However, feel free to tto DM me with more information. :smile: