Skip to content
Michael Rawson edited this page Jan 25, 2025 · 2 revisions

The following is a series of "user experience" reports about using Vampire under Cygwin. It is worth noting that since #540 Vampire no longer uses UNIX semaphores and therefore the cygrunsrv mentioned at times below should not be necessary.

2025 update (thanks to Yves Marcoux)

Yves Marcoux, EBSI, Université de Montréal 2025-01-23

I just succeeded in installing Vampire (without Z3) on Windows and thought documenting the process might be useful to others. So here are (with little prose) the steps I took. The main idea is using Cygwin (unlike others, I am using the 64 bit Cygwin). I use Windows 10, but see no reason why this would not work on Windows 11.

Download Vampire:

  • Download Vampire 4.9 (v4.9casc2024), or the current version, compressed sources from GitHub. Also available as tar.gz.
  • Make sure the file is unblocked: Right-click on the file → Properties → Unblock → Apply.
  • Uncompress the file in the directory (folder) of your choice, here I use D:\ProgMesProg\vampire.
  • Create the subdirectory D:\ProgMesProg\vampire\CMAKE-build.

Install Cygwin + needed packages:

  • Download the Cygwin setup program (this is the version for 64-bit Windows). The setup program is used for both an initial basic install and for installing optional packages.
  • Run the setup program for the first time:
    • Select Install from Internet.
    • C:\cygwin64 is proposed as the root install directory. I changed it to D:\cygwin64.
    • Select Install for all users.
    • I chose "Use system proxy settings" as an Internet connection.
    • Choose a download site near you.
    • Accept the suggested minimal base packages.
    • Click Next as many times as necessary.
    • In the last dialog, I chose to install the proposed icons (Desktop and Start Menu). Click Finish.
  • Run again the setup program, this time, select the (latest versions of) the following three packages: cmake, gcc-c++, make.
  • Those three packages depend on others, which will automatically be installed as well.
  • After the installs, the root install directory weighs around 823 MB.

Compile Vampire

I don’t know if it is because of a bug in the code, but you will first need to add three lines to the file D:\ProgMesProg\vampire\CMakeLists.txt. Otherwise, you will get fatal errors from the linker, because of multiple definitions of some symbols (around 72 symbols defined in both "D:\ProgMesProg\vampire\Lib\Environment.cpp" and "D:\ProgMesProg\vampire\Shell\Options.cpp"; can somebody investigate, please?)

  • In file D:\ProgMesProg\vampire\CMakeLists.txt, around line 10 (after the includes), add the following three lines: set(CMAKE_MODULE_LINKER_FLAGS -Wl,--allow-multiple-definition) set(CMAKE_EXE_LINKER_FLAGS -Wl,--allow-multiple-definition) set(CMAKE_STATIC_LINKER_FLAGS -Wl,--allow-multiple-definition) It is possible that only one of those lines is actually necessary, but it works with all three. Save the file.
  • Open a Cygwin64 Terminal (if you did as I did, you have an icon on your desktop).
  • cd "D:\ProgMesProg\vampire\CMAKE-build"
  • cmake .. (don’t forget the dots!) This is rather quick. You will get around 15 messages, some of them sounding alarming (like Could NOT find Z3 or fatal: not a git repository), but you can just ignore them.
  • make This is rather long (at least the first time), over 40 minutes on my machine. It compiles all of the source files, then links everything into an executable program. You get a lot of messages; at least one per source file, and a fair number of warnings, that you can just ignore.

The D:\ProgMesProg\vampire\CMAKE-build\bin\vampire_rel.exe file is created. This is the Vampire executable, which needs to be run in Cygwin.

Running Vampire

  • Open a Cygwin64 Terminal (again, if you did as I did, you have an icon on your desktop).
  • cd "D:\ProgMesProg\vampire\CMAKE-build\bin"
  • ./vampire_rel.exe --show_options on

The last command line is the one that runs Vampire. The .exe can be dropped. Use command line options and arguments appropriately to direct Vampire to do what you want. For example, if you have a problem in a file problem.fof in the same directory as the executable, you can use the command:

./vampire_rel problem.fof

to have Vampire work on it.

The executable can be relocated to any other directory.

2022 update (thanks to Boris Shminke)

Here is the more or less complete list of steps to build and run Vampire in a CASC mode on Cygwin:

  • installed Cygwin packages: gcc-core, gcc-g++, make, cmake, python3 (needed only for Z3), cygrunsrv (needed only run Vampire with semaphores)
  • run Cygwin as administrator and run /usr/bin/cygserver-config (for more details see https://www.cygwin.com/cygwin-ug-net/using-cygserver.html)
  • then run Cygwin normally for the following steps
  • build Z3
  • build Vampire with Z3
  • run Vampire with --mode casc