AppVeyor cannot yet compile CMS on MSVC

[msoos]

See https://ci.appveyor.com/project/msoos/cryptominisat/build/1.0.12 It errors out with:

LINK : fatal error LNK1181: cannot open input file '..\lib\Release\cryptominisat4.lib' [C:\projects\cryptominisat\cmsat4-src\cryptominisat4_simple.vcxproj]

and

LINK : fatal error LNK1181: cannot open input file '..\lib\Release\cryptominisat4.lib' [C:\projects\cryptominisat\cmsat4-src\libcryptominisat4ipasir.vcxproj]

Can you please try to take a look? Thanks!

[capiman]

Hi Mate,

I just downloaded and installed latest Visual Studio 2015 and cmake 3.5.1 on my new machine with Win10 on it.

I followed the steps you execute on appveyor.

1) This sequence:

git clone -q --branch=master https://github.com/msoos/cryptominisat.git c:\projects\cryptominisat
git checkout -qf 6f5166b9f6bef2d54675286bf669435a02f0ade5
echo Running cmake...
Running cmake...
cd c:\projects\cryptominisat

-> Checkout was not working, because I was not in c:\projects\cryptominisat. I had to do "cd c:\projects\cryptominisat" before checkout.

2) Next problem is xxd / tablestruct. I think by default it is compiled without stats? But it looks like tools for tablestruct are called, which I don't seem to have. I deleted some lines, hopefully the right ones. Suddenly I have seen it compiling the sources...

3) I saw in one of the CMakeFile. that ".a" was used, must be ".lib", but have not seen a problem, perhaps not used?

4) Directly to your problem. It looks like the *.lib is not created/put/read where you have assumed it to be.

Just what I say, without a solution, hope it helps:

C:\projects\cryptominisat\lib/Debug -> is empty C:\projects\cryptominisat\cmsat4-src\Debug -> contains a "cryptominisat4.dll" C:\projects\cryptominisat\cmsat4-src\temp_lib_norm.dir\Debug -> contains a "temp_lib_norm.lib" C:\projects\cryptominisat\cmsat4-src\temp_lib_ipasir.dir\Debug -> contains a "temp_lib_ipasir.lib"

But there is no cryptominisat4.lib in complete build directory.

5) Install directory (CMAKE_INSTALL_PREFIX) is not even created, therefore empty, but perhaps I must do some special CMAKE command to copy it there. At least the linker cannot find something there without this command.

Best regards, Martin

[capiman]

Workaround for compiling:

I changed (only locally in *.vcxproj, generated!):

kernel32.lib;user32.lib;gdi32.lib;winspool.lib;shell32.lib;ole32.lib;oleaut32.lib;uuid.lib;comdlg32.lib;advapi32.lib;..\lib\Release\cryptominisat4.lib

to

kernel32.lib;user32.lib;gdi32.lib;winspool.lib;shell32.lib;ole32.lib;oleaut32.lib;uuid.lib;comdlg32.lib;advapi32.lib;c:\projects\cryptominisat\cmsat4-src\temp_lib_norm.dir\Debug\temp_lib_norm.lib

First part of this line seems to come from CMAKE_CXX_STANDARD_LIBRARIES in CMakeCache.txt, second part must perhaps be changed, but I do not yet know enough about cmake to do this change.

PS: I was able to create a cryptominisat_simple.exe which was even placed in "install directory". When calling it, it crashes. I earlier builds I had to add "/F2097152" (increase stack size), otherwise crash in Dimacs parser. Perhaps same thing here. -> Added and tested *.exe, but same problem...

[msoos]

Hmmm....but we are making progress! :D Thanks a lot for the above! Do you think I should try doing it too? Or can you debug this somehow? I'm a bit reluctant to getting all the pieces together (boot into Windows, get trial MSVC, etc) but if I must then of course I will :)

[capiman]

Also see email from yesterday.

This way

