# HG changeset patch # User blanchet # Date 1280271204 -7200 # Node ID 54448f5d151f652e62cf9658da4842b2e8e49db9 # Parent dc56a9a8e19d4329a3d3cbd12a0f6ea85525f5ab improve detection of installed SPASS diff -r dc56a9a8e19d -r 54448f5d151f src/HOL/Tools/ATP_Manager/atp_systems.ML --- 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, diff -r dc56a9a8e19d -r 54448f5d151f src/HOL/Tools/Sledgehammer/sledgehammer.ML --- 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. *)