Cannot build Vampire v4.6 on Windows / Cygwin

[makarius]

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.)

[quicquid]

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?

[mdesharnais]

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.

[makarius]

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:

• https://isabelle-dev.sketis.net/rISABELLEd4c2a9191cd1
• https://isabelle.sketis.net/components/vampire-4.6.tar.gz

[mdesharnais]

My tests are completed. I can confirm that there is no regression in the average success rate between 4.5.1 and 4.6.

[MichaelRawson]

Looks like this is fixed with #283 - thanks all!

[ghost]

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.

[quickbeam123]

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?