Cannot build Vampire v4.6 on Windows / Cygwin
makarius opened this issue · 7 comments
I am trying to build the official release v4.6 for the forthcoming Isabelle release (deadline Nov/Dec 2021), see also #273
The normal "cmake . && make" procedure fails on Windows, with Cygwin bash and compiler tools:
[ 0%] Building CXX object CMakeFiles/obj.dir/Debug/Assertion.cpp.o
[ 0%] Building CXX object CMakeFiles/obj.dir/Debug/RuntimeStatistics.cpp.o
[ 1%] Building CXX object CMakeFiles/obj.dir/Debug/Tracer.cpp.o
[ 1%] Building CXX object CMakeFiles/obj.dir/Lib/Allocator.cpp.o
[ 1%] Building CXX object CMakeFiles/obj.dir/Lib/DHMap.cpp.o
[ 2%] Building CXX object CMakeFiles/obj.dir/Lib/Environment.cpp.o
[ 2%] Building CXX object CMakeFiles/obj.dir/Lib/Event.cpp.o
[ 3%] Building CXX object CMakeFiles/obj.dir/Lib/Exception.cpp.o
[ 3%] Building CXX object CMakeFiles/obj.dir/Lib/Hash.cpp.o
[ 3%] Building CXX object CMakeFiles/obj.dir/Lib/Int.cpp.o
[ 4%] Building CXX object CMakeFiles/obj.dir/Lib/IntNameTable.cpp.o
[ 4%] Building CXX object CMakeFiles/obj.dir/Lib/IntUnionFind.cpp.o
[ 5%] Building CXX object CMakeFiles/obj.dir/Lib/MemoryLeak.cpp.o
[ 5%] Building CXX object CMakeFiles/obj.dir/Lib/MultiCounter.cpp.o
[ 5%] Building CXX object CMakeFiles/obj.dir/Lib/NameArray.cpp.o
[ 6%] Building CXX object CMakeFiles/obj.dir/Lib/Random.cpp.o
[ 6%] Building CXX object CMakeFiles/obj.dir/Lib/StringUtils.cpp.o
[ 7%] Building CXX object CMakeFiles/obj.dir/Lib/System.cpp.o
/home/wenzelm/tmp/isadist/vampire-4.6/Lib/System.cpp: In static member function ‘static void Lib::System::readDir(Lib::vstring, Lib::Stack<std::basic_string<char, std::char_traits<char>, Lib::STLAllocator<char> > >&)’:
/home/wenzelm/tmp/isadist/vampire-4.6/Lib/System.cpp:454:14: error: ‘DT_REG’ was not declared in this scope
454 | case DT_REG:
| ^~~~~~
/home/wenzelm/tmp/isadist/vampire-4.6/Lib/System.cpp:457:14: error: ‘DT_DIR’ was not declared in this scope
457 | case DT_DIR:
| ^~~~~~
make[2]: *** [CMakeFiles/obj.dir/build.make:314: CMakeFiles/obj.dir/Lib/System.cpp.o] Error 1
make[1]: *** [CMakeFiles/Makefile2:111: CMakeFiles/obj.dir/all] Error 2
make: *** [Makefile:91: all] Error 2
We do need a Windows executable for Isabelle, and usually use Cygwin. (An alternative is MinGW, but not tried here.)
Hi Makarius, we just created a bugfix in the fix-cygwin branch. Could you try if that one works on your machine and if the performance within Sledgehammer is comparable to earlier versions you used?
I have some tests comparing Sledgehammer's success rate using Vampire 4.5.1 and 4.6 in different configurations running. They should complete within a few hours.
Hi Makarius, we just created a bugfix in the fix-cygwin branch. Could you try if that one works on your machine [...]?
Yes, this minimal change is fine. I have applied it to official v4.6 and produced the following multi-platform Isabelle component:
My tests are completed. I can confirm that there is no regression in the average success rate between 4.5.1 and 4.6.
Looks like this is fixed with #283 - thanks all!
I guess that the Vampire component for Isabelle https://isabelle.sketis.net/components/vampire-4.6.tar.gz cannot be used as a Windows standard release of Vampire 4.6,, but it is built to be called just from Isabelle Sledgehammer with its own parameters fixed. Am I right?
I'am trying to use Cygwin to generate binaries of Vampire 4.6 in Windows 10, but all my attemps have failed. I would be very grateful if someone would published the step-by-step proccess to do that in Windows. I would be even more grateful if someone could made available a binary release for Windows.
Dear @jiplucap, unfortunately, none of us has access to a windows machine, so any windows support is extremely hard for us.
Couldn't the "Linux Bash Shell" feature help here?