Support windows

[isuruf]

Looks like CMakeLists.txt supports windows

[mbargull]

@isuruf, do you have any idea how hard it would be to make this compile on Windows? My "compiling under Windows"-fu is more than rusty, so sadly I'm not likely to be of any help here. If everything goes well and in reference to https://github.com/conda/conda/pull/7676#discussion_r211319757 and https://github.com/msoos/cryptominisat/issues/513, we may be very interested in making this available on all platforms :wink:.

[msoos]

:) CryptoMiniSat definitely compiles under Windows. It compiles as part of the CI pipeline on AppVeyor, without a hitch. Please check it out: https://ci.appveyor.com/project/msoos/cryptominisat

[isuruf]

Looks like it can't be compiled with VS2008, so no python 2.7, but python 3.5 and above should be doable

[msoos]

That is very possible -- I do use some C++11 concepts. However, the compilation should be fine on Mac, Windows and most Linux distros after circa 12. AppVeyor only allows testing with VS2015 unfortunately.

[mbargull]

it can't be compiled with VS2008, so no python 2.7

That's a little bit unfortunate because I think we still have to provide Python 2 builds of conda for a while. But to be honest, I don't think this is problematic in regards to whether we switch to CryptoMiniSat in conda or not. We can just continue to use pycosat for the PY2 builds; supporting both solvers shouldn't introduce too much of a maintenance burden, IMO. (cc @kalefranz) (Okay, maybe I even like that fact a little bit :smiling_imp: : it gives us yet another good argument we can tell the Miniconda2/Anaconda2 users to make them finally switch to the PY3 varieties: "Do you want faster solving? Just put python=3 into your base environment!" :wink:)

[kalefranz]

😈 indeed

[kalefranz]

It also makes us keep the interface conda uses to SAT independent of any specific implementation.

[mingwandroid]

I've taken a quick look at the source code, @msoos, I see that cryptominisat already depends on boost, so would it be possible to switch out some C++11 for boost implementations since we have boost for visual studio 2008.

The first example of where this may be possible is in cmsat5-src\cryptominisat5\cryptominisat.h where it uses \<atomic>.

[kalefranz]

@mingwandroid I’m hopeful we can strip out the boost dependency as discussed in https://github.com/conda-forge/cryptominisat-feedstock/issues/9 along with M4RI. Making boost a hard dependency of conda is pretty much a non-starter.

[mbargull]

Thanks for taking a look, @mingwandroid. IIUC, Boost is only used for the (non-*_simple) executable and not for the library itself and thus completely optional (if one is willing to omit building that executable). I'm not sure if it makes sense to add it to the library itself. That being said, if you'd only use the header-only parts of Boost, that would be fine in regards to what @kalefranz just wrote since it wouldn't introduce a runtime dependency. Though, I'm not sure I would want to force @msoos to work around using modern versions of a programming language just because of possible support for some other outdated software... It'd be fine for us to continue to use pycosat for the Windows+PY2 conda users, IMHO.

[mingwandroid]

Does it actually use boost libs or just headers though? If it's headers then we don't need to introduce a dep, as you say. I expect ripping out all C++11 is not feasible or desirable though.

[mingwandroid]

I'd rather we didn't have two different solvers in play personally. It's more work for all concerned. Having them pluggable is fine as it allows for easier experimentation, but I'd definitely prefer if we can settle on one globally.

[msoos]

@kalefranz boost is not needed unless you want an executable that has all the fancy flags. CMS does not use boost for anything but options parsing (it's super boring to write that code...). So the solver is fully featured without boost and compiles fully without boost. The only thing it will do is that it will create a binary called cryptominisat5_simple that only has a restricted set of options. Everything else is the same, nothing is affected other than command line options parsing. In particular, the python interface is 100% the same.

@mingwandroid As for using boost instead of C++11 -- that won't work :( I am using C++11 extensively and replacing everything with boost would be a nightmare :( Sorry!

[mingwandroid]

Ok good to know. Two solvers it is then? So long as we get good tests that they behave equivalently then I'm ok with it, sort of!

[mingwandroid]

What about using the mingw-w64 toolchain?

[msoos]

Two solvers it is then? So long as we get good tests that they behave equivalently then I'm ok with it, sort of!

They behave perfectly equivalently -- there is no difference whatsover in the compilation of the library.

What about using the mingw-w64 toolchain?

It should compile under mingw -- there have been people compiling it like that for a long time. I haven't used it for a while (since AppVeyor) but AFAIK it should compile without (too much of a) hitch :) Could you please take a shot at it?

[mingwandroid]

To build with mingw-w64 (with mingw-w64 python) I needed this patch

[mingwandroid]

MSYS2/mingw-w64 comes pre-installed on AppVeyor btw.

[msoos]

Oh, that's cool, thanks! I have now pushed the patch in:

288a4a76017c317939a367425fb8861c58245720 a2e98500e2fdfba0b422b20b410426569823befb

I should create an appveyor built config to do the mingw-w64... do you know how to do that? I am still a bit of a newbie to AppVeyor and it took me forever to get the Windows builds in, maybe you could do it faster than I could? There is no need for everything to compile (boost, zlib, etc.) for mingw, I'd be happy with the base executable (i.e. cryptominisat5_simple), without any libs. Let me know if this is too much to ask, I'll take a shot at it then :)