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 -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