--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jul 27 20:16:14 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Wed Jul 28 00:53:24 2010 +0200
@@ -12,8 +12,8 @@
OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError
type prover_config =
- {home_var: string,
- executable: string,
+ {executable: string * string,
+ required_executables: (string * string) list,
arguments: bool -> Time.time -> string,
proof_delims: (string * string) list,
known_failures: (failure * string) list,
@@ -39,8 +39,8 @@
OldSpass | MalformedInput | MalformedOutput | UnknownError
type prover_config =
- {home_var: string,
- executable: string,
+ {executable: string * string,
+ required_executables: (string * string) list,
arguments: bool -> Time.time -> string,
proof_delims: (string * string) list,
known_failures: (failure * string) list,
@@ -84,8 +84,8 @@
("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
val e_config : prover_config =
- {home_var = "E_HOME",
- executable = "eproof",
+ {executable = ("E_HOME", "eproof"),
+ required_executables = [],
arguments = fn _ => fn timeout =>
"--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^
string_of_int (to_generous_secs timeout),
@@ -108,8 +108,8 @@
(* The "-VarWeight=3" option helps the higher-order problems, probably by
counteracting the presence of "hAPP". *)
val spass_config : prover_config =
- {home_var = "ISABELLE_ATP_MANAGER",
- executable = "SPASS_TPTP",
+ {executable = ("ISABELLE_ATP_MANAGER", "SPASS_TPTP"),
+ required_executables = [("SPASS_HOME", "SPASS")],
(* "div 2" accounts for the fact that SPASS is often run twice. *)
arguments = fn complete => fn timeout =>
("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
@@ -132,8 +132,8 @@
(* Vampire *)
val vampire_config : prover_config =
- {home_var = "VAMPIRE_HOME",
- executable = "vampire",
+ {executable = ("VAMPIRE_HOME", "vampire"),
+ required_executables = [],
arguments = fn _ => fn timeout =>
"--output_syntax tptp --mode casc -t " ^
string_of_int (to_generous_secs timeout),
@@ -183,8 +183,8 @@
({proof_delims, known_failures, max_new_relevant_facts_per_iter,
prefers_theory_relevant, explicit_forall, ...} : prover_config)
: prover_config =
- {home_var = "ISABELLE_ATP_MANAGER",
- executable = "SystemOnTPTP",
+ {executable = ("ISABELLE_ATP_MANAGER", "SystemOnTPTP"),
+ required_executables = [],
arguments = fn _ => fn timeout =>
args ^ " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
the_system atp_prefix,
@@ -203,8 +203,10 @@
val remote_spass = remote_prover spass "SPASS---" "-x" spass_config
val remote_vampire = remote_prover vampire "Vampire---9" "" vampire_config
-fun maybe_remote (name, _) ({home_var, ...} : prover_config) =
- name |> getenv home_var = "" ? remote_name
+fun maybe_remote (name, _)
+ ({executable, required_executables, ...} : prover_config) =
+ name |> exists (curry (op =) "" o getenv o fst)
+ (executable :: required_executables) ? remote_name
fun default_atps_param_value () =
space_implode " " [maybe_remote e e_config, maybe_remote spass spass_config,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Jul 27 20:16:14 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Jul 28 00:53:24 2010 +0200
@@ -708,9 +708,9 @@
(* generic TPTP-based provers *)
fun prover_fun name
- {home_var, executable, arguments, proof_delims, known_failures,
- max_new_relevant_facts_per_iter, prefers_theory_relevant,
- explicit_forall}
+ {executable, required_executables, arguments, proof_delims,
+ known_failures, max_new_relevant_facts_per_iter,
+ prefers_theory_relevant, explicit_forall}
({debug, overlord, full_types, explicit_apply, relevance_threshold,
relevance_convergence, theory_relevant, defs_relevant, isar_proof,
isar_shrink_factor, ...} : params)
@@ -753,8 +753,7 @@
else error ("No such directory: " ^ the_dest_dir ^ ".")
end;
- val home = getenv home_var
- val command = Path.explode (home ^ "/" ^ executable)
+ val command = Path.explode (getenv (fst executable) ^ "/" ^ snd executable)
(* write out problem file and call prover *)
fun command_line complete probfile =
let
@@ -778,41 +777,44 @@
val as_time = the_default 0 o Scan.read Symbol.stopper time o explode;
in (output, as_time t) end;
fun run_on probfile =
- if home = "" then
+ case filter (curry (op =) "" o getenv o fst)
+ (executable :: required_executables) of
+ (home_var, _) :: _ =>
error ("The environment variable " ^ quote home_var ^ " is not set.")
- else if File.exists command then
- let
- fun do_run complete =
- let
- val command = command_line complete probfile
- val ((output, msecs), res_code) =
- bash_output command
- |>> (if overlord then
- prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
- else
- I)
- |>> (if Config.get ctxt measure_runtime then split_time
- else rpair 0)
- val (proof, outcome) =
- extract_proof_and_outcome complete res_code proof_delims
- known_failures output
- in (output, msecs, proof, outcome) end
- val readable_names = debug andalso overlord
- val (pool, conjecture_offset) =
- write_tptp_file thy readable_names explicit_forall full_types
- explicit_apply probfile clauses
- val conjecture_shape =
- conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
- val result =
- do_run false
- |> (fn (_, msecs0, _, SOME _) =>
- do_run true
- |> (fn (output, msecs, proof, outcome) =>
- (output, msecs0 + msecs, proof, outcome))
- | result => result)
- in ((pool, conjecture_shape), result) end
- else
- error ("Bad executable: " ^ Path.implode command ^ ".");
+ | [] =>
+ if File.exists command then
+ let
+ fun do_run complete =
+ let
+ val command = command_line complete probfile
+ val ((output, msecs), res_code) =
+ bash_output command
+ |>> (if overlord then
+ prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
+ else
+ I)
+ |>> (if Config.get ctxt measure_runtime then split_time
+ else rpair 0)
+ val (proof, outcome) =
+ extract_proof_and_outcome complete res_code proof_delims
+ known_failures output
+ in (output, msecs, proof, outcome) end
+ val readable_names = debug andalso overlord
+ val (pool, conjecture_offset) =
+ write_tptp_file thy readable_names explicit_forall full_types
+ explicit_apply probfile clauses
+ val conjecture_shape =
+ conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
+ val result =
+ do_run false
+ |> (fn (_, msecs0, _, SOME _) =>
+ do_run true
+ |> (fn (output, msecs, proof, outcome) =>
+ (output, msecs0 + msecs, proof, outcome))
+ | result => result)
+ in ((pool, conjecture_shape), result) end
+ else
+ error ("Bad executable: " ^ Path.implode command ^ ".")
(* If the problem file has not been exported, remove it; otherwise, export
the proof file too. *)