C:\projects\cryptominisat\src>cl -DDRUP -DDISABLE_ZLIB /openmp /favor:INTEL64 /O2 /Fecryptominisat64simple.exe /F2097152 /TP /EHsc -I. -I.. main_simple.cpp signalcode.cpp cryptominisat.cpp cnf.cpp propengine.cpp varreplacer.cpp clausecleaner.cpp clauseusagestats.cpp prober.cpp occsimplifier.cpp subsumestrengthen.cpp clauseallocator.cpp sccfinder.cpp solverconf.cpp distillerallwithall.cpp distillerlongwithimpl.cpp str_impl_w_impl_stamp.cpp solutionextender.cpp completedetachreattacher.cpp searcher.cpp solver.cpp gatefinder.cpp sqlstats.cpp implcache.cpp stamp.cpp compfinder.cpp comphandler.cpp hyperengine.cpp subsumeimplicit.cpp cleaningstats.cpp datasync.cpp reducedb.cpp clausedumper.cpp bva.cpp intree.cpp features_calc.cpp features_to_reconf.cpp solvefeatures.cpp searchstats.cpp xorfinder.cpp cryptominisat4\GitSHA1.cpp /link

the main_simple.cpp compiles (in a 64 bit compile environment) and can be run without crashing.

[msoos]

Thanks! It's really strange that the stack is not enough. I am very-very surprised. No idea why. Thanks again, I'll looki nto these!

[capiman]

When my short analysis is correct, it comes from StreamBuffer (look for CHUNK_LIMIT in streambuffer.h), which is used in parse_DIMACS.

[capiman]

https://msdn.microsoft.com/en-us/library/tdkhxaks.aspx

"Without this option the stack size defaults to 1 MB."

which is too less for a CHUNK_LIMIT of 1048576 (bytes).

[msoos]

Wow, that was super-dumb of me. Such a rookie mistake. Fixed, thanks!

[a1880]

I am using the following global.h as forced include file to ease the MS VC++ port.

#ifndef GLOBAL_H_INCLUDED
#define GLOBAL_H_INCLUDED

//  definitions for VC++ port of Cryptominisat
//
//  Axel Kemper  03-Aug-2013
//               09-May-2014  update for Cryptominisat 4.0

//  avoid error C4996
#define _SCL_SECURE_NO_WARNINGS
#define _CRT_SECURE_NO_WARNINGS

#define NO_DRUP 1
#define NO_USE_ZLIB 1
#define USE_OPENMP 1
#define NO_USE_GAUSS 1
#define NO_STATS_NEEDED 1
#define NO_USE_MYSQL 1

#define HAVE_OPENMP 1

#define USE_M4RI 1

#pragma warning(disable : 4244)  //  C4244 : 'Argument': Konvertierung von 'const uint64_t' in 'double', möglicher Datenverlust
#pragma warning(disable : 4267)  //  C4267 : 'return': Konvertierung von 'size_t' nach 'uint32_t', Datenverlust möglich
#pragma warning(disable : 4302)  //  C4302 : truncation
#pragma warning(disable : 4311)  //  C4311 : pointer truncation
#pragma warning(disable : 4800)  //  C4800 : 'const uint32_t' : Variable wird auf booleschen Wert('True' oder 'False') gesetzt(Auswirkungen auf Leistungsverhalten möglich)
#pragma warning(disable : 4805)  //  C4805 : '==' : unsichere Kombination von Typ 'unsigned short' mit Typ 'bool' in einer Operation

typedef unsigned int  uint32_t;
typedef __int32  int32_t;

//  http://msdn.microsoft.com/en-us/library/vstudio/b0084kay.aspx
//  SSE2 is default for 64bit CPUs
#if !defined(__SSE2__) && defined(_M_X64)
#define __SSE2__ 1
#endif

#define __builtin_popcount(b)  __popcnt16(b)

