--- a/NEWS Sun Mar 14 20:29:26 2021 +0100
+++ b/NEWS Sun Mar 14 21:02:34 2021 +0100
@@ -16,6 +16,12 @@
as no timeout; before it meant immediate timeout. Rare INCOMPATIBILITY
in boundary cases.
+* Remote provers from SystemOnTPTP (notably for Sledgehammer) are now
+managed via Isabelle/Scala instead of perl; the dependency on
+libwww-perl has been eliminated (notably on Linux). Rare
+INCOMPATIBILITY: HTTP proxy configuration now works via JVM properties
+https://docs.oracle.com/en/java/javase/11/docs/api/java.base/java/net/doc-files/net-properties.html
+
*** Document preparation ***
--- a/src/Doc/Sledgehammer/document/root.tex Sun Mar 14 20:29:26 2021 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Sun Mar 14 21:02:34 2021 +0100
@@ -217,19 +217,6 @@
fail to solve the easy goal presented there, something must be wrong with the
installation.
-Remote prover invocation requires Perl with the World Wide Web Library
-(\texttt{libwww-perl}) installed. If you must use a proxy server to access the
-Internet, set the \texttt{http\_proxy} environment variable to the proxy, either
-in the environment in which Isabelle is launched or in your
-\texttt{\$ISABELLE\_HOME\_USER/etc/\allowbreak settings} file. Here are a few
-examples:
-
-\prew
-\texttt{http\_proxy=http://proxy.example.org} \\
-\texttt{http\_proxy=http://proxy.example.org:8080} \\
-\texttt{http\_proxy=http://joeblow:pAsSwRd@proxy.example.org}
-\postw
-
\section{First Steps}
\label{first-steps}
--- a/src/HOL/Tools/ATP/atp_proof.ML Sun Mar 14 20:29:26 2021 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Sun Mar 14 21:02:34 2021 +0100
@@ -25,12 +25,9 @@
ProofIncomplete |
ProofUnparsable |
UnsoundProof of bool * string list |
- CantConnect |
TimedOut |
Inappropriate |
OutOfResources |
- NoPerl |
- NoLibwwwPerl |
MalformedInput |
MalformedOutput |
Interrupted |
@@ -139,12 +136,9 @@
ProofIncomplete |
ProofUnparsable |
UnsoundProof of bool * string list |
- CantConnect |
TimedOut |
Inappropriate |
OutOfResources |
- NoPerl |
- NoLibwwwPerl |
MalformedInput |
MalformedOutput |
Interrupted |
@@ -180,14 +174,10 @@
| string_of_atp_failure (UnsoundProof (true, ss)) =
"The prover derived \"False\"" ^ from_lemmas ss ^
", which could be due to a bug in Sledgehammer or to inconsistent axioms (including \"sorry\"s)"
- | string_of_atp_failure CantConnect = "Cannot connect to server"
| string_of_atp_failure TimedOut = "Timed out"
| string_of_atp_failure Inappropriate =
"The generated problem lies outside the prover's scope"
| string_of_atp_failure OutOfResources = "The prover ran out of resources"
- | string_of_atp_failure NoPerl = "Perl" ^ missing_message_tail
- | string_of_atp_failure NoLibwwwPerl =
- "The Perl module \"libwww-perl\"" ^ missing_message_tail
| string_of_atp_failure MalformedInput = "The generated problem is malformed"
| string_of_atp_failure MalformedOutput = "The prover output is malformed"
| string_of_atp_failure Interrupted = "The prover was interrupted"
--- a/src/HOL/Tools/ATP/scripts/remote_atp Sun Mar 14 20:29:26 2021 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,119 +0,0 @@
-#!/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);
-}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Sun Mar 14 20:29:26 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Sun Mar 14 21:02:34 2021 +0100
@@ -110,11 +110,6 @@
("% SZS output start Refutation", "% SZS output end Refutation"),
("% SZS output start Proof", "% SZS output end Proof")]
-val known_perl_failures =
- [(CantConnect, "HTTP error"),
- (NoPerl, "env: perl"),
- (NoLibwwwPerl, "Can't locate HTTP")]
-
fun known_szs_failures wrap =
[(Unprovable, wrap "CounterSatisfiable"),
(Unprovable, wrap "Satisfiable"),
@@ -435,8 +430,7 @@
(MalformedInput, "Undefined symbol"),
(MalformedInput, "Free Variable"),
(Unprovable, "No formulae and clauses found in input file"),
- (InternalError, "Please report this error")] @
- known_perl_failures,
+ (InternalError, "Please report this error")],
prem_role = Conjecture,
best_slices = fn _ =>
(* FUDGE *)
@@ -626,7 +620,7 @@
Isabelle_System.absolute_path problem,
command, string_of_int (Int.min (max_remote_secs, to_secs 1 timeout) * 1000)]),
proof_delims = union (op =) tstp_proof_delims proof_delims,
- known_failures = known_failures @ known_perl_failures @ known_says_failures,
+ known_failures = known_failures @ known_says_failures,
prem_role = prem_role,
best_slices = fn ctxt => [(1.0, best_slice ctxt)],
best_max_mono_iters = default_max_mono_iters,
--- a/src/Pure/Admin/build_cygwin.scala Sun Mar 14 20:29:26 2021 +0100
+++ b/src/Pure/Admin/build_cygwin.scala Sun Mar 14 21:02:34 2021 +0100
@@ -12,7 +12,7 @@
val default_mirror: String = "https://isabelle.sketis.net/cygwin_2021"
val packages: List[String] =
- List("curl", "libgmp-devel", "nano", "perl", "perl-libwww-perl", "rlwrap", "unzip")
+ List("curl", "libgmp-devel", "nano", "perl", "rlwrap", "unzip")
def build_cygwin(progress: Progress,
mirror: String = default_mirror,
--- a/src/Pure/Tools/build_docker.scala Sun Mar 14 20:29:26 2021 +0100
+++ b/src/Pure/Tools/build_docker.scala Sun Mar 14 21:02:34 2021 +0100
@@ -15,7 +15,7 @@
private val Isabelle_Name = """^.*?(Isabelle[^/\\:]+)_linux\.tar\.gz$""".r
val packages: List[String] =
- List("curl", "less", "libfontconfig1", "libgomp1", "libwww-perl", "pwgen", "rlwrap", "unzip")
+ List("curl", "less", "libfontconfig1", "libgomp1", "perl", "pwgen", "rlwrap", "unzip")
val package_collections: Map[String, List[String]] =
Map("X11" -> List("libx11-6", "libxext6", "libxrender1", "libxtst6", "libxi6"),