Add support for windows builds

[Febbe]

In many companies, windows is the defacto standard operating system, it would therefore be useful, to also support windows as operating system.
Currently, one can enable MSYS / MINGW in the platform.mk, but bsv even fails to compile with MSYS2.
It would even better, to switch completely to a more modern build system.

[quark17]

We're happy to support Windows or use a more modern build system, if someone wants to contribute a PR. In fact, I thought we had a GitHub Issue open for switching to a better build system, but I don't see one. I'm a dinosaur, so I don't even know what would be an example of "a modern build system" -- I guess I know that CMake exists, does that count? -- if you could list what you had in mind, that would be helpful.

I don't understand how to use Windows, so I wouldn't be able to judge a PR, but am happy to accept one. A bigger issue is that GitHub doesn't provide a Windows VM for regression testing. GitHub supports connecting to your own servers, so if someone can host a Windows runner for the CI, that would help ensure that we don't break the Windows support after accepting a PR.

[Febbe]

We're happy to support Windows or use a more modern build system, if someone wants to contribute a PR. In fact, I thought we had a GitHub Issue open for switching to a better build system, but I don't see one. I'm a dinosaur, so I don't even know what would be an example of "a modern build system" -- I guess I know that CMake exists, does that count?

It's exactly what I meant, some would also consider meson, but I have no experience using meson.

I don't understand how to use Windows, so I wouldn't be able to judge a PR, but am happy to accept one. A bigger issue is that GitHub doesn't provide a Windows VM for regression testing. GitHub supports connecting to your own servers, so if someone can host a Windows runner for the CI, that would help ensure that we don't break the Windows support after accepting a PR.

GitHub actions provide them actually: https://github.com/actions/runner-images/blob/main/images/windows/Windows2022-Readme.md

I can try to provide CMake configurations, but this might take a while, because I have to do this in my free time.

[quark17]

Ah, you're right. I don't know why I thought they didn't have Windows runners. Sorry!

Currently, one can enable MSYS / MINGW in the platform.mk, but bsv even fails to compile with MSYS2.

Out of curiosity, can you say what fails? I would believe, for example, that BSC's code constructs file paths in ways that aren't portable (like using hardcoded slashes). And there are submodules like STP that have their own codebase and Makefiles that might not support Windows? (but STP can be stubbed out, or we can work on upgrading STP and Yices to newer versions) But I'd also guess that Windows executables don't load dynamic libraries in the same way? so maybe the current handling of the SMT libraries (loading via the LD_LIBRARY_PATH) won't work on Windows anyway? or would it? (but we can avoid that issue by switching to static linking for those libraries?) Are there other issues that one runs into?

I can try to provide CMake configurations

If you're able to, that would be awesome! But no worries! I know that we're all volunteers, and we're all busy, so anyone who contributes is doing so in their free time, and we're appreciative when people are able to give.

But one question: I would assume that CMake is orthogonal to getting BSC compiling with Windows? My impression is that CMake would help identify the user's environment and the particular flags and tools etc for compiling. With the current Makefiles and platform.sh, we can identify a few specific environments -- but of course it is fragile, so if the user needs a slightly different flag somewhere, then it breaks down; and we only support the configurations that we have manually added, we don't get other configurations automatically; both of which CMake would help with (as I understand). But in theory we could add a single (fragile) Windows configuration to the Makefiles, and get BSC to compile with that, and then later convert the build to CMake; versus convert the Makefiles to CMake first and then still have to get the BSC code to work on Windows. I would have thought the first way would be better? but I haven't worked with CMake or Windows.

[Febbe]

Out of curiosity, can you say what fails? I would believe, for example, that BSC's code constructs file paths in ways that aren't portable (like using hardcoded slashes). And there are submodules like STP that have their own codebase and Makefiles that might not support Windows? (but STP can be stubbed out, or we can work on upgrading STP and Yices to newer versions).

It fails to build STP and SAT:

