1.1 --- a/src/HOL/Tools/ATP_Manager/SPASS_TPTP	Wed Jul 28 18:07:25 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,19 +0,0 @@
     1.4 -#!/usr/bin/env bash
     1.5 -#
     1.6 -# Wrapper for SPASS that also outputs the Flotter-generated CNF (needed for
     1.7 -# Isar proof reconstruction)
     1.8 -#
     1.9 -# Author: Jasmin Blanchette, TU Muenchen
    1.10 -
    1.11 -options=${@:1:$(($#-1))}
    1.12 -name=${@:$(($#)):1}
    1.13 -
    1.14 -$SPASS_HOME/tptp2dfg $name $name.fof.dfg
    1.15 -$SPASS_HOME/SPASS -Flotter $name.fof.dfg \
    1.16 -    | sed 's/description({$/description({*/' \
    1.17 -    > $name.cnf.dfg
    1.18 -rm -f $name.fof.dfg
    1.19 -cat $name.cnf.dfg
    1.20 -$SPASS_HOME/SPASS $options $name.cnf.dfg \
    1.21 -    | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
    1.22 -rm -f $name.cnf.dfg

     2.1 --- a/src/HOL/Tools/ATP_Manager/SystemOnTPTP	Wed Jul 28 18:07:25 2010 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,142 +0,0 @@
     2.4 -#!/usr/bin/env perl
     2.5 -#
     2.6 -# Wrapper for custom remote provers on SystemOnTPTP
     2.7 -# Author: Fabian Immler, TU Muenchen
     2.8 -#
     2.9 -
    2.10 -use warnings;
    2.11 -use strict;
    2.12 -use Getopt::Std;
    2.13 -use HTTP::Request::Common;
    2.14 -use LWP;
    2.15 -
    2.16 -my $SystemOnTPTPFormReplyURL =
    2.17 -  "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
    2.18 -
    2.19 -# default parameters
    2.20 -my %URLParameters = (
    2.21 -    "NoHTML" => 1,
    2.22 -    "QuietFlag" => "-q01",
    2.23 -    "SubmitButton" => "RunSelectedSystems",
    2.24 -    "ProblemSource" => "UPLOAD",
    2.25 -    "ForceSystem" => "-force",
    2.26 -    );
    2.27 -
    2.28 -#----Get format and transform options if specified
    2.29 -my %Options;
    2.30 -getopts("hwxs:t:c:",\%Options);
    2.31 -
    2.32 -#----Usage
    2.33 -sub usage() {
    2.34 -  print("Usage: remote [<options>] <File name>\n");
    2.35 -  print("    <options> are ...\n");
    2.36 -  print("    -h            - print this help\n");
    2.37 -  print("    -w            - list available ATP systems\n");
    2.38 -  print("    -x            - use X2TPTP to convert output of prover\n");
    2.39 -  print("    -s<system>    - specified system to use\n");
    2.40 -  print("    -t<timelimit> - CPU time limit for system\n");
    2.41 -  print("    -c<command>   - custom command for system\n");
    2.42 -  print("    <File name>   - TPTP problem file\n");
    2.43 -  exit(0);
    2.44 -}
    2.45 -if (exists($Options{'h'})) {
    2.46 -  usage();
    2.47 -}
    2.48 -
    2.49 -#----What systems flag
    2.50 -if (exists($Options{'w'})) {
    2.51 -    $URLParameters{"SubmitButton"} = "ListSystems";
    2.52 -    delete($URLParameters{"ProblemSource"});
    2.53 -}
    2.54 -
    2.55 -#----X2TPTP
    2.56 -if (exists($Options{'x'})) {
    2.57 -    $URLParameters{"X2TPTP"} = "-S";
    2.58 -}
    2.59 -
    2.60 -#----Selected system
    2.61 -my $System;
    2.62 -if (exists($Options{'s'})) {
    2.63 -    $System = $Options{'s'};
    2.64 -} else {
    2.65 -    # use Vampire as default
    2.66 -    $System = "Vampire---9.0";
    2.67 -}
    2.68 -$URLParameters{"System___$System"} = $System;
    2.69 -
    2.70 -#----Time limit
    2.71 -if (exists($Options{'t'})) {
    2.72 -    $URLParameters{"TimeLimit___$System"} = $Options{'t'};
    2.73 -}
    2.74 -#----Custom command
    2.75 -if (exists($Options{'c'})) {
    2.76 -    $URLParameters{"Command___$System"} = $Options{'c'};
    2.77 -}
    2.78 -
    2.79 -#----Get single file name
    2.80 -if (exists($URLParameters{"ProblemSource"})) {
    2.81 -    if (scalar(@ARGV) >= 1) {
    2.82 -        $URLParameters{"UPLOADProblem"} = [shift(@ARGV)];
    2.83 -    } else {
    2.84 -      print("Missing problem file\n");
    2.85 -      usage();
    2.86 -      die;
    2.87 -    }
    2.88 -}
    2.89 -
    2.90 -# Query Server
    2.91 -my $Agent = LWP::UserAgent->new;
    2.92 -if (exists($Options{'t'})) {
    2.93 -  # give server more time to respond
    2.94 -  $Agent->timeout($Options{'t'} + 10);
    2.95 -}
    2.96 -my $Request = POST($SystemOnTPTPFormReplyURL,
    2.97 -	Content_Type => 'form-data',Content => \%URLParameters);
    2.98 -my $Response = $Agent->request($Request);
    2.99 -
   2.100 -#catch errors / failure
   2.101 -if(!$Response->is_success) {
   2.102 -  print "HTTP-Error: " . $Response->message . "\n";
   2.103 -  exit(-1);
   2.104 -} elsif (exists($Options{'w'})) {
   2.105 -  print $Response->content;
   2.106 -  exit (0);
   2.107 -} elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
   2.108 -  print "Specified System $1 does not exist\n";
   2.109 -  exit(-1);
   2.110 -} elsif (exists($Options{'x'}) &&
   2.111 -  $Response->content =~
   2.112 -    /%\s*Result\s*:\s*(Unsatisfiable|Theorem).*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/ &&
   2.113 -  $Response->content !~ /ERROR: Could not form TPTP format derivation/ )
   2.114 -{
   2.115 -  # converted output: extract proof
   2.116 -  my @lines = split( /\n/, $Response->content);
   2.117 -  my $extract = "";
   2.118 -  foreach my $line (@lines){
   2.119 -      #ignore comments
   2.120 -      if ($line !~ /^%/ && !($line eq "")) {
   2.121 -          $extract .= "$line";
   2.122 -      }
   2.123 -  }
   2.124 -  # insert newlines after ').'
   2.125 -  $extract =~ s/\s//g;
   2.126 -  $extract =~ s/\)\.cnf/\)\.\ncnf/g;
   2.127 -
   2.128 -  print "========== ~~/lib/scripts/SystemOnTPTP extracted proof: ==========\n";
   2.129 -  # orientation for "sledgehammer_proof_reconstruct.ML"
   2.130 -  print "# SZS output start CNFRefutation.\n";
   2.131 -  print "$extract\n";
   2.132 -  print "# SZS output end CNFRefutation.\n";
   2.133 -  # can be useful for debugging; Isabelle ignores this
   2.134 -  print "============== original response from SystemOnTPTP: ==============\n";
   2.135 -  print $Response->content;
   2.136 -  exit(0);
   2.137 -} elsif (!exists($Options{'x'})) {
   2.138 -  # pass output directly to Isabelle
   2.139 -  print $Response->content;
   2.140 -  exit(0);
   2.141 -}else {
   2.142 -  print "Remote script could not extract proof:\n".$Response->content;
   2.143 -  exit(-1);
   2.144 -}
   2.145 -

     3.1 --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Wed Jul 28 18:07:25 2010 +0200
     3.2 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Wed Jul 28 18:32:54 2010 +0200
     3.3 @@ -108,7 +108,7 @@
     3.4  (* The "-VarWeight=3" option helps the higher-order problems, probably by
     3.5     counteracting the presence of "hAPP". *)
     3.6  val spass_config : prover_config =
     3.7 -  {executable = ("ISABELLE_ATP_MANAGER", "SPASS_TPTP"),
     3.8 +  {executable = ("ISABELLE_ATP_MANAGER", "scripts/spass"),
     3.9     required_executables = [("SPASS_HOME", "SPASS")],
    3.10     (* "div 2" accounts for the fact that SPASS is often run twice. *)
    3.11     arguments = fn complete => fn timeout =>
    3.12 @@ -157,7 +157,7 @@
    3.13  val systems = Synchronized.var "atp_systems" ([]: string list)
    3.14  
    3.15  fun get_systems () =
    3.16 -  case bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w" of
    3.17 +  case bash_output "\"$ISABELLE_ATP_MANAGER/scripts/remote_atp\" -w" of
    3.18      (answer, 0) => split_lines answer
    3.19    | (answer, _) =>
    3.20      error ("Failed to get available systems at SystemOnTPTP:\n" ^
    3.21 @@ -180,14 +180,14 @@
    3.22     (TimedOut, "says Timeout"),
    3.23     (MalformedOutput, "Remote script could not extract proof")]
    3.24  
    3.25 -fun remote_config atp_prefix args
    3.26 +fun remote_config atp_prefix
    3.27          ({proof_delims, known_failures, max_new_relevant_facts_per_iter,
    3.28            prefers_theory_relevant, explicit_forall, ...} : prover_config)
    3.29          : prover_config =
    3.30 -  {executable = ("ISABELLE_ATP_MANAGER", "SystemOnTPTP"),
    3.31 +  {executable = ("ISABELLE_ATP_MANAGER", "scripts/remote_atp"),
    3.32     required_executables = [],
    3.33     arguments = fn _ => fn timeout =>
    3.34 -     args ^ " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
    3.35 +     " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
    3.36       the_system atp_prefix,
    3.37     proof_delims = insert (op =) tstp_proof_delims proof_delims,
    3.38     known_failures = remote_known_failures @ known_failures,
    3.39 @@ -197,23 +197,23 @@
    3.40  
    3.41  val remote_name = prefix "remote_"
    3.42  
    3.43 -fun remote_prover prover atp_prefix args config =
    3.44 -  (remote_name (fst prover), remote_config atp_prefix args config)
    3.45 +fun remote_prover (name, config) atp_prefix =
    3.46 +  (remote_name name, remote_config atp_prefix config)
    3.47  
    3.48 -val remote_e = remote_prover e "EP---" "" e_config
    3.49 -val remote_spass = remote_prover spass "SPASS---" "-x" spass_config
    3.50 -val remote_vampire = remote_prover vampire "Vampire---9" "" vampire_config
    3.51 +val remote_e = remote_prover e "EP---"
    3.52 +val remote_vampire = remote_prover vampire "Vampire---9"
    3.53  
    3.54 -fun maybe_remote (name, _)
    3.55 -                 ({executable, required_executables, ...} : prover_config) =
    3.56 -  name |> exists (curry (op =) "" o getenv o fst)
    3.57 -                 (executable :: required_executables) ? remote_name
    3.58 +fun is_installed ({executable, required_executables, ...} : prover_config) =
    3.59 +  forall (curry (op <>) "" o getenv o fst) (executable :: required_executables)
    3.60 +fun maybe_remote (name, config) =
    3.61 +  name |> not (is_installed config) ? remote_name
    3.62  
    3.63  fun default_atps_param_value () =
    3.64 -  space_implode " " [maybe_remote e e_config, maybe_remote spass spass_config,
    3.65 -                     remote_name (fst vampire)]
    3.66 +  space_implode " " ([maybe_remote e] @
    3.67 +                     (if is_installed (snd spass) then [fst spass] else []) @
    3.68 +                     [remote_name (fst vampire)])
    3.69  
    3.70 -val provers = [e, spass, vampire, remote_e, remote_spass, remote_vampire]
    3.71 +val provers = [e, spass, vampire, remote_e, remote_vampire]
    3.72  val setup = fold add_prover provers
    3.73  
    3.74  end;

     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/ATP_Manager/scripts/remote_atp	Wed Jul 28 18:32:54 2010 +0200
     4.3 @@ -0,0 +1,142 @@
     4.4 +#!/usr/bin/env perl
     4.5 +#
     4.6 +# Wrapper for custom remote provers on SystemOnTPTP
     4.7 +# Author: Fabian Immler, TU Muenchen
     4.8 +#
     4.9 +
    4.10 +use warnings;
    4.11 +use strict;
    4.12 +use Getopt::Std;
    4.13 +use HTTP::Request::Common;
    4.14 +use LWP;
    4.15 +
    4.16 +my $SystemOnTPTPFormReplyURL =
    4.17 +  "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
    4.18 +
    4.19 +# default parameters
    4.20 +my %URLParameters = (
    4.21 +    "NoHTML" => 1,
    4.22 +    "QuietFlag" => "-q01",
    4.23 +    "SubmitButton" => "RunSelectedSystems",
    4.24 +    "ProblemSource" => "UPLOAD",
    4.25 +    "ForceSystem" => "-force",
    4.26 +    );
    4.27 +
    4.28 +#----Get format and transform options if specified
    4.29 +my %Options;
    4.30 +getopts("hwxs:t:c:",\%Options);
    4.31 +
    4.32 +#----Usage
    4.33 +sub usage() {
    4.34 +  print("Usage: remote_atp [<options>] <File name>\n");
    4.35 +  print("    <options> are ...\n");
    4.36 +  print("    -h            - print this help\n");
    4.37 +  print("    -w            - list available ATP systems\n");
    4.38 +  print("    -x            - use X2TPTP to convert output of prover\n");
    4.39 +  print("    -s<system>    - specified system to use\n");
    4.40 +  print("    -t<timelimit> - CPU time limit for system\n");
    4.41 +  print("    -c<command>   - custom command for system\n");
    4.42 +  print("    <File name>   - TPTP problem file\n");
    4.43 +  exit(0);
    4.44 +}
    4.45 +if (exists($Options{'h'})) {
    4.46 +  usage();
    4.47 +}
    4.48 +
    4.49 +#----What systems flag
    4.50 +if (exists($Options{'w'})) {
    4.51 +    $URLParameters{"SubmitButton"} = "ListSystems";
    4.52 +    delete($URLParameters{"ProblemSource"});
    4.53 +}
    4.54 +
    4.55 +#----X2TPTP
    4.56 +if (exists($Options{'x'})) {
    4.57 +    $URLParameters{"X2TPTP"} = "-S";
    4.58 +}
    4.59 +
    4.60 +#----Selected system
    4.61 +my $System;
    4.62 +if (exists($Options{'s'})) {
    4.63 +    $System = $Options{'s'};
    4.64 +} else {
    4.65 +    # use Vampire as default
    4.66 +    $System = "Vampire---9.0";
    4.67 +}
    4.68 +$URLParameters{"System___$System"} = $System;
    4.69 +
    4.70 +#----Time limit
    4.71 +if (exists($Options{'t'})) {
    4.72 +    $URLParameters{"TimeLimit___$System"} = $Options{'t'};
    4.73 +}
    4.74 +#----Custom command
    4.75 +if (exists($Options{'c'})) {
    4.76 +    $URLParameters{"Command___$System"} = $Options{'c'};
    4.77 +}
    4.78 +
    4.79 +#----Get single file name
    4.80 +if (exists($URLParameters{"ProblemSource"})) {
    4.81 +    if (scalar(@ARGV) >= 1) {
    4.82 +        $URLParameters{"UPLOADProblem"} = [shift(@ARGV)];
    4.83 +    } else {
    4.84 +      print("Missing problem file\n");
    4.85 +      usage();
    4.86 +      die;
    4.87 +    }
    4.88 +}
    4.89 +
    4.90 +# Query Server
    4.91 +my $Agent = LWP::UserAgent->new;
    4.92 +if (exists($Options{'t'})) {
    4.93 +  # give server more time to respond
    4.94 +  $Agent->timeout($Options{'t'} + 10);
    4.95 +}
    4.96 +my $Request = POST($SystemOnTPTPFormReplyURL,
    4.97 +	Content_Type => 'form-data',Content => \%URLParameters);
    4.98 +my $Response = $Agent->request($Request);
    4.99 +
   4.100 +#catch errors / failure
   4.101 +if(!$Response->is_success) {
   4.102 +  print "HTTP-Error: " . $Response->message . "\n";
   4.103 +  exit(-1);
   4.104 +} elsif (exists($Options{'w'})) {
   4.105 +  print $Response->content;
   4.106 +  exit (0);
   4.107 +} elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
   4.108 +  print "Specified System $1 does not exist\n";
   4.109 +  exit(-1);
   4.110 +} elsif (exists($Options{'x'}) &&
   4.111 +  $Response->content =~
   4.112 +    /%\s*Result\s*:\s*(Unsatisfiable|Theorem).*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/ &&
   4.113 +  $Response->content !~ /ERROR: Could not form TPTP format derivation/ )
   4.114 +{
   4.115 +  # converted output: extract proof
   4.116 +  my @lines = split( /\n/, $Response->content);
   4.117 +  my $extract = "";
   4.118 +  foreach my $line (@lines){
   4.119 +      #ignore comments
   4.120 +      if ($line !~ /^%/ && !($line eq "")) {
   4.121 +          $extract .= "$line";
   4.122 +      }
   4.123 +  }
   4.124 +  # insert newlines after ').'
   4.125 +  $extract =~ s/\s//g;
   4.126 +  $extract =~ s/\)\.cnf/\)\.\ncnf/g;
   4.127 +
   4.128 +  print "========== ~~/lib/scripts/SystemOnTPTP extracted proof: ==========\n";
   4.129 +  # orientation for "sledgehammer_proof_reconstruct.ML"
   4.130 +  print "# SZS output start CNFRefutation.\n";
   4.131 +  print "$extract\n";
   4.132 +  print "# SZS output end CNFRefutation.\n";
   4.133 +  # can be useful for debugging; Isabelle ignores this
   4.134 +  print "============== original response from SystemOnTPTP: ==============\n";
   4.135 +  print $Response->content;
   4.136 +  exit(0);
   4.137 +} elsif (!exists($Options{'x'})) {
   4.138 +  # pass output directly to Isabelle
   4.139 +  print $Response->content;
   4.140 +  exit(0);
   4.141 +}else {
   4.142 +  print "Remote script could not extract proof:\n".$Response->content;
   4.143 +  exit(-1);
   4.144 +}
   4.145 +

     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Tools/ATP_Manager/scripts/spass	Wed Jul 28 18:32:54 2010 +0200
     5.3 @@ -0,0 +1,19 @@
     5.4 +#!/usr/bin/env bash
     5.5 +#
     5.6 +# Wrapper for SPASS that also outputs the Flotter-generated CNF (needed for
     5.7 +# Isar proof reconstruction)
     5.8 +#
     5.9 +# Author: Jasmin Blanchette, TU Muenchen
    5.10 +
    5.11 +options=${@:1:$(($#-1))}
    5.12 +name=${@:$(($#)):1}
    5.13 +
    5.14 +$SPASS_HOME/tptp2dfg $name $name.fof.dfg
    5.15 +$SPASS_HOME/SPASS -Flotter $name.fof.dfg \
    5.16 +    | sed 's/description({$/description({*/' \
    5.17 +    > $name.cnf.dfg
    5.18 +rm -f $name.fof.dfg
    5.19 +cat $name.cnf.dfg
    5.20 +$SPASS_HOME/SPASS $options $name.cnf.dfg \
    5.21 +    | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
    5.22 +rm -f $name.cnf.dfg