--- a/doc-src/Sledgehammer/sledgehammer.tex Thu Feb 10 10:32:12 2011 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex Thu Feb 10 18:44:39 2011 +0100
@@ -143,7 +143,11 @@
\item[$\bullet$] Alternatively, you can download the Isabelle-aware E and SPASS
binary packages from Isabelle's download page. Extract the archives, then add a
-line to your \texttt{\char`\~/.isabelle/etc/components} file with the absolute
+line to your \texttt{\$ISABELLE\_HOME\_USER/etc/components}%
+\footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at
+startup. Its value can be retrieved by invoking \texttt{isabelle}
+\texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.}
+file with the absolute
path to E or SPASS. For example, if the \texttt{components} does not exist yet
and you extracted SPASS to \texttt{/usr/local/spass-3.7}, create the
\texttt{components} file with the single line
@@ -173,7 +177,7 @@
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{\char`\~/.isabelle/etc/settings} file. Here are a few examples:
+\texttt{\char`\~/\$ISABELLE\_HOME\_USER/etc/settings} file. Here are a few examples:
\prew
\texttt{http\_proxy=http://proxy.example.org} \\
--- a/src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML Thu Feb 10 10:32:12 2011 +0100
+++ b/src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML Thu Feb 10 18:44:39 2011 +0100
@@ -39,13 +39,6 @@
relevance_thresholds
(the_default default_max_relevant max_relevant) is_built_in_const
relevance_fudge relevance_override chained_ths hyp_ts concl_t
- (* Check for constants other than the built-in HOL constants. If none of
- them appear (as should be the case for TPTP problems, unless "auto" or
- "simp" already did its "magic"), we can skip the relevance filter. *)
- val pure_goal =
- not (exists_Const (fn (s, _) => String.isSubstring "." s andalso
- not (String.isSubstring "HOL" s))
- (prop_of goal))
val problem =
{state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
facts = map Sledgehammer_Provers.Untranslated_Fact facts,
--- a/src/HOL/Tools/ATP/atp_proof.ML Thu Feb 10 10:32:12 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Feb 10 18:44:39 2011 +0100
@@ -27,7 +27,7 @@
val strip_spaces : (char -> bool) -> string -> string
val short_output : bool -> string -> string
- val string_for_failure : string -> failure -> string
+ val string_for_failure : failure -> string
val extract_important_message : string -> string
val extract_known_failure :
(failure * string) list -> string -> failure option
@@ -82,22 +82,20 @@
fun short_output verbose output =
if verbose then elide_string 1000 output else ""
-fun missing_message_tail prover =
- " appears to be missing. You will need to install it if you want to run " ^
- prover ^ "s remotely."
+val missing_message_tail =
+ " appears to be missing. You will need to install it if you want to invoke \
+ \remote provers."
-fun string_for_failure prover Unprovable =
- "The " ^ prover ^ " problem is unprovable."
- | string_for_failure prover IncompleteUnprovable =
- "The " ^ prover ^ " cannot prove the problem."
- | string_for_failure prover ProofMissing =
- "The " ^ prover ^ " claims the conjecture is a theorem but did not provide \
- \a proof."
- | string_for_failure _ CantConnect = "Cannot connect to remote server."
- | string_for_failure _ TimedOut = "Timed out."
- | string_for_failure prover OutOfResources =
- "The " ^ prover ^ " ran out of resources."
- | string_for_failure _ SpassTooOld =
+fun string_for_failure Unprovable =
+ "The problem is unprovable."
+ | string_for_failure IncompleteUnprovable =
+ "The prover gave up."
+ | string_for_failure ProofMissing =
+ "The prover claims the conjecture is a theorem but did not provide a proof."
+ | string_for_failure CantConnect = "Cannot connect to remote server."
+ | string_for_failure TimedOut = "Timed out."
+ | string_for_failure OutOfResources = "The prover ran out of resources."
+ | string_for_failure SpassTooOld =
"Isabelle requires a more recent version of SPASS with support for the \
\TPTP syntax. To install it, download and extract the package \
\\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \
@@ -106,26 +104,23 @@
(Path.variable "ISABELLE_HOME_USER" ::
map Path.basic ["etc", "components"])))) ^
" on a line of its own."
- | string_for_failure _ VampireTooOld =
+ | string_for_failure VampireTooOld =
"Isabelle requires a more recent version of Vampire. To install it, follow \
\the instructions from the Sledgehammer manual (\"isabelle doc\
\ sledgehammer\")."
- | string_for_failure prover NoPerl = "Perl" ^ missing_message_tail prover
- | string_for_failure prover NoLibwwwPerl =
- "The Perl module \"libwww-perl\"" ^ missing_message_tail prover
- | string_for_failure _ NoRealZ3 =
+ | string_for_failure NoPerl = "Perl" ^ missing_message_tail
+ | string_for_failure NoLibwwwPerl =
+ "The Perl module \"libwww-perl\"" ^ missing_message_tail
+ | string_for_failure NoRealZ3 =
"The environment variable \"Z3_REAL_SOLVER\" must be set to Z3's full path."
- | string_for_failure prover MalformedInput =
- "The " ^ prover ^ " problem is malformed. Please report this to the \
- \Isabelle developers."
- | string_for_failure prover MalformedOutput =
- "The " ^ prover ^ " output is malformed."
- | string_for_failure prover Crashed = "The " ^ prover ^ " crashed."
- | string_for_failure prover InternalError =
- "An internal " ^ prover ^ " error occurred."
- | string_for_failure prover (UnknownError string) =
- (* "An" is correct for "ATP" and "SMT". *)
- "An " ^ prover ^ " error occurred" ^
+ | string_for_failure MalformedInput =
+ "The generated problem is malformed. Please report this to the Isabelle \
+ \developers."
+ | string_for_failure MalformedOutput = "The prover output is malformed."
+ | string_for_failure Crashed = "The prover crashed."
+ | string_for_failure InternalError = "An internal prover error occurred."
+ | string_for_failure (UnknownError string) =
+ "A prover error occurred" ^
(if string = "" then ". (Pass the \"verbose\" option for details.)"
else ":\n" ^ string)
--- a/src/HOL/Tools/ATP/atp_systems.ML Thu Feb 10 10:32:12 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Feb 10 18:44:39 2011 +0100
@@ -260,7 +260,7 @@
(output, 0) => split_lines output
| (output, _) =>
error (case extract_known_failure known_perl_failures output of
- SOME failure => string_for_failure "ATP" failure
+ SOME failure => string_for_failure failure
| NONE => perhaps (try (unsuffix "\n")) output ^ ".")
fun find_system name [] systems = find_first (String.isPrefix name) systems
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu Feb 10 10:32:12 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu Feb 10 18:44:39 2011 +0100
@@ -74,9 +74,9 @@
generated; if it returns "false" for an overloaded constant, the ATP gets a
license to do unsound reasoning if the type system is "overloaded_args". *)
fun is_overloaded thy s =
- not (!precise_overloaded_args) orelse
- s = @{const_name finite} orelse
- (s <> @{const_name HOL.eq} andalso
+ not (s = @{const_name HOL.eq}) andalso
+ not (s = @{const_name Metis.fequal}) andalso
+ (not (!precise_overloaded_args) orelse s = @{const_name finite} orelse
length (Defs.specifications_of (Theory.defs_of thy) s) > 1)
fun needs_type_args thy type_sys s =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Feb 10 10:32:12 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Feb 10 18:44:39 2011 +0100
@@ -30,11 +30,6 @@
(* wrapper for calling external prover *)
-fun short_string_for_failure ATP_Proof.Unprovable = "Unprovable."
- | short_string_for_failure ATP_Proof.TimedOut = "Timed out."
- | short_string_for_failure ATP_Proof.Interrupted = "Interrupted."
- | short_string_for_failure _ = "Error."
-
fun n_facts names =
let val n = length names in
string_of_int n ^ " fact" ^ plural_s n ^
@@ -81,10 +76,9 @@
in
print silent (fn () =>
case outcome of
- SOME failure => short_string_for_failure failure
- | NONE =>
- if length used_facts = length facts then "Found proof."
- else "Found proof with " ^ n_facts used_facts ^ ".");
+ SOME failure => string_for_failure failure
+ | NONE => if length used_facts = length facts then "Found proof."
+ else "Found proof with " ^ n_facts used_facts ^ ".");
result
end
@@ -151,13 +145,11 @@
fun minimize_facts prover_name (params as {timeout, ...}) explicit_apply_opt
silent i n state facts =
let
- val thy = Proof.theory_of state
val ctxt = Proof.context_of state
val prover = get_prover ctxt false prover_name
val msecs = Time.toMilliseconds timeout
val _ = print silent (fn () => "Sledgehammer minimize: " ^
quote prover_name ^ ".")
- val {goal, ...} = Proof.goal state
fun do_test timeout =
test_facts params explicit_apply_opt silent prover timeout i n state
val timer = Timer.startRealTimer ()
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Feb 10 10:32:12 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Feb 10 18:44:39 2011 +0100
@@ -467,7 +467,7 @@
|>> append_to_message)
| SOME ProofMissing =>
(NONE, metis_proof_text metis_params |>> append_to_message)
- | SOME failure => (outcome, (string_for_failure "ATP" failure, []))
+ | SOME failure => (outcome, (string_for_failure failure, []))
in
{outcome = outcome, message = message, used_facts = used_facts,
run_time_in_msecs = msecs}
@@ -663,7 +663,7 @@
else
"")
end
- | SOME failure => string_for_failure "SMT solver" failure
+ | SOME failure => string_for_failure failure
in
{outcome = outcome, used_facts = map fst used_facts,
run_time_in_msecs = run_time_in_msecs, message = message}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Feb 10 10:32:12 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Feb 10 18:44:39 2011 +0100
@@ -238,16 +238,16 @@
else
())
end
- fun launch_atps (accum as (success, _)) =
- if success orelse null atps then
+ fun launch_atps accum =
+ if null atps then
accum
else
launch_provers state
(get_facts "ATP" no_dangerous_types atp_relevance_fudge o K atps)
(ATP_Translated_Fact oo K (translate_atp_fact ctxt o fst))
(K (K NONE)) atps
- fun launch_smts (accum as (success, _)) =
- if success orelse null smts then
+ fun launch_smts accum =
+ if null smts then
accum
else
let