Get solvers to build under windows

[chrjabs]

Getting the solvers to build under windows seems to be a challenge, since many of them use some GCC / Unix specific features. Get as many of them to compile in windows as possible, and include checks and tests in the CI.

[Coloquinte]

Cadical and Kissat are hard to provide on Windows (Kissat issue and Cadical instructions), but Minisat would be a good start so people can still use the crate :)

[chrjabs]

CaDiCaL and Kissat still not working

[marceline-cramer]

I've managed to get CaDiCaL working for Windows using the x86-64-pc-windows-gnu target cross-compiling from Ubuntu using cargo zigbuild. However, I've needed to fork rustsat-cadical to remove the invocations of the compiler tests in build.rs, which don't run on Ubuntu. I've needed to use zigbuild on Ubuntu because Windows doesn't have the headers available and because even when using zigbuild, Windows fails to link the final binaries. Compiling for x86-64-pc-windows-msvc seems out of the question for now because of CaDiCaL's heavy dependency on Unix-specific headers (such as unistd.h).

Also note that the compiler tests in build.rs also generally block any form of cross-compilation without running in an entire VM such as qemu. I also removed those tests so that my arm64 builds could compile without virtualization. From my understanding, those checks are there to replace autoconf compiler tests in CaDiCaL's vanilla build toolchain, but perhaps there's another way around those. This is its own can of worms.

Here's my current CI pipeline. Please note that while I set CC and CXX to Clang (and install Clang on Windows), zigbuild on Windows is overriding that with its own CC/CXX on the inside.

UPDATE: I forgot to mention that I have had no luck using cargo cross. It seems to be missing crucial cross-compilation headers for targets that it describes as having first-class support for (such as aarch64-unknown-linux-gnu). I've been much better off manually installing Ubuntu's cross compilation headers and using zigbuild instead.

[chrjabs]

Thanks for the info. It might be worth looking into getting some of this information into the documentation at least. With respect to the compilation tests in the build script, one could consider introducing an environment variable that allows for selecting available compiler features manually rather than detecting them on the fly. Would that work for you usecase?

[marceline-cramer]

That makes a lot of sense, yeah! Seems like a good compromise between changing the logic and avoiding cross-compilation. In my fork, though, I test that the tests compile and use that as the indicator for compiler support rather than testing if they both compile and run. I'm not sure if that breaks any logic meaningfully.

[chrjabs]

@marceline-cramer would you mind converting your project from your fork to the PR I just opened, setting CADICAL_RUN_CPP_TESTS=0 and then seeing if your CI still works?
You can also have a look at the PR in general (especially the first and last commit, the others are just things I came across along the way) and let me know if I missed anything.