# HG changeset patch
# User wenzelm
# Date 1223035579 -7200
# Node ID d0b8b0a1fca51fc000c50a2bec171abc656199e3
# Parent  206db9ad527e67bf475ada081bc050e8c88b2f7e
Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);

diff -r 206db9ad527e -r d0b8b0a1fca5 CONTRIBUTORS
--- 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.
diff -r 206db9ad527e -r d0b8b0a1fca5 NEWS
--- 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].
 
diff -r 206db9ad527e -r d0b8b0a1fca5 contrib/SystemOnTPTP/vampire
--- /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";
+}
diff -r 206db9ad527e -r d0b8b0a1fca5 etc/settings
--- 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)