I'am trying to use Cygwin to generate binaries of Vampire 4.6 in Windows 10

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

Originally posted by @jiplucap in #282 (comment)

[makarius]

The Isabelle component for vampire-4.6 should work as regular Windows executable, but you need to ensure that certain Cygwin DLLs are present. One way is to run it from a Cygwin terminal; you can then also figure out which DLLs are required:

ldd vampire.exe 
	ntdll.dll => /cygdrive/c/Windows/SYSTEM32/ntdll.dll (0x7ffd49c90000)
	KERNEL32.DLL => /cygdrive/c/Windows/system32/KERNEL32.DLL (0x7ffd49b50000)
	KERNELBASE.dll => /cygdrive/c/Windows/system32/KERNELBASE.dll (0x7ffd46f90000)
	cygwin1.dll => /usr/bin/cygwin1.dll (0x180040000)
	cyggcc_s-seh-1.dll => /usr/bin/cyggcc_s-seh-1.dll (0x50caa0000)
	cygstdc++-6.dll => /usr/bin/cygstdc++-6.dll (0x5f9b80000)

For example, you could copy the DLLs into the directory where vampire.exe resides, and distribute the whole thing as "Windows executable".

The build process for vampire.exe on Cygwin works as on Linux, but you need a version of vampire where this actually works. Official vampire-4.6 this requires the subsequent patch (from the README of the Isabelle component):

--- vampire-4.6/CMakeLists.txt~	2021-10-04 15:54:14.000000000 +0200
+++ vampire-4.6/CMakeLists.txt	2021-10-06 20:30:52.258940100 +0200
@@ -863,6 +863,10 @@
   add_compile_definitions(VDEBUG=0)
 endif()
 
+if (CYGWIN)
+ add_compile_definitions(_BSD_SOURCE)
+endif()
+                    
 # configure warning flags
 if(CMAKE_CXX_COMPILER_ID STREQUAL GNU OR CMAKE_CXX_COMPILER_ID MATCHES Clang$)
   add_compile_options(-Wall)

Afterwards it is a perfectly normal build:

    cmake -G "Unix Makefiles" .
    make

[ghost]

Thank you very much.
I have placed the dlls as you said and the .exe works.
However, I must say that though the command "vampire --show_options on" (https://vprover.github.io/usage.html) works perfectly, then some options are not valid, for example:

vampire --mode casc -t 300 peaceful.p
System fail: Cannot create semaphore. error 88: Function not implemented

[makarius]

I can reproduce it with the Isabelle Cygwin compilation, while Linux works.
Maybe this is a genuine limitation on the Windows platform; or maybe just accidental for version 4.6.
Some Vampire expert is required here, but I am not in this category.

[selig]

It is known that a Windows executable cannot be run in portfolio mode due to the way we fork and use alarms for running different schedules. Sledgehammer doesn't use portfolio mode so this isn't an issue there but is generally annoying.

I've never touched Cygwin. @quickbeam123 has done in the past. Nobody is currently looking at the issue AFAIK but it would be great to fix.

There was a relevant discussion here: #283

[ghost]

I knew this discussion #283 but, as selig points out, I wished that some fix would allow to have standard vampire binaries for Windows users.

[makarius]

Standard Windows binaries can mean various things

• Cygwin as imitation of Linux, with minor drawbacks (often done in Isabelle)
• MingGW as approximation of Windows, with other minor drawbacks (sometimes done in Isabelle)
• Windows Services for Linux with original Linux binaries (not yet tried in Isabelle)

All these variations will have some shortcomings. How well it works depends on both developers and users taking the problem seriously.

[ghost]

Thank you, Makarius. I think that an invariant drawback in Cygwin and MingGW is the semaphore/alarm problem. The third solution WSL is nowadyas quite unlikely to be easily adopted by most Windows users.

[quickbeam123]

Actually, it's apparently still relatively easy to compile Vampire under Cygwin and have it run in portfolio mode.

Boris Shminke spent some time to figure it out for us and put the recipe up on our local (usually overlooked) wiki:

https://github.com/vprover/vampire/wiki/Vampire-under-Cygwin:-a-2022-update-(big-thanks-to-Boris-Shminke)

[MichaelRawson]

An update: I think the major blocker for Vampire working on other platforms (including Windows) is reliance on semaphores, and to a lesser degree signals. I'm slowly trying to phase these out, but in the meantime it seems that Cygwin works for everything except portfolio modes - portfolio modes apparently work with some kind of server, according to Boris Shminke in the wiki page.

Wiki page has moved to Cygwin.

Closing as this isn't an open bug in the usual sense, but a long-term project we're aware of and actively trying to fix.

[MichaelRawson]

I've added a note in the README to help future intrepid Windows voyagers. Closing in favour of #462.