src/HOL/Tools/ATP/scripts/remote_atp

misc tuning and clarification: prefer Executable.libraries_closure;

#!/usr/bin/env perl
#
# Wrapper for custom remote provers on SystemOnTPTP
# Author: Fabian Immler, TU Muenchen
# Author: Jasmin Blanchette, TU Muenchen
#

use warnings;
use strict;
use Getopt::Std;
use HTTP::Request::Common;
use LWP;

my $SystemOnTPTPFormReplyURL =
  "http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply";

# default parameters
my %URLParameters = (
    "NoHTML" => 1,
    "QuietFlag" => "-q01",
    "SubmitButton" => "RunSelectedSystems",
    "ProblemSource" => "UPLOAD",
    "ForceSystem" => "-force",
    );

#----Get format and transform options if specified
my %Options;
getopts("hws:t:c:q:",\%Options);

#----Usage
sub usage() {
  print("Usage: remote_atp [<options>] <file_name>\n");
  print("Options:\n");
  print("    -h              print this help\n");
  print("    -w              list available ATPs\n");
  print("    -s<system>      ATP to use\n");
  print("    -t<time_limit>  CPU time limit for ATP\n");
  print("    -c<command>     custom ATP invocation command\n");
  print("    -q<num>         quietness level (0 = most verbose, 3 = least verbose)\n");
  print("    <file_name>     TPTP problem file\n");
  exit(0);
}
if (exists($Options{'h'})) {
  usage();
}

#----What systems flag
if (exists($Options{'w'})) {
    $URLParameters{"SubmitButton"} = "ListSystems";
    delete($URLParameters{"ProblemSource"});
}

#----X2TPTP
if (exists($Options{'x'})) {
    $URLParameters{"X2TPTP"} = "-S";
}

#----Selected system
my $System;
if (exists($Options{'s'})) {
    $System = $Options{'s'};
} else {
    # use Vampire as default
    $System = "Vampire---9.0";
}
$URLParameters{"System___$System"} = $System;

#----Time limit
if (exists($Options{'t'})) {
    $URLParameters{"TimeLimit___$System"} = $Options{'t'};
}
#----Custom command
if (exists($Options{'c'})) {
    $URLParameters{"Command___$System"} = $Options{'c'};
}
#----Quietness
if (exists($Options{'q'})) {
    $URLParameters{"QuietFlag"} = "-q" . $Options{'q'};
}

#----Get single file name
if (exists($URLParameters{"ProblemSource"})) {
    if (scalar(@ARGV) >= 1) {
        $URLParameters{"UPLOADProblem"} = [shift(@ARGV)];
    } else {
      print("Missing problem file\n");
      usage();
      die;
    }
}

# Query Server
my $Agent = LWP::UserAgent->new;
$Agent->env_proxy;
$Agent->agent("Sledgehammer");
if (exists($Options{'t'})) {
  # give server more time to respond
  $Agent->timeout($Options{'t'} + 15);
}
my $Request = POST($SystemOnTPTPFormReplyURL,
	Content_Type => 'form-data',Content => \%URLParameters);
my $Response = $Agent->request($Request);

#catch errors / failure
if(!$Response->is_success) {
  my $message = $Response->message;
  $message =~ s/ \(Bad hostname ['"][^'"]*['"]\)//;
  print "HTTP error: " . $message . "\n";
  exit(-1);
} elsif (exists($Options{'w'})) {
  print $Response->content;
  exit (0);
} elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
  print "The ATP \"$1\" is not available at SystemOnTPTP\n";
  exit(-1);
} else {
  print $Response->content;
  exit(0);
}