--- a/src/HOL/TPTP/CASC/ReadMe Mon Jul 13 14:40:16 2015 +0200
+++ b/src/HOL/TPTP/CASC/ReadMe Mon Jul 13 16:54:27 2015 +0200
@@ -1,31 +1,42 @@
-Isabelle/HOL 2013 at CASC-24
+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:
+ various tools are invoked as follows (given a file name %s):
- Isabelle, competition version:
- ./bin/isabelle tptp_isabelle %d %s
+ Isabelle, competition version:
+ STAREXEC_WALLCLOCK_LIMIT=300 ./bin/starexec_run_isabelle %s
- Isabelle, demo version:
- ./bin/isabelle tptp_isabelle_hot %d %s
+ Isabelle, demo version:
+ STAREXEC_WALLCLOCK_LIMIT=300 ./bin/starexec_run_isabelle_hot %s
- Nitpick and Nitrox:
- ./bin/isabelle tptp_nitpick %d %s
+ Nitpick (formerly also called Nitrox):
+ STAREXEC_WALLCLOCK_LIMIT=300 ./bin/starexec_run_nitpick %s
- Refute:
- ./bin/isabelle tptp_refute %d %s
+ Refute:
+ STAREXEC_WALLCLOCK_LIMIT=300 ./bin/starexec_run_refute %s
Here's an example:
- ./bin/isabelle tptp_isabelle_hot 300 $TPTP/Problems/SET/SET014^4.p
+ STAREXEC_WALLCLOCK_LIMIT=300 ./bin/starexec_run_isabelle $TPTP/Problems/SET/SET014^4.p
The output should look as follows:
- > val it = (): unit
- val commit = fn: unit -> bool
- Loading theory "Scratch_tptp_isabelle_hot_29414_2568"
running nitpick for 7 s
FAILURE: nitpick
running simp for 15 s
@@ -34,37 +45,35 @@
Additional sanity tests:
- ./bin/isabelle tptp_isabelle_hot 300 $TPTP/Problems/CSR/CSR150^3.p
- ./bin/isabelle tptp_isabelle_hot 300 $TPTP/Problems/SYO/SYO304^5.p
- ./bin/isabelle tptp_isabelle_hot 300 $TPTP/Problems/PUZ/PUZ087^1.p
+ 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.
- The first problem is unprovable; the second one is proved by Satallax; the
- third one is proved by LEO-II.
+ All the tools accept CNF, FOF, TFF0, or THF0 problems and output SZS
+ statuses of the form
- All the tools accept CNF, FOF, TFF0, or THF0 problems and output SZS statuses
- of the form
-
- % SZS status XXX
+ % SZS status XXX
where XXX is in the set
{Unknown, TimedOut, Unsatisfiable, Theorem, Satisfiable, CounterSatisfiable}
- Nitpick and Nitrox also output a model within "% SZS begin" and "% SZS end"
- tags.
+ 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
+ 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
+ /usr/lib64/jvm/java-1.5.0-gcj-4.5-1.5.0.0/jre/bin/java
- See the emails we exchanged on July 18, 2011, with the subject "No problem on
+ See the emails we exchanged on 18 July 2011, with the subject "No problem on
my Linux 64-bit".
Enjoy!
@@ -72,39 +81,43 @@
Notes to myself:
- I downloaded the official Isabelle2013 Linux package from
+ I downloaded the official Isabelle2015 Linux package from
+
+ http://isabelle.in.tum.de/dist/Isabelle2015_linux.tar.gz
- http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2013_linux.tar.gz
+ on "macbroy21" and renamed the directory "Isabelle2015-CASC". I modified
- on a "macbroy" machine and renamed the directory "Isabelle2013-CASC". I built
- a "HOL-TPTP" image:
+ 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/Isabelle2013/heaps .
+ mv ~/.isabelle/Isabelle2015/heaps .
- To use this image and suppress some scary output, I added
-
- HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val it = (): unit"
+ I created some wrapper scripts in "./bin":
- to the next-to-last lines of "src/HOL/TPTP/lib/Tools/tptp_[inrs]*".
+ starexec_run_default
+ starexec_run_isabelle
+ starexec_run_isabelle_hot
+ starexec_run_nitpick
+ starexec_run_refute
- At this point I tested the "SYN044^4" mentioned above.
-
- I renamed "README" to "README.orig" and copied this "ReadMe" over.
+ I tested the "SET014^4" problem mentioned above.
Next, I installed and enabled ATPs.
- LEO-II (1.4.3):
+ LEO-II (1.6.2):
I logged to a 32-bit Linux ("lxlabbroy") machine. I retrieved LEO-II from
- http://www.ags.uni-sb.de/~leo/leo2_v1.4.3.tgz
+ http://page.mi.fu-berlin.de/cbenzmueller/leo/leo2_v1.6.2.tgz
- I did "make opt". I copied
- "bin/leo.opt" to "~/Isabelle2013-CASC/contrib/leo".
+ I did "make opt". I copied "bin/leo.opt" to
+ "~/Isabelle2015-CASC/contrib/leo".
I added this line to "etc/settings":
@@ -130,39 +143,57 @@
Vampire (2.6):
- I copied the file "vampire_rel.linux64" from the 2012 CASC archive to
- "~/Isabelle2013-CASC/contrib/vampire".
+ 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=2.6
+ VAMPIRE_VERSION=3.0
+
+ Z3 TPTP (4.3.2.0 postrelease):
- Z3 (3.2):
+ I cloned out the git repository:
+
+ git clone https://git01.codeplex.com/z3
- I uncommented the following line in "contrib/z3-3.2/etc/settings":
+ 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).
- # Z3_NON_COMMERCIAL="yes"
+ I added this line to "etc/settings":
+
+ Z3_TPTP_HOME=$ISABELLE_HOME/contrib
- To test that the examples actually worked, I did
+ 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:
- ./bin/isabelle tty
- theory T imports Main begin;
- lemma "a = b ==> [b] = [a]";
- sledgehammer [e leo2 satallax spass vampire z3 z3_tptp] ();
+ 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
- and I performed the aforementioned sanity tests.
+ ./bin/isabelle_process -e 'use_thy "/tmp/T";'
+
+ I also performed the aforementioned sanity tests.
- Ideas for next year:
+ 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.
- * Expand "p b" to "(b & p True) | (~ b & p False)" (cf. "CSR148^3").
- * Select subset of axioms (cf. "CSR148^3").
That's it.
Jasmin Blanchette
- 21 May 2013
+ 10 June 2015