//  ignore noexcept(true)
#define NO_NOEXCEPT 1

#if defined(__cplusplus)

#define or ||
#define and &&

#else
#  define inline __inline
#endif

#endif GLOBAL_H_INCLUDED

[msoos]

Ah, nice, thanks! I'll try to use it :)

BTW, I think the inline and the popcount can now be removed from there. Also, uint32_t should be there in #include <cstdint> under C++11. The rest is actually quite nice, thanks a lot, I'll try my best :)

[msoos]

So the only thing remaining based on this: https://ci.appveyor.com/project/msoos/cryptominisat is that the library is somehow placed at the wrong place. It is placed at

C:\projects\cryptominisat\cmsat4-src\Release\cryptominisat4.dll

but it is looked for here:

LINK : fatal error LNK1181: cannot open input file '..\lib\Release\cryptominisat4.lib' [C:\projects\cryptominisat\cmsat4-src\cryptominisat4_simple.vcxproj]

in other words, the "lib" is a bit of an extra there for no reason. I this this should be easy to fix :)

[capiman]

Can you tell, where the above files (temp_lib_norm.lib, temp_lib_ipasir.lib, cryptominisat4.lib) are placed on Linux? Is there some copy step from temp_lib_norm.lib to cryptominisat4.lib?

Is this done by the following code (taken from CMakeLists.txt)?

add_library(libcryptominisat4 SHARED ${cms_lib_objects_norm}) target_link_libraries(libcryptominisat4 LINK_PUBLIC ${cryptoms_lib_link_libs} )

... list(APPEND cms_lib_objects_norm $)

...

  add_library(temp_lib_norm OBJECT 
  ${cryptoms_lib_files} 
  cryptominisat.cpp 
  ) 

and

  set(cryptoms_lib_files 
  cnf.cpp 
  propengine.cpp 
  varreplacer.cpp 

... )

[msoos]

Sorry, I was on vacation. Thanks for that pointer, I'll look into that! Thanks a lot again,

Mate

[msoos]

Hey @capiman @a1880 could you please check out https://ci.appveyor.com/project/msoos/cryptominisat/build/1.0.73/artifacts

Does it work on your system? It probably needs Visual Studio 2015 Runtime (freely downloadable). On a related note, do you have any idea what flags I need to pass Visual Studio so it would compile such that the VS Runtime is not needed to be installed?

Thanks a lot in advance!

Mate

[a1880]

Hi Mate,

I have tried cryptominisat4_simple.exe on my Windows 7 64bit system.

It worked OK for the attached CNF file. I have Visual Studio 2015 on my system.

I was a bit shocked that the whole package is 55 megabyte big.

The executable alone is about half the size of my usual “full” cryptominisat4.5.3 compiles.

Looking at the .exe file with “Dependency Walker”, I get:

So, it is a 64-bit build which depends on the MS VC++ runtime.

To avoid the dependency, I am using the compile switch “/MT” (Runtime Library Multi-threaded).

Best greetings,

Axel

[a1880]

cannot upload my mail as pdf or zip to show the pictures. Sorry!

[msoos]

Yeah, I'm trying to do the /MT trick, I'm getting some issues. It'd be great if you could take a look a the logs. I also tried /WHOLEARCHIVE but I get internal linker error. I'd be really grateful if you could fix this You wouldn't need to compile CryptoMiniSat anymore :) Also, I've been integrating your option parser. I got very far, the ONLY issue I have right now is that it parser --a for the first long option that starts with "a" (e.g. --america or --anaconda). But there are more than one that start with "--a", so I need it to instead tell me that the command line is incorrect. Do you know how to do that? I pushed a new axelparser branch, it's not a continuation of your branch unfortunately, I messed up. If you could clone it and take a peek, that'd be awesome!

[msoos]

The issue I'm getting is:

