The TPTP ATP System Building Conventions

by Geoff Sutcliffe and Stephan Schulz and Nik Sultana

Motivation

Over the years of supporting ATP system development (the TSTP, SystemOnTPTP, CASC, etc.), I've spent many hours compiling and installing ATP systems, and some of the build processes are attriciously complex. This proposal aims to set conventions that will make it easy to build ATP systems, which if adopted will make life much better for ATP users. Commonly adopted conventions will allow users to follow the same pattern of activities when installing multiple ATP systems.

Directory Layout

The system must unpack into a single directory named after the system and the system version. The suggested format is the system name written in the normal camel-case that would be used in a publication, followed by three hyphens and then the version number, e.g., Vampire---2.6, iProver---0.99. This format allows for easy extraction of the two components (because only a crazy person would have three hyphens as part of their system name or version number).

Build Commands

The build sequence is one used by many open source software packages.

./configure <options>
make
make install

configure configures the system to run on the current platform. This includes specifying where the executables, library files, and man pages (if any) will be installed, and provide system specific build parameters. The minimal <option>s that must be supported are:
- --help : Print this help.
- --bindir=<path> : Specify the directory for executables.
- --libdir=<path> : Specify the directory for library files that are needed for execution.
- --exec-prefix=<path> : Equivalent to --bindir=<path>/bin --libdir=<path>/lib.
- --mandir=<path> : Specify directory for the man pages.
- --prefix=<path> : Equivalent to --bindir=<path>/bin --libdir=<path>/lib --mandir=<path>/man.
The default is equivalent to --prefix=/usr/local
Many ATP systems rely on the use of other ATP systems as external subsystems, e.g., some instantiation-based systems use an external propositional system, and some higher order systems delegate subproblems to first-order subsystems. Other ATP systems rely on other external software, e.g., some systems need to know the location of a Prolog interpreter. It is generally preferable to specify the location of such external software at run time, as command line parameters. If the location of external software (executables, etc.) has to be known at build time, it is recommended that the location be specified by configure options of the form:
- --use-<software>=<path>
e.g., --use-eprover=/usr/local/bin/eprover, or --use-prolog=/usr/bin/swipl. In contrast, the use of resource files in home directories, environment variables, and other approaches that have a global impact on a user account, are discouraged.
make performs the build. This typically invokes a compiler, etc., but could even be a no-op for interpreted systems.
make install moves the executables, library files, and man pages into the specified directories. If these directories are not owned by the user, it may be necessary to execute this step as the superuser.