# HG changeset patch # User blanchet # Date 1342815585 -7200 # Node ID 416e4123baf36366bb4e5baeaf31ff48e2909568 # Parent 48628962976b56f62e2762572c58ea4fc012c5d6 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster) diff -r 48628962976b -r 416e4123baf3 src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Fri Jul 20 22:19:45 2012 +0200 +++ b/src/HOL/TPTP/atp_theory_export.ML Fri Jul 20 22:19:45 2012 +0200 @@ -66,7 +66,7 @@ val ord = effective_term_order ctxt atp val _ = problem |> lines_for_atp_problem format ord (K []) |> File.write_list prob_file - val path = getenv (List.last (fst exec)) ^ "/" ^ snd exec + val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec) val command = File.shell_path (Path.explode path) ^ " " ^ arguments ctxt false "" (seconds 1.0) (ord, K [], K []) ^ " " ^ diff -r 48628962976b -r 416e4123baf3 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Fri Jul 20 22:19:45 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Jul 20 22:19:45 2012 +0200 @@ -14,8 +14,7 @@ type slice_spec = int * atp_format * string * string * bool type atp_config = - {exec : string list * string, - required_vars : string list list, + {exec : string list * string list, arguments : Proof.context -> bool -> string -> Time.time -> term_order * (unit -> (string * int) list) @@ -87,8 +86,7 @@ type slice_spec = int * atp_format * string * string * bool type atp_config = - {exec : string list * string, - required_vars : string list list, + {exec : string list * string list, arguments : Proof.context -> bool -> string -> Time.time -> term_order * (unit -> (string * int) list) @@ -190,8 +188,7 @@ val alt_ergo_tff1 = TFF (Polymorphic, TPTP_Explicit) val alt_ergo_config : atp_config = - {exec = (["WHY3_HOME"], "why3"), - required_vars = [], + {exec = (["WHY3_HOME"], ["why3"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn _ => "--format tff1 --prover alt-ergo --timelimit " ^ @@ -263,7 +260,7 @@ \--prefer-initial-clauses -winvfreqrank -c1 -Ginvfreqconjmax -F1 \ \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*" ^ e_selection_heuristic_case heuristic "FunWeight" "SymOffsetWeight" ^ - "(SimulateSOS, " ^ + "(SimulateSOS," ^ (e_selection_heuristic_case heuristic e_default_fun_weight e_default_sym_offs_weight |> Config.get ctxt |> Real.ceil |> signed_string_of_int) ^ @@ -303,8 +300,7 @@ fun e_kbo () = if is_recent_e_version () then "KBO6" else "KBO" val e_config : atp_config = - {exec = (["E_HOME"], "eproof"), - required_vars = [], + {exec = (["E_HOME"], ["eproof_ram", "eproof"]), arguments = fn ctxt => fn full_proof => fn heuristic => fn timeout => fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) => @@ -314,11 +310,7 @@ "--term-ordering=" ^ (if is_lpo then "LPO4" else e_kbo ()) ^ " " ^ "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^ e_shell_level_argument full_proof, - proof_delims = - (* work-around for bug in "epclextract" version 1.6 *) - ("# SZS status Theorem\n# SZS output start Saturation.", - "# SZS output end Saturation.") :: - tstp_proof_delims, + proof_delims = tstp_proof_delims, known_failures = [(TimedOut, "Failure: Resource limit exceeded (time)"), (TimedOut, "time limit exceeded")] @ @@ -348,8 +340,7 @@ THF (Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_Without_Defs) val leo2_config : atp_config = - {exec = (["LEO2_HOME"], "leo"), - required_vars = [], + {exec = (["LEO2_HOME"], ["leo"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn _ => "--foatp e --atp e=\"$E_HOME\"/eprover \ @@ -377,8 +368,7 @@ THF (Monomorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs) val satallax_config : atp_config = - {exec = (["SATALLAX_HOME"], "satallax"), - required_vars = [], + {exec = (["SATALLAX_HOME"], ["satallax"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn _ => "-p hocore -t " ^ string_of_int (to_secs 1 timeout), @@ -405,8 +395,7 @@ (* FIXME: Make "SPASS_NEW_HOME" legacy. *) val spass_config : atp_config = - {exec = (["SPASS_NEW_HOME", "SPASS_HOME"], "SPASS"), - required_vars = [], + {exec = (["SPASS_NEW_HOME", "SPASS_HOME"], ["SPASS"]), arguments = fn _ => fn _ => fn extra_options => fn timeout => fn _ => ("-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout)) |> extra_options <> "" ? prefix (extra_options ^ " "), @@ -447,8 +436,7 @@ val vampire_tff0 = TFF (Monomorphic, TPTP_Implicit) val vampire_config : atp_config = - {exec = (["VAMPIRE_HOME"], "vampire"), - required_vars = [], + {exec = (["VAMPIRE_HOME"], ["vampire"]), arguments = fn _ => fn _ => fn sos => fn timeout => fn _ => "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^ " --proof tptp --output_axiom_names on\ @@ -491,8 +479,7 @@ val z3_tff0 = TFF (Monomorphic, TPTP_Implicit) val z3_tptp_config : atp_config = - {exec = (["Z3_HOME"], "z3"), - required_vars = [], + {exec = (["Z3_HOME"], ["z3"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn _ => "MBQI=true -tptp -t:" ^ string_of_int (to_secs 1 timeout), proof_delims = [], @@ -513,8 +500,7 @@ (* Not really a prover: Experimental Polymorphic THF and DFG output *) fun dummy_config format type_enc : atp_config = - {exec = (["ISABELLE_ATP"], "scripts/dummy_atp"), - required_vars = [], + {exec = (["ISABELLE_ATP"], ["scripts/dummy_atp"]), arguments = K (K (K (K (K "")))), proof_delims = [], known_failures = known_szs_status_failures, @@ -577,8 +563,7 @@ fun remote_config system_name system_versions proof_delims known_failures prem_role best_slice : atp_config = - {exec = (["ISABELLE_ATP"], "scripts/remote_atp"), - required_vars = [], + {exec = (["ISABELLE_ATP"], ["scripts/remote_atp"]), arguments = fn _ => fn _ => fn command => fn timeout => fn _ => (if command <> "" then "-c " ^ quote command ^ " " else "") ^ "-s " ^ the_system system_name system_versions ^ " " ^ @@ -660,8 +645,8 @@ val supported_atps = Symtab.keys o Data.get fun is_atp_installed thy name = - let val {exec, required_vars, ...} = get_atp thy name () in - forall (exists (fn var => getenv var <> "")) (fst exec :: required_vars) + let val {exec, ...} = get_atp thy name () in + exists (fn var => getenv var <> "") (fst exec) end fun refresh_systems_on_tptp () = diff -r 48628962976b -r 416e4123baf3 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Jul 20 22:19:45 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Jul 20 22:19:45 2012 +0200 @@ -631,9 +631,8 @@ val mono_max_privileged_facts = 10 fun run_atp mode name - ({exec, required_vars, arguments, proof_delims, known_failures, - prem_role, best_slices, best_max_mono_iters, - best_max_new_mono_instances, ...} : atp_config) + ({exec, arguments, proof_delims, known_failures, prem_role, best_slices, + best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config) (params as {debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, max_facts, max_mono_iters, max_new_mono_instances, isar_proof, isar_shrink_factor, @@ -660,9 +659,17 @@ Path.append (Path.explode dest_dir) problem_file_name else error ("No such directory: " ^ quote dest_dir ^ ".") - val command = + val command0 = case find_first (fn var => getenv var <> "") (fst exec) of - SOME var => Path.explode (getenv var ^ "/" ^ snd exec) + SOME var => + let + val pref = getenv var ^ "/" + val paths = map (Path.explode o prefix pref) (snd exec) + in + case find_first File.exists paths of + SOME path => path + | NONE => error ("Bad executable: " ^ Path.print (hd paths) ^ ".") + end | NONE => error ("The environment variable " ^ quote (hd (fst exec)) ^ " is not set.") fun split_time s = @@ -680,179 +687,162 @@ raw_explode #> Scan.read Symbol.stopper time #> the_default 0 in (output, as_time t |> Time.fromMilliseconds) end fun run_on prob_file = - case find_first (forall (fn var => getenv var = "")) - (fst exec :: required_vars) of - SOME home_vars => - error ("The environment variable " ^ quote (hd home_vars) ^ - " is not set.") - | NONE => - if File.exists command then + let + (* If slicing is disabled, we expand the last slice to fill the entire + time available. *) + val actual_slices = get_slices slice (best_slices ctxt) + val num_actual_slices = length actual_slices + fun monomorphize_facts facts = + let + val ctxt = + ctxt + |> repair_monomorph_context max_mono_iters best_max_mono_iters + max_new_mono_instances best_max_new_mono_instances + (* pseudo-theorem involving the same constants as the subgoal *) + val subgoal_th = + Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy + val rths = + facts |> chop mono_max_privileged_facts + |>> map (pair 1 o snd) + ||> map (pair 2 o snd) + |> op @ + |> cons (0, subgoal_th) + in + Monomorph.monomorph atp_schematic_consts_of rths ctxt |> fst |> tl + |> curry ListPair.zip (map fst facts) + |> maps (fn (name, rths) => + map (pair name o zero_var_indexes o snd) rths) + end + fun run_slice time_left (cache_key, cache_value) + (slice, (time_frac, (complete, + (key as (best_max_facts, format, best_type_enc, + best_lam_trans, best_uncurried_aliases), + extra)))) = let - (* If slicing is disabled, we expand the last slice to fill the - entire time available. *) - val actual_slices = get_slices slice (best_slices ctxt) - val num_actual_slices = length actual_slices - fun monomorphize_facts facts = - let - val ctxt = - ctxt - |> repair_monomorph_context max_mono_iters best_max_mono_iters - max_new_mono_instances best_max_new_mono_instances - (* pseudo-theorem involving the same constants as the subgoal *) - val subgoal_th = - Logic.list_implies (hyp_ts, concl_t) - |> Skip_Proof.make_thm thy - val rths = - facts |> chop mono_max_privileged_facts - |>> map (pair 1 o snd) - ||> map (pair 2 o snd) - |> op @ - |> cons (0, subgoal_th) - in - Monomorph.monomorph atp_schematic_consts_of rths ctxt - |> fst |> tl - |> curry ListPair.zip (map fst facts) - |> maps (fn (name, rths) => - map (pair name o zero_var_indexes o snd) rths) - end - fun run_slice time_left (cache_key, cache_value) - (slice, (time_frac, (complete, - (key as (best_max_facts, format, best_type_enc, - best_lam_trans, best_uncurried_aliases), - extra)))) = - let - val num_facts = - length facts |> is_none max_facts ? Integer.min best_max_facts - val soundness = if strict then Strict else Non_Strict - val type_enc = - type_enc |> choose_type_enc soundness best_type_enc format - val sound = is_type_enc_sound type_enc - val real_ms = Real.fromInt o Time.toMilliseconds - val slice_timeout = - ((real_ms time_left - |> (if slice < num_actual_slices - 1 then - curry Real.min (time_frac * real_ms timeout) - else - I)) - * 0.001) |> seconds - val generous_slice_timeout = - Time.+ (slice_timeout, atp_timeout_slack) - val _ = - if debug then - quote name ^ " slice #" ^ string_of_int (slice + 1) ^ - " with " ^ string_of_int num_facts ^ " fact" ^ - plural_s num_facts ^ " for " ^ - string_from_time slice_timeout ^ "..." - |> Output.urgent_message - else - () - val readable_names = not (Config.get ctxt atp_full_names) - val lam_trans = - case lam_trans of - SOME s => s - | NONE => best_lam_trans - val uncurried_aliases = - case uncurried_aliases of - SOME b => b - | NONE => best_uncurried_aliases - val value as (atp_problem, _, fact_names, _, _) = - if cache_key = SOME key then - cache_value - else - facts - |> map untranslated_fact - |> not sound - ? filter_out (is_dangerous_prop ctxt o prop_of o snd) - |> take num_facts - |> not (is_type_enc_polymorphic type_enc) - ? monomorphize_facts - |> map (apsnd prop_of) - |> prepare_atp_problem ctxt format prem_role type_enc - atp_mode lam_trans uncurried_aliases - readable_names true hyp_ts concl_t - fun sel_weights () = atp_problem_selection_weights atp_problem - fun ord_info () = atp_problem_term_order_info atp_problem - val ord = effective_term_order ctxt name - val full_proof = debug orelse isar_proof - val args = arguments ctxt full_proof extra slice_timeout - (ord, ord_info, sel_weights) - val command = - File.shell_path command ^ " " ^ args ^ " " ^ - File.shell_path prob_file - |> enclose "TIMEFORMAT='%3R'; { time " " ; } 2>&1" - val _ = - atp_problem - |> lines_for_atp_problem format ord ord_info - |> cons ("% " ^ command ^ "\n") - |> File.write_list prob_file - val ((output, run_time), (atp_proof, outcome)) = - TimeLimit.timeLimit generous_slice_timeout - Isabelle_System.bash_output command - |>> (if overlord then - prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") - else - I) - |> fst |> split_time - |> (fn accum as (output, _) => - (accum, - extract_tstplike_proof_and_outcome verbose complete - proof_delims known_failures output - |>> atp_proof_from_tstplike_proof atp_problem - handle UNRECOGNIZED_ATP_PROOF () => - ([], SOME ProofIncomplete))) - handle TimeLimit.TimeOut => - (("", slice_timeout), ([], SOME TimedOut)) - val outcome = - case outcome of - NONE => - (case used_facts_in_unsound_atp_proof ctxt fact_names - atp_proof - |> Option.map (sort string_ord) of - SOME facts => - let - val failure = - UnsoundProof (is_type_enc_sound type_enc, facts) - in - if debug then - (warning (string_for_failure failure); NONE) - else - SOME failure - end - | NONE => NONE) - | _ => outcome - in ((SOME key, value), (output, run_time, atp_proof, outcome)) end - val timer = Timer.startRealTimer () - fun maybe_run_slice slice - (result as (cache, (_, run_time0, _, SOME _))) = - let - val time_left = Time.- (timeout, Timer.checkRealTimer timer) - in - if Time.<= (time_left, Time.zeroTime) then - result - else - run_slice time_left cache slice - |> (fn (cache, (output, run_time, atp_proof, outcome)) => - (cache, (output, Time.+ (run_time0, run_time), - atp_proof, outcome))) - end - | maybe_run_slice _ result = result - in - ((NONE, ([], Symtab.empty, Vector.fromList [], [], Symtab.empty)), - ("", Time.zeroTime, [], SOME InternalError)) - |> fold maybe_run_slice actual_slices - end - else - error ("Bad executable: " ^ Path.print command) + val num_facts = + length facts |> is_none max_facts ? Integer.min best_max_facts + val soundness = if strict then Strict else Non_Strict + val type_enc = + type_enc |> choose_type_enc soundness best_type_enc format + val sound = is_type_enc_sound type_enc + val real_ms = Real.fromInt o Time.toMilliseconds + val slice_timeout = + ((real_ms time_left + |> (if slice < num_actual_slices - 1 then + curry Real.min (time_frac * real_ms timeout) + else + I)) + * 0.001) |> seconds + val generous_slice_timeout = + Time.+ (slice_timeout, atp_timeout_slack) + val _ = + if debug then + quote name ^ " slice #" ^ string_of_int (slice + 1) ^ + " with " ^ string_of_int num_facts ^ " fact" ^ + plural_s num_facts ^ " for " ^ + string_from_time slice_timeout ^ "..." + |> Output.urgent_message + else + () + val readable_names = not (Config.get ctxt atp_full_names) + val lam_trans = + case lam_trans of + SOME s => s + | NONE => best_lam_trans + val uncurried_aliases = + case uncurried_aliases of + SOME b => b + | NONE => best_uncurried_aliases + val value as (atp_problem, _, fact_names, _, _) = + if cache_key = SOME key then + cache_value + else + facts + |> map untranslated_fact + |> not sound + ? filter_out (is_dangerous_prop ctxt o prop_of o snd) + |> take num_facts + |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts + |> map (apsnd prop_of) + |> prepare_atp_problem ctxt format prem_role type_enc atp_mode + lam_trans uncurried_aliases + readable_names true hyp_ts concl_t + fun sel_weights () = atp_problem_selection_weights atp_problem + fun ord_info () = atp_problem_term_order_info atp_problem + val ord = effective_term_order ctxt name + val full_proof = debug orelse isar_proof + val args = arguments ctxt full_proof extra slice_timeout + (ord, ord_info, sel_weights) + val command = + File.shell_path command0 ^ " " ^ args ^ " " ^ + File.shell_path prob_file + |> enclose "TIMEFORMAT='%3R'; { time " " ; } 2>&1" + val _ = + atp_problem + |> lines_for_atp_problem format ord ord_info + |> cons ("% " ^ command ^ "\n") + |> File.write_list prob_file + val ((output, run_time), (atp_proof, outcome)) = + TimeLimit.timeLimit generous_slice_timeout + Isabelle_System.bash_output command + |>> (if overlord then + prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") + else + I) + |> fst |> split_time + |> (fn accum as (output, _) => + (accum, + extract_tstplike_proof_and_outcome verbose complete + proof_delims known_failures output + |>> atp_proof_from_tstplike_proof atp_problem + handle UNRECOGNIZED_ATP_PROOF () => + ([], SOME ProofIncomplete))) + handle TimeLimit.TimeOut => + (("", slice_timeout), ([], SOME TimedOut)) + val outcome = + case outcome of + NONE => + (case used_facts_in_unsound_atp_proof ctxt fact_names atp_proof + |> Option.map (sort string_ord) of + SOME facts => + let + val failure = + UnsoundProof (is_type_enc_sound type_enc, facts) + in + if debug then (warning (string_for_failure failure); NONE) + else SOME failure + end + | NONE => NONE) + | _ => outcome + in ((SOME key, value), (output, run_time, atp_proof, outcome)) end + val timer = Timer.startRealTimer () + fun maybe_run_slice slice + (result as (cache, (_, run_time0, _, SOME _))) = + let + val time_left = Time.- (timeout, Timer.checkRealTimer timer) + in + if Time.<= (time_left, Time.zeroTime) then + result + else + run_slice time_left cache slice + |> (fn (cache, (output, run_time, atp_proof, outcome)) => + (cache, (output, Time.+ (run_time0, run_time), + atp_proof, outcome))) + end + | maybe_run_slice _ result = result + in + ((NONE, ([], Symtab.empty, Vector.fromList [], [], Symtab.empty)), + ("", Time.zeroTime, [], SOME InternalError)) + |> fold maybe_run_slice actual_slices + end (* If the problem file has not been exported, remove it; otherwise, export the proof file too. *) fun cleanup prob_file = if dest_dir = "" then try File.rm prob_file else NONE fun export prob_file (_, (output, _, _, _)) = - if dest_dir = "" then - () - else - File.write (Path.explode (Path.implode prob_file ^ "_proof")) output + if dest_dir = "" then () + else File.write (Path.explode (Path.implode prob_file ^ "_proof")) output val ((_, (_, pool, fact_names, _, sym_tab)), (output, run_time, atp_proof, outcome)) = with_path cleanup export run_on problem_path_name