# HG changeset patch # User blanchet # Date 1306485007 -7200 # Node ID c96f06bffd90fd34b748ed7cf461aea1f954d196 # Parent 20e9caff1f862aa2d0228e9cb5443f633aedbbd6 merge timeout messages from several ATPs into one message to avoid clutter diff -r 20e9caff1f86 -r c96f06bffd90 doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Fri May 27 10:30:07 2011 +0200 +++ b/doc-src/Sledgehammer/sledgehammer.tex Fri May 27 10:30:07 2011 +0200 @@ -544,9 +544,9 @@ \prew \slshape The prover found a type-unsound proof involving ``\textit{foo}'', -``\textit{bar}'', ``\textit{baz}'' even though a supposedly type-sound encoding -was used (or, less likely, your axioms are inconsistent). You might want to -report this to the Isabelle developers. +``\textit{bar}'', and ``\textit{baz}'' even though a supposedly type-sound +encoding was used (or, less likely, your axioms are inconsistent). You might +want to report this to the Isabelle developers. \postw \point{Auto can solve it---why not Sledgehammer?} diff -r 20e9caff1f86 -r c96f06bffd90 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Fri May 27 10:30:07 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Fri May 27 10:30:07 2011 +0200 @@ -44,6 +44,7 @@ type 'a proof = ('a, 'a, 'a fo_term) formula step list + val serial_commas : string -> string list -> string list val strip_spaces : bool -> (char -> bool) -> string -> string val short_output : bool -> string -> string val string_for_failure : failure -> string @@ -93,6 +94,12 @@ InternalError | UnknownError of string +fun serial_commas _ [] = ["??"] + | serial_commas _ [s] = [s] + | serial_commas conj [s1, s2] = [s1, conj, s2] + | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3] + | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss + fun strip_c_style_comment _ [] = [] | strip_c_style_comment is_evil (#"*" :: #"/" :: cs) = strip_spaces_in_list true is_evil cs @@ -141,7 +148,8 @@ \remote provers." fun involving [] = "" - | involving ss = "involving " ^ commas_quote ss ^ " " + | involving ss = + "involving " ^ space_implode " " (serial_commas "and" (map quote ss)) ^ " " fun string_for_failure Unprovable = "The problem is unprovable." | string_for_failure IncompleteUnprovable = "The prover gave up." diff -r 20e9caff1f86 -r c96f06bffd90 src/HOL/Tools/Sledgehammer/async_manager.ML --- a/src/HOL/Tools/Sledgehammer/async_manager.ML Fri May 27 10:30:07 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/async_manager.ML Fri May 27 10:30:07 2011 +0200 @@ -8,9 +8,11 @@ signature ASYNC_MANAGER = sig - val break_into_chunks : string list -> string list + val implode_desc : string * string -> string + val break_into_chunks : string -> string list val launch : - string -> Time.time -> Time.time -> string -> (unit -> string) -> unit + string -> Time.time -> Time.time -> string * string + -> (unit -> bool * string) -> unit val kill_threads : string -> string -> unit val running_threads : string -> string -> unit val thread_messages : string -> string -> int option -> unit @@ -27,6 +29,12 @@ (** thread management **) +val implode_desc = op ^ o apfst quote + +fun implode_message (workers, work) = + space_implode " " (ATP_Proof.serial_commas "and" (map quote workers)) ^ work + + (* data structures over threads *) structure Thread_Heap = Heap @@ -45,10 +53,12 @@ type state = {manager: Thread.thread option, timeout_heap: Thread_Heap.T, - active: (Thread.thread * (string * Time.time * Time.time * string)) list, - canceling: (Thread.thread * (string * Time.time * string)) list, - messages: (string * string) list, - store: (string * string) list} + active: + (Thread.thread + * (string * Time.time * Time.time * (string * string))) list, + canceling: (Thread.thread * (string * Time.time * (string * string))) list, + messages: (bool * (string * (string * string))) list, + store: (string * (string * string)) list} fun make_state manager timeout_heap active canceling messages store : state = {manager = manager, timeout_heap = timeout_heap, active = active, @@ -60,17 +70,17 @@ (* unregister thread *) -fun unregister message thread = +fun unregister (urgent, message) thread = Synchronized.change global_state (fn state as {manager, timeout_heap, active, canceling, messages, store} => (case lookup_thread active thread of - SOME (tool, _, _, desc) => + SOME (tool, _, _, desc as (worker, its_desc)) => let val active' = delete_thread thread active; val now = Time.now () val canceling' = (thread, (tool, now, desc)) :: canceling - val message' = desc ^ "\n" ^ message - val messages' = (tool, message') :: messages; + val message' = (worker, its_desc ^ "\n" ^ message) + val messages' = (urgent, (tool, message')) :: messages val store' = (tool, message') :: (if length store <= message_store_limit then store else #1 (chop message_store_limit store)); @@ -95,18 +105,23 @@ (* This is a workaround for Proof General's off-by-a-few sendback display bug, whereby "pr" in "proof" is not highlighted. *) -val break_into_chunks = maps (space_explode "\000" o replace_all "\n\n" "\000") +val break_into_chunks = space_explode "\000" o replace_all "\n\n" "\000" fun print_new_messages () = - case Synchronized.change_result global_state - (fn {manager, timeout_heap, active, canceling, messages, store} => - (messages, make_state manager timeout_heap active canceling [] - store)) of - [] => () - | msgs as (tool, _) :: _ => - let val ss = break_into_chunks (map snd msgs) in - List.app Output.urgent_message (tool ^ ": " ^ hd ss :: tl ss) - end + Synchronized.change_result global_state + (fn {manager, timeout_heap, active, canceling, messages, store} => + messages + |> List.partition (fn (urgent, _) => null active orelse urgent) + ||> (fn postponed_messages => + make_state manager timeout_heap active canceling + postponed_messages store)) + |> map (fn (_, (tool, (worker, work))) => ((tool, work), worker)) + |> AList.group (op =) + |> List.app (fn ((tool, work), workers) => + tool ^ ": " ^ + implode_message (workers |> sort string_ord, work) + |> break_into_chunks + |> List.app Output.urgent_message) fun check_thread_manager () = Synchronized.change global_state (fn state as {manager, timeout_heap, active, canceling, messages, store} => @@ -141,7 +156,7 @@ do (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action |> these - |> List.app (unregister "Timed out.\n"); + |> List.app (unregister (false, "Timed out.\n")); print_new_messages (); (*give threads some time to respond to interrupt*) OS.Process.sleep min_wait_time) @@ -168,8 +183,7 @@ let val self = Thread.self () val _ = register tool birth_time death_time desc self - val message = f () - in unregister message self end); + in unregister (f ()) self end); ()) @@ -177,7 +191,7 @@ (* kill threads *) -fun kill_threads tool workers = Synchronized.change global_state +fun kill_threads tool das_wort_worker = Synchronized.change global_state (fn {manager, timeout_heap, active, canceling, messages, store} => let val killing = @@ -185,7 +199,9 @@ if tool' = tool then SOME (th, (tool', Time.now (), desc)) else NONE) active val state' = make_state manager timeout_heap [] (killing @ canceling) messages store; - val _ = if null killing then () else Output.urgent_message ("Killed active " ^ workers ^ ".") + val _ = + if null killing then () + else Output.urgent_message ("Killed active " ^ das_wort_worker ^ "s.") in state' end); @@ -193,7 +209,7 @@ fun seconds time = string_of_int (Time.toSeconds time) ^ " s" -fun running_threads tool workers = +fun running_threads tool das_wort_worker = let val {active, canceling, ...} = Synchronized.value global_state; @@ -201,37 +217,36 @@ fun running_info (_, (tool', birth_time, death_time, desc)) = if tool' = tool then SOME ("Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^ - seconds (Time.- (death_time, now)) ^ " to live:\n" ^ desc) + seconds (Time.- (death_time, now)) ^ " to live:\n" ^ + implode_desc desc) else NONE fun canceling_info (_, (tool', death_time, desc)) = if tool' = tool then - SOME ("Trying to interrupt thread since " ^ - seconds (Time.- (now, death_time)) ^ ":\n" ^ desc) + SOME ("Trying to interrupt " ^ das_wort_worker ^ " since " ^ + seconds (Time.- (now, death_time)) ^ ":\n" ^ implode_desc desc) else NONE val running = case map_filter running_info active of - [] => ["No " ^ workers ^ " running."] - | ss => "Running " ^ workers ^ ":" :: ss + [] => ["No " ^ das_wort_worker ^ "s running."] + | ss => "Running " ^ das_wort_worker ^ "s " :: ss val interrupting = case map_filter canceling_info canceling of [] => [] - | ss => "Trying to interrupt the following " ^ workers ^ ":" :: ss + | ss => "Interrupting " ^ das_wort_worker ^ "s " :: ss in Output.urgent_message (space_implode "\n\n" (running @ interrupting)) end -fun thread_messages tool worker opt_limit = +fun thread_messages tool das_wort_worker opt_limit = let val limit = the_default message_display_limit opt_limit; val tool_store = Synchronized.value global_state |> #store |> filter (curry (op =) tool o fst) val header = - "Recent " ^ worker ^ " messages" ^ + "Recent " ^ das_wort_worker ^ " messages" ^ (if length tool_store <= limit then ":" else " (" ^ string_of_int limit ^ " displayed):"); - in - List.app Output.urgent_message (header :: break_into_chunks - (map snd (#1 (chop limit tool_store)))) - end + val ss = tool_store |> chop limit |> #1 |> map (implode_desc o snd) + in List.app Output.urgent_message (header :: maps break_into_chunks ss) end end; diff -r 20e9caff1f86 -r c96f06bffd90 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 27 10:30:07 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 27 10:30:07 2011 +0200 @@ -68,7 +68,7 @@ val smt_slice_fact_frac : real Config.T val smt_slice_time_frac : real Config.T val smt_slice_min_secs : int Config.T - val das_Tool : string + val das_tool : string val select_smt_solver : string -> Proof.context -> Proof.context val is_smt_prover : Proof.context -> string -> bool val is_unit_equational_atp : Proof.context -> string -> bool @@ -115,7 +115,7 @@ (* Identifier to distinguish Sledgehammer from other tools using "Async_Manager". *) -val das_Tool = "Sledgehammer" +val das_tool = "Sledgehammer" val select_smt_solver = Context.proof_map o SMT_Config.select_solver @@ -252,9 +252,9 @@ commas (local_provers @ remote_provers) ^ ".") end -fun kill_provers () = Async_Manager.kill_threads das_Tool "provers" -fun running_provers () = Async_Manager.running_threads das_Tool "provers" -val messages = Async_Manager.thread_messages das_Tool "prover" +fun kill_provers () = Async_Manager.kill_threads das_tool "prover" +fun running_provers () = Async_Manager.running_threads das_tool "prover" +val messages = Async_Manager.thread_messages das_tool "prover" (** problems, results, ATPs, etc. **) diff -r 20e9caff1f86 -r c96f06bffd90 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri May 27 10:30:07 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri May 27 10:30:07 2011 +0200 @@ -31,16 +31,16 @@ fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i n goal = - quote name ^ - (if verbose then - " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts - else - "") ^ - " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ - (if blocking then - "." - else - ":\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))) + (name, + (if verbose then + " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts + else + "") ^ + " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ + (if blocking then + "." + else + ":\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))) val auto_minimize_min_facts = Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts} @@ -86,6 +86,11 @@ | NONE => result end) +val someN = "some" +val noneN = "none" +val timeoutN = "timeout" +val unknownN = "unknown" + fun launch_prover (params as {debug, blocking, max_relevant, slicing, timeout, expect, ...}) auto minimize_command only @@ -109,7 +114,9 @@ problem |> get_minimizing_prover ctxt auto name params (minimize_command name) |> (fn {outcome, message, ...} => - (if is_some outcome then "none" else "some" (* sic *), message)) + (if outcome = SOME ATP_Proof.TimedOut then timeoutN + else if is_some outcome then noneN + else someN, message)) fun go () = let val (outcome_code, message) = @@ -117,13 +124,13 @@ really_go () else (really_go () - handle ERROR message => ("unknown", "Error: " ^ message ^ "\n") + handle ERROR message => (unknownN, "Error: " ^ message ^ "\n") | exn => if Exn.is_interrupt exn then reraise exn else - ("unknown", "Internal error:\n" ^ - ML_Compiler.exn_message exn ^ "\n")) + (unknownN, "Internal error:\n" ^ + ML_Compiler.exn_message exn ^ "\n")) val _ = (* The "expect" argument is deliberately ignored if the prover is missing so that the "Metis_Examples" can be processed on any @@ -135,22 +142,27 @@ error ("Unexpected outcome: " ^ quote outcome_code ^ ".") else warning ("Unexpected outcome: " ^ quote outcome_code ^ "."); - in (outcome_code = "some", message) end + in (outcome_code, message) end in if auto then - let val (success, message) = TimeLimit.timeLimit timeout go () in + let + val (outcome_code, message) = TimeLimit.timeLimit timeout go () + val success = (outcome_code = someN) + in (success, state |> success ? Proof.goal_message (fn () => Pretty.chunks [Pretty.str "", Pretty.mark Markup.hilite (Pretty.str message)])) end else if blocking then - let val (success, message) = TimeLimit.timeLimit hard_timeout go () in - List.app Output.urgent_message - (Async_Manager.break_into_chunks [desc ^ "\n" ^ message]); - (success, state) + let val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go () in + Async_Manager.implode_desc desc ^ "\n" ^ message + |> Async_Manager.break_into_chunks + |> List.app Output.urgent_message; + (outcome_code = someN, state) end else - (Async_Manager.launch das_Tool birth_time death_time desc (snd o go); + (Async_Manager.launch das_tool birth_time death_time desc + (apfst (curry (op <>) timeoutN) o go); (false, state)) end diff -r 20e9caff1f86 -r c96f06bffd90 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri May 27 10:30:07 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri May 27 10:30:07 2011 +0200 @@ -38,12 +38,7 @@ fun plural_s n = if n = 1 then "" else "s" -fun serial_commas _ [] = ["??"] - | serial_commas _ [s] = [s] - | serial_commas conj [s1, s2] = [s1, conj, s2] - | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3] - | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss - +val serial_commas = ATP_Proof.serial_commas val simplify_spaces = ATP_Proof.strip_spaces false (K true) fun parse_bool_option option name s =