THE LEO-II System Installation Guide
(Christoph Benzmueller and Nik Sultana)


NOTES:
  * LEO-II runs under OCaml
  * It follows the TPTP ATP System Building Conventions
     ( http://www.cs.miami.edu/~tptp/TPTP/Proposals/SystemBuild.html )


LEO-II Installation Instructions:
 (1) Choose an [installation-directory], e.g. /home/chris/
 (2) Download latest LEO-II version from
         http://www.leoprover.org
     and store it in [installation-directory]
 (3) Change to the installation directory
                   cd [installation-directory]
 (4) Extract the files of the packages
                   tar xzf leo2-v***.tgz
 (5) Change to the main source directory of the LEO-II package
                   cd [installation-directory]/leo2/src

 (6) Run the configuration script -- running "./configure --help" will
     describe the options available.

 (7) Build a LEO-II executable -- there are different alternatives and
     each of them should work:
             - "make" will build an OCaml-bytecode version of LEO-II
             - "make opt" will build a native version of LEO-II
             - "make clean" removes generated binaries

     You can obtain a faster-performing binary by sacrificing
     helpful error messages. For this, use "make opt debug=false".

     To build LEO-II you need to have the ocamlfind utility.
     Furthermore, building MiniSAT (which is included in the
     distribution of LEO-II) requires a C++ compiler.

     What used to be camlp4 macros are now the values in the generated
     file src/general/build_config.ml, which "make" writes from the
     variables at the top of the Makefile.  Nothing preprocesses the
     sources any more.

     Running these commands will create an executable
                  [installation-directory]/leo2/bin/leo

 (7) Try the following in case of errors during build
       - If you have multiple versions of OCaml in your PATH, you
         can specify which version to use via the --ocamlbindir parameter
         to the configure script.


Enabling the cooperation of LEO-II with at least one First-Order Prover:
- LEO-II is designed to cooperate with first-order provers. Thus installation
  of a first order prover is crucial in order to run LEO-II. While LEO-II
  can cooperate with different first-order provers, we recommend here to
  install the 'The E Equational Theorem Prover' which is available at
  https://github.com/eprover/eprover

- In the following we assume that the binary for running prover E is available
  in file
                   [eprover-directory]/eprover
- In order to inform LEO-II where it can find this binary for E you need to
  provide a file
                   [your-homedirectory]/.leoatprc
  containing the following entries:
                   e = [eprover-directory]/eprover
		   epclextract = [eprover-directory]/epclextract

  The epclextract entry is needed only for "--proofoutput 2", which reports
  what the first-order prover contributed.  Without it that option has
  nothing to call.  Everything else works with the e entry alone, and
  "--atp e=[eprover-directory]/eprover" on the command line does instead of
  the file.

Running LEO-II in Automatic Mode:
- To start LEO-II you need to type:
                  [installation-directory]/leo2/bin/leo
- Parameters are given in the following sequence:
                  [installation-directory]/leo2/bin/leo [OPTIONS] [FILE]
  In order to see which options can be set, run
                  [installation-directory]/leo2/bin/leo --help
- Two examples are in [installation-directory]/leo2/examples.  Both are
  proved in well under a second:
   [installation-directory]/leo2/bin/leo [installation-directory]/leo2/examples/extensionality.p --proofoutput 1
   [installation-directory]/leo2/bin/leo [installation-directory]/leo2/examples/sets.p

   A whole directory at once, each problem with its own time limit.  This
   writes a summary table into the directory, so it needs write permission
   there:
   [installation-directory]/leo2/bin/leo -d [installation-directory]/leo2/examples -f e -t 40

   At CASC LEO-II is called as follows:
   [installation-directory]/leo2/bin/leo --timeout 30 --proofoutput 1 --foatp e \
     --atp e=[e-directory]/eprover '[problem-file-directory/SET014^4.tptp'


Running several settings at once:
- "--cores N" runs N settings side by side and answers with the first that
  settles the problem.  The default is one core, at which nothing runs in
  parallel and the search is exactly what it has always been.

Running LEO-II in Interactive Mode is not currently recommended due to several open issues.
