src/HOL/TPTP/CASC/ReadMe

imported patch up_casc

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_TOOL" 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 -e 'use_thy "/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