How to Build & Run Vampire ATP in Cygwin

Vampire is an Automated Theorem Prover.  It was apparently developed on Linux, but it can be run on Windows using Cygwin, which provides the build tools, software packages and operating system services that Vampire depends on.  Here are some instructions for building and running Vampire in 64-bit Windows 10.  A note on building Vampire with Cygwin can be found on Vampire's GitHub page, here.

Install Cygwin:

1. Install Cygwin and its default packages.
2. Install these Cygwin packages:
   
   • cygrunsrv
   • gcc-core
   • gcc-g++
   • make
   • zlib
   • zlib-devel
   • zlib-devel
   • zlib0
3. Move C:\cygwin64\bin to the front of the %PATH% environment variable.

Install Git Command-Line Tools

1. Install the Git command-line tools.  An installer can be downloaded from https://git-scm.com/download/win.

Install the Z3 Theorem Prover

1. Download a Win64 release of Z3 from https://github.com/Z3Prover/z3/releases.
2. Make z3.dll available from PATH, either by putting z3.dll from this release in some folder that is in PATH, or by adding the Z3 "bin" folder to PATH.

Build Vampire

1. Pull Vampire's Git repository from GitHub (https://github.com/vprover/vampire).
2. In Vampire's Makefile, add "-D_GNU_SOURCE" to CXXFLAGS and CCFLAGS.
3. Change all instances of "exit(0);" in the source code to "_Exit(0);".  This is needed to prevent the child processes forked by the main Vampire process from calling the main process' atexit handlers.
4. Create a folder named "include" in the Vampire repository's main folder.
5. Copy the contents of the Z3 "bin" folder to that "include" folder.
6. Compile and link vampire by issuing the command "make vampire_z3_rel" from a command prompt.

Start the Cygwin Windows Service

1. Start Cygwin's bash shell.
2. From the bash command prompt, issue the command "cygserver-config" to configure the Cygwin Windows service.
3. In Windows, right-click "This PC", select "Manage", then select "Services and Applications, then select "Services", then start the "CYGWIN cygserver" service.

 Run Vampire

1. Run Vampire from a command prompt.  For example:
   vampire_z3_rel_master_4055 --mode casc -t 300 "Problems\SET\SET159-6.p"
2. Vampire may not succeed in deleting the semaphores that it creates in the Cygwin server.  To delete them, issue the command "ipcs -s | grep '^s\\s' | cut -d' ' -f3|xargs -n 1 ipcrm -s" from a command prompt.  Alternatively, add a call to system() at the end of Vampire's main function that issues this command.