Febbe@PC-Febbe UCRT64 /c/Users/Febbe/Desktop/ws/bsc-2024.07/bsc
$ make install-src
make  -C src  PREFIX=/c/Users/Febbe/Desktop/ws/bsc-2024.07/bsc/inst  install
make[1]: Entering directory '/c/Users/Febbe/Desktop/ws/bsc-2024.07/bsc/src'
make  -C vendor/stp   PREFIX=/c/Users/Febbe/Desktop/ws/bsc-2024.07/bsc/inst  install
make[2]: Entering directory '/c/Users/Febbe/Desktop/ws/bsc-2024.07/bsc/src/vendor/stp'
make -C src install
make[3]: Entering directory '/c/Users/Febbe/Desktop/ws/bsc-2024.07/bsc/src/vendor/stp/src'
make -C sat core
make[4]: Entering directory '/c/Users/Febbe/Desktop/ws/bsc-2024.07/bsc/src/vendor/stp/src/sat'
make LIB="core" -C core libr
make[5]: Entering directory '/c/Users/Febbe/Desktop/ws/bsc-2024.07/bsc/src/vendor/stp/src/sat/core'
depend.mk:1: *** multiple target patterns.  Stop.

Interestingly, the produced file looks like this (the last path is missing the /c/):

/c/Users/Febbe/Desktop/ws/bsc-2024.07/bsc/src/vendor/stp/src/sat/core/Main.o /c/Users/Febbe/Desktop/ws/bsc-2024.07/bsc/src/vendor/stp/src/sat/core/Main.or /c/Users/Febbe/Desktop/ws/bsc-2024.07/bsc/src/vendor/stp/src/sat/core/Main.od /c/Users/Febbe/Desktop/ws/bsc-2024.07/bsc/src/vendor/stp/src/sat/core/Main.op: \
/c/Users/Febbe/Desktop/ws/bsc-2024.07/bsc/src/vendor/stp/src/sat/core/ C /c/Users/Febbe/Desktop/ws/bsc-2024.07/bsc/src/vendor/stp/src/sat/core/ Cr /c/Users/Febbe/Desktop/ws/bsc-2024.07/bsc/src/vendor/stp/src/sat/core/ Cd /c/Users/Febbe/Desktop/ws/bsc-2024.07/bsc/src/vendor/stp/src/sat/core/ Cp:/Users/Febbe/Desktop/ws/bsc-2024.07/bsc/src/vendor/stp/src/sat/core/Main.cc \
/c/Users/Febbe/Desktop/ws/bsc-2024.07/bsc/src/vendor/stp/src/sat/core/ C /c/Users/Febbe/Desktop/ws/bsc-2024.07/bsc/src/vendor/stp/src/sat/core/ Cr /c/Users/Febbe/Desktop/ws/bsc-2024.07/bsc/src/vendor/stp/src/sat/core/ Cd /c/Users/Febbe/Desktop/ws/bsc-2024.07/bsc/src/vendor/stp/src/sat/core/ Cp:/Users/Febbe/Desktop/ws/bsc-2024.07/bsc/src/vendor/stp/src/sat/utils/System.h \

[...]

But I'd also guess that Windows executables don't load dynamic libraries in the same way? So maybe the current handling of the SMT libraries (loading via the LD_LIBRARY_PATH) won't work on Windows anyway? or would it? (but we can avoid that issue by switching to static linking for those libraries?) Are there other issues that one runs into?

Yes, the loading is a bit different, but the operating system automatically does that for on-load-time dynamic libraries, as long the OS can find them.

Are there other issues that one runs into?

• Most issues result from using POSIX OS functions.
  • A temporary workaround is to use a POSIX-compliant toolchain like MSYS2 or CYGWIN. Those add a compatibility layer between POSIX and the native WIN32-API. Unfortunately not all posix functions have an implementation in MSYS/CYGWIN.
• Another issue may arise from SIGNALS, which aren't supported on Windows.
  • E.G. SIGVTALRM, the correct solution, would be to use the Windows API, but I fixed that with a std::thread and a sleep. The CPP implementation of sleep_for works similarly.

I would assume that CMake is orthogonal to getting BSC compiling with Windows?

It is, at least, to support a build via MSYS. But makefiles aren't supported on Windows, when we want to compile BSC natively via cl.exe (MSVC) or clang-cl.exe (LLVM with MSVC support), we must switch to a platform-independent build system.
Supporting MSYS as the platform would be way easier.