--- a/CONTRIBUTORS Fri Oct 03 13:21:01 2008 +0200
+++ b/CONTRIBUTORS Fri Oct 03 14:06:19 2008 +0200
@@ -7,6 +7,13 @@
Contributions to this Isabelle version
--------------------------------------
+* August 2008: Fabian Immler, TUM
+ Vampire wrapper script for remote SystemOnTPTP service.
+
+
+Contributions to Isabelle2008
+-----------------------------
+
* 2007/2008:
Alexander Krauss, TUM and Florian Haftmann, TUM and Stefan Berghofer, TUM
HOL library improvements.
--- a/NEWS Fri Oct 03 13:21:01 2008 +0200
+++ b/NEWS Fri Oct 03 14:06:19 2008 +0200
@@ -66,6 +66,10 @@
*** HOL ***
+* Wrapper script for remote SystemOnTPTP service allows to use
+sledghammer without local ATP installation (Vampire etc.); see
+ISABELLE_HOME/contrib/SystemOnTPTP/.
+
* Normalization by evaluation now allows non-leftlinear equations.
Declare with attribute [code nbe].
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/contrib/SystemOnTPTP/vampire Fri Oct 03 14:06:19 2008 +0200
@@ -0,0 +1,60 @@
+#!/usr/bin/env perl
+#
+# Vampire Wrapper for SystemOnTPTP
+# Author: Fabian Immler, TU Muenchen
+#
+# - querys a Vampire theorem prover on SystemOnTPTP
+# (http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP)
+# - behaves like a local Vampire
+# => can be used for Isabelle when Vampire is not available (e.g. on a Mac)
+#
+
+use warnings;
+use strict;
+
+use Getopt::Std;
+use HTTP::Request::Common;
+use LWP::UserAgent;
+
+# address of proof-server
+my $SystemOnTPTPFormReplyURL = "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
+
+#name of prover and its executable on the server, e.g.
+# Vampire---9.0
+# jumpirefix
+my $prover = "Vampire---9.0";
+my $command = "jumpirefix";
+
+# pass arguments
+my $options = "";
+while(scalar(@ARGV)>1){
+ $options.=" ".shift(@ARGV);
+}
+# last argument is problemfile to be uploaded
+my $problem = [shift(@ARGV)];
+
+# fill in form
+my %URLParameters = (
+ "NoHTML" => 1,
+ "QuietFlag" => "-q01",
+ "SubmitButton" => "RunSelectedSystems",
+ "ProblemSource" => "UPLOAD",
+ "UPLOADProblem" => $problem,
+ "System___$prover" => "$prover",
+ "Format___$prover" => "tptp",
+ "Command___$prover" => "$command $options %s"
+);
+
+# Query Server
+my $Agent = LWP::UserAgent->new;
+my $Request = POST($SystemOnTPTPFormReplyURL,
+ Content_Type => 'form-data',Content => \%URLParameters);
+my $Response = $Agent->request($Request);
+
+#catch errors, let isabelle/watcher know
+if($Response->is_success){
+ print $Response->content;
+} else {
+ print $Response->message;
+ print "\nCANNOT PROVE\n";
+}
--- a/etc/settings Fri Oct 03 13:21:01 2008 +0200
+++ b/etc/settings Fri Oct 03 14:06:19 2008 +0200
@@ -227,7 +227,8 @@
# External provers
E_HOME=$(choosefrom "$ISABELLE_HOME/contrib/E/$ML_PLATFORM" "/usr/local/E" "")
-VAMPIRE_HOME=$(choosefrom "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" "/usr/local/Vampire" "")
+VAMPIRE_HOME=$(choosefrom "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" "/usr/local/Vampire" \
+ "$ISABELLE_HOME/contrib/SystemOnTPTP" "")
SPASS_HOME=$(choosefrom "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" "/usr/local/SPASS" "")
# HOL4 proof objects (cf. Isabelle/src/HOL/Import)