This distribution of Vampire 4.2.2 prerelease has been compiled from the
sources obtained from https://github.com/vprover/vampire/.

    $ unzip master.zip
    $ cd vampire-master
    $ make vampire_rel

Vampire can be freely used for noncommercial use. See "LICENCE" for details.

For Linux and macOS, repository version master 3893 (May 2018) was used. For
Windows, repository version master 3984 (June 2018) was used, including a
Windows-specific bug fix (thanks to Martin Suda).

The Linux executable was built on a 64-bit installation of Ubuntu 12.04.5 LTS
running in VirtualBox. The Mac executable was built on a 64-bit macOS 10.10
machine called "macbroy31". The Windows executable was built on a 64-bit
Windows Server 2012 machine called "vmnipkow9", using Cygwin64. All the
executables were "strip"ped. The executables were renamed from "vampire_rel_*"
to "vampire".

On Linux, it was necessary to change the "CXX" and "CC" variables to

    CXX = g++-4.8
    CC = gcc-4.8

and to remove the "-Wno-terminate" option in "CXXFLAGS". Moreover, we needed
to add

    #include <signal.h>

in "CASC/ScheduleExecutor.cpp".

On Windows/Cygwin, a few kludges were necessary to resolve compilation errors.
In "Lib/Sys/Multiprocessing.cpp", we added

    enum {
      DT_DIR = 4,
      DT_REG = 8
    };

In "Lib/System.cpp", we added

    extern "C" int kill(pid_t, int);

And in "Lib/Timer.cpp", we added

    #undef UNIX_USE_SIGALRM

See also https://github.com/vprover/vampire/issues/52/.

As a result of the change to "Lib/Timer.cpp", the Windows version of Vampire
does not support time slicing. This is reflected in the default value for the
"$VAMPIRE_EXTRA_OPTIONS" variable in "etc/settings". This situation is not
ideal, but since Isabelle performs its own time slicing, it is acceptable.


Enjoy!


        Jasmin Blanchette
        12 June 2018