[00:02:06]   C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\bin\x86_amd64\CL.exe /c /IC:\projects\cryptominisat /I"C:\projects\cryptominisat\cmsat4-src" /nologo /W1 /WX- /O2 /D WIN32 /D _WINDOWS /D EBUG /D NDEBUG /D _FORTIFY_SOURCE=0 /D USE_PTHREADS /D "CMAKE
[00:02:06] _INTDIR=\"Release\"" /D _MBCS /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Zc:inline /GR /Fo"cryptominisat4_simple.dir\Release\\" /Fd"cryptominisat4_simple.dir\Release\vc140.pdb" /Gd /TP /errorReport:queue  /Zc:inline C:\projects\cryptominisat\
[00:02:06] src\main_simple.cpp
[00:02:06]   main_simple.cpp
[00:02:08] Link:
[00:02:08]   C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\bin\x86_amd64\link.exe /ERRORREPORT:QUEUE /OUT:"C:\projects\cryptominisat\Release\cryptominisat4_simple.exe" /INCREMENTAL:NO /NOLOGO kernel32.lib user32.lib gdi32.lib winspool.lib shell32.lib ole32.l
[00:02:08] ib oleaut32.lib uuid.lib comdlg32.lib advapi32.lib ..\lib\Release\cryptominisat4.lib /MANIFEST /MANIFESTUAC:"level='asInvoker' uiAccess='false'" /manifest:embed /DEBUG /PDB:"C:/projects/cryptominisat/Release/cryptominisat4_simple.pdb" /SUBSYSTEM:CONSOLE /S
[00:02:08] TACK:"1572864" /TLBID:1 /DYNAMICBASE /NXCOMPAT /IMPLIB:"C:/projects/cryptominisat/lib/Release/cryptominisat4_simple.lib" /MACHINE:X64  /machine:x64 /PDBCOMPRESS /MT cryptominisat4_simple.dir\Release\main_simple.obj
[00:02:08] LINK : warning LNK4044: unrecognized option '/MT'; ignored [C:\projects\cryptominisat\cmsat4-src\cryptominisat4_simple.vcxproj]

So link.exe doesn't eat /MT. Dunno why. Also, does that executable run at all? If all it needs is the Visual Studio runtime, that's pretty darn good, no? At least nothing else is needed and it can be send to people? That'd be awesome for me!!

[capiman]

As far as I know /MT is for compiler, not linker. Also see here: http://stackoverflow.com/questions/1691395/how-to-statically-link-using-link-exe

[msoos]

Thanks, I read that already when I wrote that post, it doesn't work unfortunately. See below why.

Can you try to fix it? Here is how to build it on Windows:

cmake -DCMAKE_BUILD_TYPE=Release -G "Visual Studio 14 2015 Win64" -DSTATICCOMPILE=ON -DCMAKE_INSTALL_PREFIX=%P%
msbuild "INSTALL.vcxproj"

Please do that and then try to fix cmake so it compiles into a statically linked executable. Would be really nice! Plus it'd be nice for you as it would always alert me if the Windows build dies! :) No more having to create and issue, I'd know immediately :) And you could just download the static exe and won't even need to compile.

[capiman]

Got two problems (not reaching link step):

1) CompilerIdC.exe (intermediate file by cmake 3.5.1 and 3.5.2) is detected by my Microsoft virus scanner as https://www.microsoft.com/security/portal/threat/encyclopedia/entry.aspx?name=Trojan%3aWin32%2fMaltule.C!cl&threatid=2147709295&enterprise=0 but only during run of cmake. If I revert the file (from quarantaine) and scan it again, it seems to be clean. Also virustotal.com does not seems to detect a virus in this file. I assume it is a false positive...?

