Building plugins on Windows?

Stream: lean4

[Mac]

Is it currently not possible to build a Lean package into a plugin (i.e. shared library) on Windows? Running leanpkg build lib LEANC_OPTS="-shared" gives <lean>/bin/lean.exe.a: No such file or directory which is due to lean.exe.a not being built because of these commented out lines (https://github.com/leanprover/lean4/blob/02e917793e07d480ee09bda7b51210b976b47e6d/src/shell/CMakeLists.txt#L14-L20) which are stated to be "broken" (possibly due to some upstream MSYS2 problems?).

[Sebastian Ullrich]

Yeah, I don't know what broke upstream. So my best bet for a solution is https://github.com/leanprover/lean4/issues/466.