# HG changeset patch # User wenzelm # Date 1615752154 -3600 # Node ID e92f2e44e4d8dcaf887c2769aa25f6f161a685da # Parent 1cc848548f219f890c4175a2994b5acb9755d711 removed spurious references to perl / libwww-perl; diff -r 1cc848548f21 -r e92f2e44e4d8 NEWS --- 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 *** diff -r 1cc848548f21 -r e92f2e44e4d8 src/Doc/Sledgehammer/document/root.tex --- 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} diff -r 1cc848548f21 -r e92f2e44e4d8 src/HOL/Tools/ATP/atp_proof.ML --- 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" diff -r 1cc848548f21 -r e92f2e44e4d8 src/HOL/Tools/ATP/scripts/remote_atp --- 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 [] \n"); - print("Options:\n"); - print(" -h print this help\n"); - print(" -w list available ATPs\n"); - print(" -s ATP to use\n"); - print(" -t CPU time limit for ATP\n"); - print(" -c custom ATP invocation command\n"); - print(" -q quietness level (0 = most verbose, 3 = least verbose)\n"); - print(" 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); -} diff -r 1cc848548f21 -r e92f2e44e4d8 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- 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, diff -r 1cc848548f21 -r e92f2e44e4d8 src/Pure/Admin/build_cygwin.scala --- 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, diff -r 1cc848548f21 -r e92f2e44e4d8 src/Pure/Tools/build_docker.scala --- 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"),