1.1 --- a/CONTRIBUTORS	Fri Oct 03 13:21:01 2008 +0200
     1.2 +++ b/CONTRIBUTORS	Fri Oct 03 14:06:19 2008 +0200
     1.3 @@ -7,6 +7,13 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* August 2008: Fabian Immler, TUM
     1.8 +  Vampire wrapper script for remote SystemOnTPTP service.
     1.9 +
    1.10 +
    1.11 +Contributions to Isabelle2008
    1.12 +-----------------------------
    1.13 +
    1.14  * 2007/2008:
    1.15    Alexander Krauss, TUM and Florian Haftmann, TUM and Stefan Berghofer, TUM
    1.16    HOL library improvements.

     2.1 --- a/NEWS	Fri Oct 03 13:21:01 2008 +0200
     2.2 +++ b/NEWS	Fri Oct 03 14:06:19 2008 +0200
     2.3 @@ -66,6 +66,10 @@
     2.4  
     2.5  *** HOL ***
     2.6  
     2.7 +* Wrapper script for remote SystemOnTPTP service allows to use
     2.8 +sledghammer without local ATP installation (Vampire etc.); see
     2.9 +ISABELLE_HOME/contrib/SystemOnTPTP/.
    2.10 +
    2.11  * Normalization by evaluation now allows non-leftlinear equations.
    2.12  Declare with attribute [code nbe].
    2.13  

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/contrib/SystemOnTPTP/vampire	Fri Oct 03 14:06:19 2008 +0200
     3.3 @@ -0,0 +1,60 @@
     3.4 +#!/usr/bin/env perl
     3.5 +#
     3.6 +# Vampire Wrapper for SystemOnTPTP
     3.7 +# Author: Fabian Immler, TU Muenchen
     3.8 +#
     3.9 +# - querys a Vampire theorem prover on SystemOnTPTP
    3.10 +#   (http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP)
    3.11 +# - behaves like a local Vampire
    3.12 +# => can be used for Isabelle when Vampire is not available (e.g. on a Mac)
    3.13 +#
    3.14 +
    3.15 +use warnings;
    3.16 +use strict;
    3.17 +
    3.18 +use Getopt::Std;
    3.19 +use HTTP::Request::Common;
    3.20 +use LWP::UserAgent;
    3.21 +
    3.22 +# address of proof-server
    3.23 +my $SystemOnTPTPFormReplyURL = "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
    3.24 +
    3.25 +#name of prover and its executable on the server, e.g.
    3.26 +# Vampire---9.0
    3.27 +# jumpirefix
    3.28 +my $prover = "Vampire---9.0";
    3.29 +my $command = "jumpirefix";
    3.30 +
    3.31 +# pass arguments
    3.32 +my $options = "";
    3.33 +while(scalar(@ARGV)>1){
    3.34 +	$options.=" ".shift(@ARGV);
    3.35 +}
    3.36 +# last argument is problemfile to be uploaded
    3.37 +my $problem = [shift(@ARGV)];
    3.38 +
    3.39 +# fill in form
    3.40 +my %URLParameters = (
    3.41 +    "NoHTML" => 1,
    3.42 +    "QuietFlag" => "-q01",
    3.43 +    "SubmitButton" => "RunSelectedSystems",
    3.44 +    "ProblemSource" => "UPLOAD",
    3.45 +    "UPLOADProblem" => $problem,
    3.46 +    "System___$prover" => "$prover",
    3.47 +    "Format___$prover" => "tptp",
    3.48 +    "Command___$prover" => "$command $options %s"
    3.49 +);
    3.50 +
    3.51 +# Query Server
    3.52 +my $Agent = LWP::UserAgent->new;
    3.53 +my $Request = POST($SystemOnTPTPFormReplyURL,
    3.54 +	Content_Type => 'form-data',Content => \%URLParameters);
    3.55 +my $Response = $Agent->request($Request);
    3.56 +    
    3.57 +#catch errors, let isabelle/watcher know
    3.58 +if($Response->is_success){
    3.59 +	print $Response->content;
    3.60 +} else {
    3.61 +	print $Response->message;
    3.62 +	print "\nCANNOT PROVE\n";
    3.63 +}

     4.1 --- a/etc/settings	Fri Oct 03 13:21:01 2008 +0200
     4.2 +++ b/etc/settings	Fri Oct 03 14:06:19 2008 +0200
     4.3 @@ -227,7 +227,8 @@
     4.4  
     4.5  # External provers
     4.6  E_HOME=$(choosefrom "$ISABELLE_HOME/contrib/E/$ML_PLATFORM" "/usr/local/E" "")
     4.7 -VAMPIRE_HOME=$(choosefrom "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" "/usr/local/Vampire" "")
     4.8 +VAMPIRE_HOME=$(choosefrom "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" "/usr/local/Vampire" \
     4.9 +  "$ISABELLE_HOME/contrib/SystemOnTPTP" "")
    4.10  SPASS_HOME=$(choosefrom "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" "/usr/local/SPASS" "")
    4.11  
    4.12  # HOL4 proof objects (cf. Isabelle/src/HOL/Import)