2) It seem to try to build something with SQL (Stats) and does not find a file "xxd": CustomBuild: Building Custom Rule C:/cryptominisat-20160606/cryptominisat/src/CMakeLists.txt CMake does not need to re-run because C:\cryptominisat-20160606\cryptominisat\cmsat4-src\CMakeFiles\generate.stamp is up-to-date. Generating sql_tablestructure.cpp Der Befehl "xxd" ist entweder falsch geschrieben oder konnte nicht gefunden werden. C:\Program Files (x86)\MSBuild\Microsoft.Cpp\v4.0\V140\Microsoft.CppCommon.targets(171,5): error MSB6006: "cmd.exe" wurde mit dem Code 9009 beendet. [C:\cryptominisat-20160606\cryptominisat\cmsat4-src\tablestruct.vcxproj] How can I disable stats? Or where to get xxd? What is it doing?

[msoos]

Have you had a look at the AppVeyor logs? Please take a look. It builds there, maybe you could try to debug? xxd is missing on windows, I might need to commit the generated code into github. I'll fix that. The viruscanner is very weird. CompilerIdC.exe I never generate so that's strange. That's probably generated by Visual C++. Can you please work a bit more on this and look into all of it? I have been trying to make your life easier with Appveyor but it feel as though nobody is interested to put real effort ( mean hours, days) into it, other than me :S

[capiman]

1) I reported the case yesterday to Microsoft as possible false alarm. Virus scanner signature was updated. Today Microsoft Defender remains silent when running cmake on a clean directory.

2) I created a dummy for xxd, error went away.

3) I think I fixed error message for "/MT" and "/DEBUG".

Compare modified section with original:

if(WIN32 AND NOT CYGWIN)
    set(DEF_INSTALL_CMAKE_DIR CMake)
#     add_compile_options($<$<CONFIG:Debug>:-DDEBUG>)
#     add_compile_options($<$<CONFIG:Debug>:/Od>)
#     add_compile_options($<$<CONFIG:Debug>:/Gm>)
    add_compile_options(/DEBUG)
    add_compile_options(/GS)
    add_compile_options(/W1)
    add_compile_options(/Zc:inline)
    add_compile_options(/fp:precise)
    add_compile_options(/EHsc)
    add_compile_options(/MT)

    # set(CMAKE_SHARED_LINKER_FLAGS "${CMAKE_SHARED_LINKER_FLAGS} ")
    set(CMAKE_SHARED_LINKER_FLAGS "${CMAKE_SHARED_LINKER_FLAGS} /INCREMENTAL:NO")
    set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} /PDBCOMPRESS")
    set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} /STACK:1572864")

    # RelWithDebInfo specific flags
    # set(CMAKE_SHARED_LINKER_FLAGS "${CMAKE_SHARED_LINKER_FLAGS} /DEBUG") # /OPT:REF /OPT:ICF
    # set(CMAKE_STATIC_LINKER_FLAGS "${CMAKE_STATIC_LINKER_FLAGS} /DEBUG")
    # set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} /DEBUG")
else()
  set(DEF_INSTALL_CMAKE_DIR lib/cmake/cryptominisat4)
endif()

4) I am not sure if this fixes the static link problem. @a1880 Perhaps Axel, can you have a look again with Dependancy Walker, once Mate has intregrated the change?

[msoos]

Wow, great work Martin, thanks for reporting it to MS, that was good job! Also, thanks for that fixed CMakeLists, I just pushed it. I will try to do something with XXD. We are making a lot of progress :) Thanks again!

[a1880]

Today (13-Jun-2016), I have checked the latest cryptominisat4_simple.exe executable produced by AppVeyor. The executable is compiled for 64-bit and does not depend on MS VC++ runtime libraries.

[msoos]

Wow, thanks! That's really cool!

[a1880]

The executable runs quite fast compared to my elder 4.5.3 compiles. It is a pitty, but I can't currently spare the time to fix the ak_program_options to get a non-simple version. I noticed that this version is much faster in multi-threaded mode compared to single threaded. Might be due to different default parameters.

[msoos]

Thanks! No worries, I'll try fixing it up. Thanks for all the hard work both of you!

Mate