Windows Builds with MSVC

[cpkleynhans]

Changes required to get KodKod to build on Windows with MSVC. Fixes #57

[cpkleynhans]

This is still a work in progress. I've managed to get everything to build except for minisat prover.

Looks like most of minisat prover's code is platform independent with the exception of File.h and File.cc Those require the posix file APIs to be present.

I'm considering either disabling minisat prover on Windows (when using MSVC, not when we use MinGW), or just writing my own File.cc for Windows (which I worry about getting appropriate test coverage for).

Any thoughts? (@mhyee)

[mhyee]

I think it's safer to just disable minisat_prover when using MSVC. It is not our responsibility to fork and rewrite the solvers. (Unrelated, but this is why I prefer using GCC over rewriting code to get Kodkod to build on Mavericks.)

If I have a chance tomorrow, I'll try pulling your changes and confirming that it builds on my Windows machine.

[cpkleynhans]

@mhyee Yes I think you're right.

I think I'll try to write up some helper methods to make it easier to selectively enable/disable solvers (perhaps using some sort of feature detection for cases like OpenMP).

[cpkleynhans]

Ok, I've disabled building minisat prover when using MSVC.

[cpkleynhans]

Took a look at lingeling and cryptominisat.

I've managed to get cryptominisat to build on my machine with a small change to one of its headers. lingeling looks like it will be harder, its doing something complicated in its wscript file.

[cpkleynhans]

Also, /Wall seems to be incredibly noisy with MSVC (it warns us when functions were not inlined for example). I'll see if there is a better set of warning flags to pass it.

[mhyee]

Were you going to add anything else to this PR?

It turns out my Windows machine isn't quite set up for Kodkod dev. The changes look reasonable, so feel free to merge if you're done. Unless you'd like confirmation on another Windows machine.

[cpkleynhans]

@mhyee So, I think there's one last problem to address. Currently waf deps depends on curl being installed on the system (we shell out to perform the actual download). This worked on my machine because I happened to have curl installed, but I don't know if that's a safe assumption in general.

Currently, we only require the dependencies to be installed if unit tests are to be run. Perhaps we should create a new all-no-tests command that skips the unit tests and thus wouldn't require any external dependencies?

[mhyee]

I don't think we can assume that curl is installed.

I think it's fair to require dependencies. I don't think we should create an all-no-tests task -- if people want to work on Kodkod, that includes running the tests and having all the required dependencies.

What we could do is make the error handling more graceful -- maybe check for curl and output a message if it can't be found.

[cpkleynhans]

So, I agree that anyone doing development on kodkod should be running the tests, but will everyone who builds kodkod be making modifications (and if they aren't making modifications should they be required to run tests just to build the jar file)?

Regardless making the error handling for missing dependencies is a good idea.

[mhyee]

OK, I see what you mean. Adding an all-no-tests task is probably a good idea then.

[cpkleynhans]

Ok, I've added a --skip-tests flag to waf all.

Still going to look into better error messages.

[cpkleynhans]

I've rewritten the deps task to download dependencies using python's built-in urllib2 instead of shelling out to curl.

One thing that worries me is that we aren't performing any verification of the libraries we download to ensure they are what we expect. I'm going to look into adding some verification, maybe file hashes.

[cpkleynhans]

@mhyee Ok, I think that's all the changes we need to make to get things building with MSVC on Windows. I'm going to try testing these on a "cleaner" Windows install to make sure everything works.

[cpkleynhans]

Ok, I've spun up a Windows 8.1 VM with Visual Studio 2013 Express, Python, Java and Git. The build seems to go fine except that its building 32-bit binaries for a 64-bit system.

I'm going to investigate to see whether this is a limitation of using an Express edition, or if its a problem with the build system.

[cpkleynhans]

Ok, looks like its just that Visual Studio 2013 Express doesn't ship with the native x64 compilers. Used vcvarsall.bat to setup a cross compile and everything worked fine.

I think that's all the changes we need, @mhyee can you take another quick look before I merge?

[mhyee]

I just have two nitpicks, but otherwise, everything looks fine. You can merge (after fixing or wontfixing the two comments). Unless you'd like me to set up a Windows VM and confirm this PR on my own.