src/HOL/TPTP/CASC/ReadMe

isabelle process -T THEORY;

Notes from Geoff:

I added a few lines to the top of bin/isabelle ...

   ## Geoff makes Isabelle a robust tool, because he's kind
   function cleanup {
       rm -rf $HOME
   }
   if [ -z ${HOME+x} ]; then
       HOME="/tmp/Isabelle_$$"
       trap cleanup EXIT
   fi

... which you might like to adopt. Now it works on SystemOnTPTP.


Notes to Geoff:

  Once you have open the archive, Isabelle and its tool are ready to go. The
  various tools are invoked as follows (given a file name %s):

  	Isabelle, competition version:
  		STAREXEC_WALLCLOCK_LIMIT=300 ./bin/starexec_run_isabelle %s

  	Isabelle, demo version:
  		STAREXEC_WALLCLOCK_LIMIT=300 ./bin/starexec_run_isabelle_hot %s

  	Nitpick (formerly also called Nitrox):
  		STAREXEC_WALLCLOCK_LIMIT=300 ./bin/starexec_run_nitpick %s

  	Refute:
  		STAREXEC_WALLCLOCK_LIMIT=300 ./bin/starexec_run_refute %s

  Here's an example:

		STAREXEC_WALLCLOCK_LIMIT=300 ./bin/starexec_run_isabelle $TPTP/Problems/SET/SET014^4.p

  The output should look as follows:

    running nitpick for 7 s
    FAILURE: nitpick
    running simp for 15 s
    SUCCESS: simp
    % SZS status Theorem

  Additional sanity tests:

		STAREXEC_WALLCLOCK_LIMIT=300 ./bin/starexec_run_isabelle_hot $TPTP/Problems/CSR/CSR150^3.p
		STAREXEC_WALLCLOCK_LIMIT=300 ./bin/starexec_run_isabelle_hot $TPTP/Problems/SYO/SYO304^5.p

  The first problem is unprovable; the second one is proved by Satallax.

  All the tools accept CNF, FOF, TFF0, or THF0 problems and output SZS
  statuses of the form

  	% SZS status XXX

  where XXX is in the set

    {Unknown, TimedOut, Unsatisfiable, Theorem, Satisfiable, CounterSatisfiable}

  Nitpick also output a model within "% SZS begin" and "% SZS end" tags, in
  its idiosyncratic syntax.

  In 2011, there were some problems with Java (needed for Nitpick), because it
  required so much memory at startup. I doubt there will be any problems this
  year, because Isabelle now includes its own version of Java, but the solution
  back then was to replace

  	exec isabelle java

  in the last line of the "contrib/kodkodi-1.5.2/bin/kodkodi" script with

  	/usr/lib64/jvm/java-1.5.0-gcj-4.5-1.5.0.0/jre/bin/java

  See the emails we exchanged on 18 July 2011, with the subject "No problem on
  my Linux 64-bit".

  Enjoy!


Notes to myself:

  I downloaded the official Isabelle2015 Linux package from

    http://isabelle.in.tum.de/dist/Isabelle2015_linux.tar.gz

  on "macbroy21" and renamed the directory "Isabelle2015-CASC". I modified

    src/HOL/TPTP/atp_problem_import.ML

  to include changes backported from the development version of Isabelle. I
  then built a "HOL-TPTP" image:

    ./bin/isabelle build -b HOL-TPTP

  I copied the heaps over to "./heaps":

    mv ~/.isabelle/Isabelle2015/heaps .

  I created some wrapper scripts in "./bin":

    starexec_run_default
    starexec_run_isabelle
    starexec_run_isabelle_hot
    starexec_run_nitpick
    starexec_run_refute

  I tested the "SET014^4" problem mentioned above.

  Next, I installed and enabled ATPs.

  LEO-II (1.6.2):

    I logged to a 32-bit Linux ("lxlabbroy") machine. I retrieved LEO-II from

      http://page.mi.fu-berlin.de/cbenzmueller/leo/leo2_v1.6.2.tgz

    I did "make opt". I copied "bin/leo.opt" to
    "~/Isabelle2015-CASC/contrib/leo".

    I added this line to "etc/settings":

      LEO2_HOME=$ISABELLE_HOME/contrib

  Satallax (2.7):

    I logged to a 32-bit Linux ("lxlabbroy") machine. I retrieved Satallax from

      http://www.ps.uni-saarland.de/~cebrown/satallax/downloads/satallax-2.7.tar.gz

    I added E to the path so that it gets detected by Satallax's configure
    script:

      export PATH=$PATH:~/Isabelle2013-CASC/contrib/e-1.6-2/x86-linux

    I followed the instructions in "satallax-2.7/INSTALL". I copied
    "bin/satallax.opt" to "~/Isabelle2013-CASC/contrib/satallax".

    I added this line to "etc/settings":

      SATALLAX_HOME=$ISABELLE_HOME/contrib

  Vampire (2.6):

    I copied the file "vampire", which I probably got from the 2013 CASC
    archive and moved it to "~/Isabelle2013-CASC/contrib/vampire".

    I added these lines to "etc/settings":

      VAMPIRE_HOME=$ISABELLE_HOME/contrib
      VAMPIRE_VERSION=3.0

  Z3 TPTP (4.3.2.0 postrelease):

    I cloned out the git repository:

      git clone https://git01.codeplex.com/z3

    I build Z3 and from "build", ran "make examples" to build "z3_tptp".
    I copied "z3_tptp" as "z3_tptp-solver" and "libz3.so" to "./contrib",
    and put a wrapper called "z3_tptp" to set the library path correctly
    (inspired by the CVC4 setup on Mac OS X).

    I added this line to "etc/settings":

      Z3_TPTP_HOME=$ISABELLE_HOME/contrib

    Unfortunately, I got "z3::exception" errors. I did not investigate this
    further and commented out the environment variable in "etc/settings".

  To test that the examples actually worked, I create a file called
  "/tmp/T.thy" with the following content:

    theory T imports Main begin
    lemma "a = b ==> [b] = [a]"
    sledgehammer [cvc4 e leo2 satallax spass vampire z3 z3_tptp] ()
    oops
    end

  Then I ran

    ./bin/isabelle process -T /tmp/T

  I also performed the aforementioned sanity tests.

  Finally, I renamed "README" to "README.orig" and copied this "ReadMe" over.

  Ideas for a future year:

    * Unfold definitions, esp. if it makes the problem more first-order (cf.
      "SEU466^1").
    * Detect and remove needless definitions.

  That's it.


                Jasmin Blanchette
                10 June 2015