# HG changeset patch # User wenzelm # Date 1443890305 -7200 # Node ID 69022bbcd012e3aad784d30d4f1793a55729ec35 # Parent 6a5a188ab3e7222ccd82b355574daea0bed96488# Parent d84b4d39bce115f79870692c7351d86003626d8c merged diff -r d84b4d39bce1 -r 69022bbcd012 NEWS --- a/NEWS Fri Oct 02 23:22:49 2015 +0200 +++ b/NEWS Sat Oct 03 18:38:25 2015 +0200 @@ -243,15 +243,18 @@ * Discontinued simp_legacy_precond. Potential INCOMPATIBILITY. * Sledgehammer: + - The MaSh relevance filter has been sped up. - Proof reconstruction has been improved, to minimize the incidence of cases where Sledgehammer gives a proof that does not work. - Auto Sledgehammer now minimizes and preplays the results. - Handle Vampire 4.0 proof output without raising exception. - Eliminated "MASH" environment variable. Use the "MaSh" option in Isabelle/jEdit instead. INCOMPATIBILITY. + - Eliminated obsolete "blocking" option and related subcommands. * Nitpick: - Removed "check_potential" and "check_genuine" options. + - Eliminated obsolete "blocking" option. * New commands lift_bnf and copy_bnf for lifting (copying) a BNF structure on the raw type to an abstract type defined using typedef. diff -r d84b4d39bce1 -r 69022bbcd012 src/Doc/Nitpick/document/root.tex --- a/src/Doc/Nitpick/document/root.tex Fri Oct 02 23:22:49 2015 +0200 +++ b/src/Doc/Nitpick/document/root.tex Sat Oct 03 18:38:25 2015 +0200 @@ -118,22 +118,22 @@ must find a model for the axioms. If it finds no model, we have an indication that the axioms might be unsatisfiable. -For Isabelle/jEdit users, Nitpick provides an automatic mode that can be enabled -via the ``Auto Nitpick'' option under ``Plugins > Plugin Options > Isabelle > -General.'' In this mode, Nitpick is run on every newly entered theorem. +Nitpick provides an automatic mode that can be enabled via the ``Auto Nitpick'' +option under ``Plugins > Plugin Options > Isabelle > General'' in +Isabelle/jEdit. In this mode, Nitpick is run on every newly entered theorem. \newbox\boxA \setbox\boxA=\hbox{\texttt{nospam}} -\newcommand\authoremail{\texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak -in.\allowbreak tum.\allowbreak de}} +\newcommand\authoremail{\texttt{jasmin.blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak +inria\allowbreak .\allowbreak fr}} To run Nitpick, you must also make sure that the theory \textit{Nitpick} is imported---this is rarely a problem in practice since it is part of \textit{Main}. The examples presented in this manual can be found in Isabelle's \texttt{src/HOL/\allowbreak Nitpick\_\allowbreak Examples/\allowbreak Manual\_Nits.thy} theory. The known bugs and limitations at the time of writing are listed in -\S\ref{known-bugs-and-limitations}. Comments and bug reports concerning either +\S\ref{known-bugs-and-limitations}. Comments and bug reports concerning the tool or the manual should be directed to the author at \authoremail. \vskip2.5\smallskipamount @@ -1740,18 +1740,18 @@ format (\S\ref{output-format}), regression testing (\S\ref{regression-testing}), optimizations (\S\ref{optimizations}), and timeouts (\S\ref{timeouts}). -If you use Isabelle/jEdit, Nitpick also provides an automatic mode that can -be enabled via the ``Auto Nitpick'' option under ``Plugins > Plugin Options -> Isabelle > General.'' For automatic runs, +Nitpick also provides an automatic mode that can be enabled via the +``Auto Nitpick'' option under ``Plugins > Plugin Options > Isabelle > General'' +in Isabelle/jEdit. For automatic runs, \textit{user\_axioms} (\S\ref{mode-of-operation}), \textit{assms} (\S\ref{mode-of-operation}), and \textit{mono} -(\S\ref{scope-of-search}) are implicitly enabled, \textit{blocking} -(\S\ref{mode-of-operation}), \textit{verbose} (\S\ref{output-format}), and +(\S\ref{scope-of-search}) are implicitly enabled, +\textit{verbose} (\S\ref{output-format}) and \textit{debug} (\S\ref{output-format}) are disabled, \textit{max\_potential} (\S\ref{output-format}) is taken to be 0, \textit{max\_threads} (\S\ref{optimizations}) is taken to be 1, and \textit{timeout} -(\S\ref{timeouts}) is superseded by the ``Auto Time Limit'' in jEdit. Nitpick's -output is also more concise. +(\S\ref{timeouts}) is superseded by the ``Auto Time Limit'' in +Isabelle/jEdit. Nitpick's output is also more concise. The number of options can be overwhelming at first glance. Do not let that worry you: Nitpick's defaults have been chosen so that it almost always does the right @@ -1781,19 +1781,13 @@ \end{enum} Default values are indicated in curly brackets (\textrm{\{\}}). Boolean options -have a negated counterpart (e.g., \textit{blocking} vs.\ -\textit{non\_blocking}). When setting them, ``= \textit{true}'' may be omitted. +have a negated counterpart (e.g., \textit{mono} vs.\ +\textit{non\_mono}). When setting them, ``= \textit{true}'' may be omitted. \subsection{Mode of Operation} \label{mode-of-operation} \begin{enum} -\optrue{blocking}{non\_blocking} -Specifies whether the \textbf{nitpick} command should operate synchronously. -The asynchronous (non-blocking) mode lets the user start proving the putative -theorem while Nitpick looks for a counterexample, but it can also be more -confusing. For technical reasons, automatic runs currently always block. - \optrue{falsify}{satisfy} Specifies whether Nitpick should look for falsifying examples (countermodels) or satisfying examples (models). This manual assumes throughout that diff -r d84b4d39bce1 -r 69022bbcd012 src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Fri Oct 02 23:22:49 2015 +0200 +++ b/src/Doc/Sledgehammer/document/root.tex Sat Oct 03 18:38:25 2015 +0200 @@ -345,9 +345,7 @@ \textit{compress} (\S\ref{output-format}). \item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the -provers' time limit. It is set to 30 seconds, but since Sledgehammer runs -asynchronously you should not hesitate to raise this limit to 60 or 120 seconds -if you are the kind of user who can think clearly while ATPs are active. +provers' time limit. It is set to 30 seconds by default. \end{enum} Options can be set globally using \textbf{sledgehammer\_params} @@ -579,23 +577,11 @@ \item[\labelitemi] \textbf{\textit{run} (the default):} Runs Sledgehammer on subgoal number \qty{num} (1 by default), with the given options and facts. -\item[\labelitemi] \textbf{\textit{messages}:} Redisplays recent messages issued -by Sledgehammer. This allows you to examine results that might have been lost -due to Sledgehammer's asynchronous nature. The \qty{num} argument specifies a -limit on the number of messages to display (10 by default). - \item[\labelitemi] \textbf{\textit{supported\_provers}:} Prints the list of automatic provers supported by Sledgehammer. See \S\ref{installation} and \S\ref{mode-of-operation} for more information on how to install automatic provers. -\item[\labelitemi] \textbf{\textit{running\_provers}:} Prints information about -currently running automatic provers, including elapsed runtime and remaining -time until timeout. - -\item[\labelitemi] \textbf{\textit{kill\_all}:} Terminates all running -threads (automatic provers and machine learners). - \item[\labelitemi] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}. \end{enum} @@ -625,10 +611,6 @@ \item[\labelitemi] \textbf{\textit{relearn\_prover}:} Same as \textit{unlearn} followed by \textit{learn\_prover}. - -\item[\labelitemi] \textbf{\textit{running\_learners}:} Prints information about -currently running machine learners, including elapsed runtime and remaining -time until timeout. \end{enum} Sledgehammer's behavior can be influenced by various \qty{options}, which can be @@ -740,8 +722,8 @@ \end{enum} Default values are indicated in curly brackets (\textrm{\{\}}). Boolean options -have a negative counterpart (e.g., \textit{blocking} vs.\ -\textit{non\_blocking}). When setting Boolean options or their negative +have a negative counterpart (e.g., \textit{minimize} vs.\ +\textit{dont\_minimize}). When setting Boolean options or their negative counterparts, ``= \textit{true\/}'' may be omitted. \subsection{Mode of Operation} @@ -931,14 +913,6 @@ \opnodefault{prover}{string} Alias for \textit{provers}. -\opfalse{blocking}{non\_blocking} -Specifies whether the \textbf{sledgehammer} command should operate -synchronously. The asynchronous (non-blocking) mode lets the user start proving -the putative theorem manually while Sledgehammer looks for a proof, but it can -also be more confusing. Irrespective of the value of this option, Sledgehammer -is always run synchronously if \textit{debug} (\S\ref{output-format}) is -enabled. - \optrue{slice}{dont\_slice} Specifies whether the time allocated to a prover should be sliced into several segments, each of which has its own set of possibly prover-dependent options. @@ -1246,8 +1220,7 @@ \opfalse{debug}{no\_debug} Specifies whether Sledgehammer should display additional debugging information beyond what \textit{verbose} already displays. Enabling \textit{debug} also -enables \textit{verbose} and \textit{blocking} (\S\ref{mode-of-operation}) -behind the scenes. +enables \textit{verbose} behind the scenes. \nopagebreak {\small See also \textit{spy} (\S\ref{mode-of-operation}) and @@ -1298,13 +1271,11 @@ problem. \end{enum} -Sledgehammer emits an error (if \textit{blocking} is enabled) or a warning -(otherwise) if the actual outcome differs from the expected outcome. This option -is useful for regression testing. +Sledgehammer emits an error if the actual outcome differs from the expected outcome. This option is +useful for regression testing. \nopagebreak -{\small See also \textit{blocking} (\S\ref{mode-of-operation}) and -\textit{timeout} (\S\ref{timeouts}).} +{\small See also \textit{timeout} (\S\ref{timeouts}).} \end{enum} \subsection{Timeouts} diff -r d84b4d39bce1 -r 69022bbcd012 src/HOL/Metis_Examples/Proxies.thy --- a/src/HOL/Metis_Examples/Proxies.thy Fri Oct 02 23:22:49 2015 +0200 +++ b/src/HOL/Metis_Examples/Proxies.thy Sat Oct 03 18:38:25 2015 +0200 @@ -14,8 +14,8 @@ imports Type_Encodings begin -sledgehammer_params [prover = spass, blocking, fact_filter = mepo, timeout = 30, - preplay_timeout = 0, dont_minimize] +sledgehammer_params [prover = spass, fact_filter = mepo, timeout = 30, preplay_timeout = 0, + dont_minimize] text {* Extensionality and set constants *} diff -r d84b4d39bce1 -r 69022bbcd012 src/HOL/TPTP/atp_problem_import.ML --- a/src/HOL/TPTP/atp_problem_import.ML Fri Oct 02 23:22:49 2015 +0200 +++ b/src/HOL/TPTP/atp_problem_import.ML Sat Oct 03 18:38:25 2015 +0200 @@ -116,7 +116,7 @@ (if s = "genuine" then if falsify then "CounterSatisfiable" else "Satisfiable" else - "Unknown") + "GaveUp") |> writeln val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy snd file_name val params = @@ -268,7 +268,7 @@ (if success then if null conjs then "Unsatisfiable" else "Theorem" else - "Unknown")) + "GaveUp")) fun sledgehammer_tptp_file thy timeout file_name = let diff -r d84b4d39bce1 -r 69022bbcd012 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Fri Oct 02 23:22:49 2015 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Sat Oct 03 18:38:25 2015 +0200 @@ -22,7 +22,6 @@ monos: (typ option * bool option) list, wfs: ((string * typ) option * bool option) list, sat_solver: string, - blocking: bool, falsify: bool, debug: bool, verbose: bool, @@ -106,7 +105,6 @@ monos: (typ option * bool option) list, wfs: ((string * typ) option * bool option) list, sat_solver: string, - blocking: bool, falsify: bool, debug: bool, verbose: bool, @@ -636,7 +634,7 @@ (if genuine then if falsify then "CounterSatisfiable" else "Satisfiable" else - "Unknown") ^ "\n" ^ + "GaveUp") ^ "\n" ^ "% SZS output start FiniteModel") val (reconstructed_model, codatatypes_ok) = reconstruct_hol_model diff -r d84b4d39bce1 -r 69022bbcd012 src/HOL/Tools/Nitpick/nitpick_commands.ML --- a/src/HOL/Tools/Nitpick/nitpick_commands.ML Fri Oct 02 23:22:49 2015 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML Sat Oct 03 18:38:25 2015 +0200 @@ -44,7 +44,6 @@ ("wf", "smart"), ("sat_solver", "smart"), ("batch_size", "smart"), - ("blocking", "true"), ("falsify", "true"), ("user_axioms", "smart"), ("assms", "true"), @@ -76,7 +75,6 @@ ("dont_finitize", "finitize"), ("non_mono", "mono"), ("non_wf", "wf"), - ("non_blocking", "blocking"), ("satisfy", "falsify"), ("no_user_axioms", "user_axioms"), ("no_assms", "assms"), @@ -234,7 +232,6 @@ else lookup_bool_option_assigns read_type_polymorphic "mono" val wfs = lookup_bool_option_assigns read_const_polymorphic "wf" val sat_solver = lookup_string "sat_solver" - val blocking = mode <> Normal orelse lookup_bool "blocking" val falsify = lookup_bool "falsify" val debug = (mode <> Auto_Try andalso lookup_bool "debug") val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose") @@ -275,8 +272,8 @@ {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns, iters_assigns = iters_assigns, bitss = bitss, bisim_depths = bisim_depths, boxes = boxes, finitizes = finitizes, monos = monos, wfs = wfs, - sat_solver = sat_solver, blocking = blocking, falsify = falsify, - debug = debug, verbose = verbose, overlord = overlord, spy = spy, + sat_solver = sat_solver, falsify = falsify, debug = debug, + verbose = verbose, overlord = overlord, spy = spy, user_axioms = user_axioms, assms = assms, whacks = whacks, merge_type_vars = merge_type_vars, binary_ints = binary_ints, destroy_constrs = destroy_constrs, specialize = specialize, @@ -340,7 +337,7 @@ val thy = Proof.theory_of state val ctxt = Proof.context_of state val _ = List.app check_raw_param override_params - val params as {blocking, debug, ...} = + val params as {debug, ...} = extract_params ctxt mode (default_raw_params thy) override_params fun go () = (unknownN, []) @@ -348,7 +345,7 @@ else if debug then fn f => fn x => f x else handle_exceptions ctxt) (fn _ => pick_nits_in_subgoal state params mode i step) - in if blocking then go () else Future.fork (tap go) |> K (unknownN, []) end + in go () end |> `(fn (outcome_code, _) => outcome_code = genuineN) fun string_for_raw_param (name, value) = diff -r d84b4d39bce1 -r 69022bbcd012 src/HOL/Tools/Sledgehammer/async_manager_legacy.ML --- a/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Fri Oct 02 23:22:49 2015 +0200 +++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Sat Oct 03 18:38:25 2015 +0200 @@ -10,13 +10,9 @@ signature ASYNC_MANAGER_LEGACY = sig - val break_into_chunks : string -> string list val thread : string -> Time.time -> Time.time -> string * string -> (unit -> bool * string) -> unit - val kill_threads : string -> string -> unit val has_running_threads : string -> bool - val running_threads : string -> string -> unit - val thread_messages : string -> string -> int option -> unit end; structure Async_Manager_Legacy : ASYNC_MANAGER_LEGACY = @@ -31,9 +27,6 @@ Simple_Thread.attributes {name = "async_manager", stack_limit = NONE, interrupts = interrupts}); -val message_store_limit = 20 -val message_display_limit = 10 - fun implode_message (workers, work) = space_implode " " (Try.serial_commas "and" workers) ^ work @@ -54,18 +47,17 @@ (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} + messages: (bool * (string * (string * string))) list} -fun make_state manager timeout_heap active canceling messages store : state = - {manager = manager, timeout_heap = timeout_heap, active = active, - canceling = canceling, messages = messages, store = store} +fun make_state manager timeout_heap active canceling messages : state = + {manager = manager, timeout_heap = timeout_heap, active = active, canceling = canceling, + messages = messages} -val global_state = Synchronized.var "async_manager" (make_state NONE Thread_Heap.empty [] [] [] []) +val global_state = Synchronized.var "async_manager" (make_state NONE Thread_Heap.empty [] [] []) fun unregister (urgent, message) thread = Synchronized.change global_state - (fn state as {manager, timeout_heap, active, canceling, messages, store} => + (fn state as {manager, timeout_heap, active, canceling, messages} => (case lookup_thread active thread of SOME (tool, _, _, desc as (worker, its_desc)) => let @@ -75,50 +67,30 @@ val message' = (worker, its_desc ^ (if message = "" then "" else "\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)) - in make_state manager timeout_heap active' canceling' messages' store' end + in make_state manager timeout_heap active' canceling' messages' end | NONE => state)) val min_wait_time = seconds 0.3 val max_wait_time = seconds 10.0 -fun replace_all bef aft = - let - fun aux seen "" = String.implode (rev seen) - | aux seen s = - if String.isPrefix bef s then - aux seen "" ^ aft ^ aux [] (unprefix bef s) - else - aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE)) - in aux [] end - -(* 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 = space_explode "\000" o replace_all "\n\n" "\000" - fun print_new_messages () = Synchronized.change_result global_state - (fn {manager, timeout_heap, active, canceling, messages, store} => + (fn {manager, timeout_heap, active, canceling, messages} => messages |> List.partition (fn (urgent, _) => (null active andalso null canceling) orelse urgent) - ||> (fn postponed_messages => - make_state manager timeout_heap active canceling - postponed_messages store)) + ||> make_state manager timeout_heap active canceling) |> map (fn (_, (tool, (worker, work))) => ((tool, work), worker)) |> AList.group (op =) |> List.app (fn ((_, ""), _) => () | ((tool, work), workers) => tool ^ ": " ^ implode_message (workers |> sort_distinct string_ord, work) - |> break_into_chunks - |> List.app writeln) + |> writeln) fun check_thread_manager () = Synchronized.change global_state - (fn state as {manager, timeout_heap, active, canceling, messages, store} => + (fn state as {manager, timeout_heap, active, canceling, messages} => if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state else let val manager = SOME (make_thread false (fn () => let @@ -128,7 +100,7 @@ | SOME (time, _) => time) (*action: find threads whose timeout is reached, and interrupt canceling threads*) - fun action {manager, timeout_heap, active, canceling, messages, store} = + fun action {manager, timeout_heap, active, canceling, messages} = let val (timeout_threads, timeout_heap') = Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap in @@ -138,14 +110,14 @@ let val _ = List.app (Simple_Thread.interrupt_unsynchronized o #1) canceling val canceling' = filter (Thread.isActive o #1) canceling - val state' = make_state manager timeout_heap' active canceling' messages store + val state' = make_state manager timeout_heap' active canceling' messages in SOME (map #2 timeout_threads, state') end end in while Synchronized.change_result global_state - (fn state as {timeout_heap, active, canceling, messages, store, ...} => + (fn state as {timeout_heap, active, canceling, messages, ...} => if null active andalso null canceling andalso null messages - then (false, make_state NONE timeout_heap active canceling messages store) + then (false, make_state NONE timeout_heap active canceling messages) else (true, state)) do (Synchronized.timed_access global_state @@ -156,15 +128,15 @@ (* give threads some time to respond to interrupt *) OS.Process.sleep min_wait_time) end)) - in make_state manager timeout_heap active canceling messages store end) + in make_state manager timeout_heap active canceling messages end) fun register tool birth_time death_time desc thread = (Synchronized.change global_state - (fn {manager, timeout_heap, active, canceling, messages, store} => + (fn {manager, timeout_heap, active, canceling, messages} => let val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active - val state' = make_state manager timeout_heap' active' canceling messages store + val state' = make_state manager timeout_heap' active' canceling messages in state' end); check_thread_manager ()) @@ -177,60 +149,7 @@ in unregister (f ()) self end); ()) -fun kill_threads tool das_wort_worker = Synchronized.change global_state - (fn {manager, timeout_heap, active, canceling, messages, store} => - let - val killing = - map_filter (fn (th, (tool', _, _, desc)) => - 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 writeln ("Interrupted active " ^ das_wort_worker ^ "s.") - in state' end) - -fun str_of_time time = string_of_int (Time.toSeconds time) ^ " s" - fun has_running_threads tool = exists (fn (_, (tool', _, _, _)) => tool' = tool) (#active (Synchronized.value global_state)) -fun running_threads tool das_wort_worker = - let - val {active, canceling, ...} = Synchronized.value global_state - val now = Time.now () - fun running_info (_, (tool', birth_time, death_time, desc)) = - if tool' = tool then - SOME ("Running: " ^ str_of_time (Time.- (now, birth_time)) ^ " -- " ^ - str_of_time (Time.- (death_time, now)) ^ " to live:\n" ^ op ^ desc) - else - NONE - fun canceling_info (_, (tool', death_time, desc)) = - if tool' = tool then - SOME ("Trying to interrupt " ^ das_wort_worker ^ " since " ^ - str_of_time (Time.- (now, death_time)) ^ ":\n" ^ op ^ desc) - else - NONE - val running = - case map_filter running_info active of - [] => ["No " ^ das_wort_worker ^ "s running."] - | ss => "Running " ^ das_wort_worker ^ "s" :: ss - val interrupting = - case map_filter canceling_info canceling of - [] => [] - | ss => "Interrupting " ^ das_wort_worker ^ "s" :: ss - in writeln (space_implode "\n\n" (running @ interrupting)) end - -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 " ^ das_wort_worker ^ " messages" ^ - (if length tool_store <= limit then ":" - else " (" ^ string_of_int limit ^ " displayed):") - val ss = tool_store |> chop limit |> #1 |> map (op ^ o snd) - in List.app writeln (header :: maps break_into_chunks ss) end - end; diff -r d84b4d39bce1 -r 69022bbcd012 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Oct 02 23:22:49 2015 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Sat Oct 03 18:38:25 2015 +0200 @@ -60,10 +60,6 @@ ordered_outcome_codes |> the_default unknownN -fun prover_description verbose name num_facts = - (quote name, - if verbose then " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts else "") - fun is_metis_method (Metis_Method _) = true | is_metis_method _ = false @@ -117,16 +113,14 @@ end end -fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, minimize, timeout, - preplay_timeout, expect, ...}) mode writeln_result only learn +fun launch_prover (params as {debug, verbose, spy, max_facts, minimize, timeout, preplay_timeout, + expect, ...}) mode writeln_result only learn {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name = let val ctxt = Proof.context_of state val hard_timeout = time_mult 3.0 timeout val _ = spying spy (fn () => (state, subgoal, name, "Launched")); - val birth_time = Time.now () - val death_time = Time.+ (birth_time, hard_timeout) val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt name) val num_facts = length facts |> not only ? Integer.min max_facts @@ -214,34 +208,23 @@ if expect = "" orelse outcome_code = expect orelse not (is_prover_installed ctxt name) then () - else if blocking then + else error ("Unexpected outcome: " ^ quote outcome_code ^ ".") - else - warning ("Unexpected outcome: " ^ quote outcome_code ^ "."); in (outcome_code, message) end in if mode = Auto_Try then let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in (outcome_code, if outcome_code = someN then [message ()] else []) end - else if blocking then + else let val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go () val outcome = if outcome_code = someN orelse mode = Normal then quote name ^ ": " ^ message () else "" val _ = - if outcome <> "" andalso is_some writeln_result then - the writeln_result outcome - else - outcome - |> Async_Manager_Legacy.break_into_chunks - |> List.app writeln + if outcome <> "" andalso is_some writeln_result then the writeln_result outcome + else writeln outcome in (outcome_code, []) end - else - (Async_Manager_Legacy.thread SledgehammerN birth_time death_time - (prover_description verbose name num_facts) - ((fn (outcome_code, message) => (verbose orelse outcome_code = someN, message ())) o go); - (unknownN, [])) end val auto_try_max_facts_divisor = 2 (* FUDGE *) @@ -257,14 +240,13 @@ cat_lines (map (fn (filter, facts) => (if filter = "" then "" else quote filter ^ ": ") ^ string_of_facts facts) factss) -fun run_sledgehammer (params as {verbose, spy, blocking, provers, max_facts, ...}) mode - writeln_result i (fact_override as {only, ...}) state = +fun run_sledgehammer (params as {verbose, spy, provers, max_facts, ...}) mode writeln_result i + (fact_override as {only, ...}) state = if null provers then error "No prover is set." else (case subgoal_count state of - 0 => - ((if blocking then error else writeln) "No subgoal!"; (false, (noneN, []))) + 0 => (error "No subgoal!"; (false, (noneN, []))) | n => let val _ = Proof.assert_backward state @@ -278,7 +260,6 @@ val css = clasimpset_rule_table_of ctxt val all_facts = nearly_all_facts ctxt ho_atp fact_override keywords css chained hyp_ts concl_t - val _ = () |> not blocking ? kill_provers val _ = (case find_first (not o is_prover_supported ctxt) provers of SOME name => error ("No such prover: " ^ name ^ ".") @@ -325,13 +306,13 @@ else (learn chained; provers - |> (if blocking then Par_List.map else map) (launch problem #> fst) + |> Par_List.map (launch problem #> fst) |> max_outcome_code |> rpair []) end in - (if blocking then launch_provers () - else (Future.fork launch_provers; (unknownN, []))) - handle TimeLimit.TimeOut => (print "Sledgehammer ran out of time."; (unknownN, [])) + launch_provers () + handle TimeLimit.TimeOut => + (print "Sledgehammer ran out of time."; (unknownN, [])) end |> `(fn (outcome_code, _) => outcome_code = someN)) diff -r d84b4d39bce1 -r 69022bbcd012 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Oct 02 23:22:49 2015 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Sat Oct 03 18:38:25 2015 +0200 @@ -32,11 +32,7 @@ val z3N = "z3" val runN = "run" -val messagesN = "messages" val supported_proversN = "supported_provers" -val kill_allN = "kill_all" -val running_proversN = "running_provers" -val running_learnersN = "running_learners" val refresh_tptpN = "refresh_tptp" (** Sledgehammer commands **) @@ -59,7 +55,6 @@ ("verbose", "false"), ("overlord", "false"), ("spy", "false"), - ("blocking", "false"), ("type_enc", "smart"), ("strict", "false"), ("lam_trans", "smart"), @@ -88,7 +83,6 @@ ("quiet", "verbose"), ("no_overlord", "overlord"), ("dont_spy", "spy"), - ("non_blocking", "blocking"), ("non_strict", "strict"), ("no_uncurried_aliases", "uncurried_aliases"), ("dont_learn", "learn"), @@ -248,8 +242,6 @@ val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose") val overlord = lookup_bool "overlord" val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy" - val blocking = - Isabelle_Process.is_active () orelse mode <> Normal orelse debug orelse lookup_bool "blocking" val provers = lookup_string "provers" |> space_explode " " |> mode = Auto_Try ? single o hd val type_enc = if mode = Auto_Try then @@ -280,8 +272,8 @@ val preplay_timeout = lookup_time "preplay_timeout" val expect = lookup_string "expect" in - {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = blocking, - provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans, + {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers, + type_enc = type_enc, strict = strict, lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter, max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, @@ -330,14 +322,8 @@ ignore (run_sledgehammer (get_params Normal thy override_params) Normal writeln_result i fact_override state) end - else if subcommand = messagesN then - messages opt_i else if subcommand = supported_proversN then supported_provers ctxt - else if subcommand = kill_allN then - (kill_provers (); kill_learners ()) - else if subcommand = running_proversN then - running_provers () else if subcommand = unlearnN then mash_unlearn () else if subcommand = learn_isarN orelse subcommand = learn_proverN orelse @@ -353,8 +339,6 @@ [("preplay_timeout", ["0"])])) fact_override (#facts (Proof.goal state)) (subcommand = learn_proverN orelse subcommand = relearn_proverN)) - else if subcommand = running_learnersN then - running_learners () else if subcommand = refresh_tptpN then refresh_systems_on_tptp () else @@ -418,7 +402,6 @@ ((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @ [("isar_proofs", [if isar_proofs_arg = "true" then "true" else "smart"]), ("try0", [try0_arg]), - ("blocking", ["true"]), ("debug", ["false"]), ("verbose", ["false"]), ("overlord", ["false"])]); diff -r d84b4d39bce1 -r 69022bbcd012 src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Fri Oct 02 23:22:49 2015 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Sat Oct 03 18:38:25 2015 +0200 @@ -76,7 +76,7 @@ fun postprocess_isar_proof_remove_show_stuttering (Proof (fix, assms, steps)) = let fun process_steps [] = [] - | process_steps (steps as [Prove ([], [], l1, t1, subs1, facts1, meths1, comment1), + | process_steps (steps as [Prove ([], [], _, t1, subs1, facts1, meths1, comment1), Prove ([Show], [], l2, t2, _, _, _, comment2)]) = if t1 aconv t2 then [Prove ([Show], [], l2, t2, subs1, facts1, meths1, comment1 ^ comment2)] else steps diff -r d84b4d39bce1 -r 69022bbcd012 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Oct 02 23:22:49 2015 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sat Oct 03 18:38:25 2015 +0200 @@ -81,8 +81,6 @@ val mash_weight : real val relevant_facts : Proof.context -> params -> string -> int -> fact_override -> term list -> term -> raw_fact list -> (string * fact list) list - val kill_learners : unit -> unit - val running_learners : unit -> unit end; structure Sledgehammer_MaSh : SLEDGEHAMMER_MASH = @@ -96,6 +94,8 @@ open Sledgehammer_Prover_Minimize open Sledgehammer_MePo +val anonymous_proof_prefix = "." + val trace = Attrib.setup_config_bool @{binding sledgehammer_mash_trace} (K false) val duplicates = Attrib.setup_config_bool @{binding sledgehammer_fact_duplicates} (K false) @@ -1091,31 +1091,36 @@ |> drop (length old_facts) end -fun maximal_wrt_graph G keys = - let - val tab = Symtab.empty |> fold (fn name => Symtab.default (name, ())) keys +fun maximal_wrt_graph _ [] = [] + | maximal_wrt_graph G keys = + if can (Graph.get_node G o the_single) keys then + keys + else + let + val tab = Symtab.empty |> fold (fn name => Symtab.default (name, ())) keys - fun insert_new seen name = not (Symtab.defined seen name) ? insert (op =) name + fun insert_new seen name = not (Symtab.defined seen name) ? insert (op =) name - fun num_keys keys = Graph.Keys.fold (K (Integer.add 1)) keys 0 + fun num_keys keys = Graph.Keys.fold (K (Integer.add 1)) keys 0 - fun find_maxes _ (maxs, []) = map snd maxs - | find_maxes seen (maxs, new :: news) = - find_maxes (seen |> num_keys (Graph.imm_succs G new) > 1 ? Symtab.default (new, ())) - (if Symtab.defined tab new then - let - val newp = Graph.all_preds G [new] - fun is_ancestor x yp = member (op =) yp x - val maxs = maxs |> filter (fn (_, max) => not (is_ancestor max newp)) - in - if exists (is_ancestor new o fst) maxs then (maxs, news) - else ((newp, new) :: filter_out (fn (_, max) => is_ancestor max newp) maxs, news) - end - else - (maxs, Graph.Keys.fold (insert_new seen) (Graph.imm_preds G new) news)) - in - find_maxes Symtab.empty ([], Graph.maximals G) - end + fun find_maxes _ (maxs, []) = map snd maxs + | find_maxes seen (maxs, new :: news) = + find_maxes (seen |> num_keys (Graph.imm_succs G new) > 1 ? Symtab.default (new, ())) + (if Symtab.defined tab new then + let + val newp = Graph.all_preds G [new] + fun is_ancestor x yp = member (op =) yp x + val maxs = maxs |> filter (fn (_, max) => not (is_ancestor max newp)) + in + if exists (is_ancestor new o fst) maxs then (maxs, news) + else ((newp, new) :: filter_out (fn (_, max) => is_ancestor max newp) maxs, news) + end + else + (maxs, Graph.Keys.fold (insert_new seen) (Graph.imm_preds G new) news)) + in + find_maxes Symtab.empty ([], + G |> Graph.restrict (not o String.isPrefix anonymous_proof_prefix) |> Graph.maximals) + end fun maximal_wrt_access_graph _ _ [] = [] | maximal_wrt_access_graph ctxt access_G ((fact as (_, th)) :: facts) = @@ -1261,8 +1266,9 @@ Async_Manager_Legacy.thread MaShN birth_time death_time desc task end -fun learned_proof_name () = - Date.fmt ".%Y%m%d.%H%M%S." (Date.fromTimeLocal (Time.now ())) ^ serial_string () +fun anonymous_proof_name () = + Date.fmt (anonymous_proof_prefix ^ "%Y%m%d.%H%M%S.") (Date.fromTimeLocal (Time.now ())) ^ + serial_string () fun mash_learn_proof ctxt ({timeout, ...} : params) t facts used_ths = if not (null used_ths) andalso is_mash_enabled () then @@ -1280,7 +1286,7 @@ |> filter (is_fact_in_graph ctxt access_G) |> map (nickname_of_thm ctxt) - val name = learned_proof_name () + val name = anonymous_proof_name () val (access_G', xtabs', rev_learns) = add_node Automatic_Proof name parents feats deps (access_G, xtabs, []) @@ -1600,7 +1606,4 @@ | _ => [(effective_fact_filter, mesh)]) end -fun kill_learners () = Async_Manager_Legacy.kill_threads MaShN "learner" -fun running_learners () = Async_Manager_Legacy.running_threads MaShN "learner" - end; diff -r d84b4d39bce1 -r 69022bbcd012 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Oct 02 23:22:49 2015 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Sat Oct 03 18:38:25 2015 +0200 @@ -22,7 +22,6 @@ verbose : bool, overlord : bool, spy : bool, - blocking : bool, provers : string list, type_enc : string option, strict : bool, @@ -73,11 +72,7 @@ ((''a * stature) * 'b) list val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context -> Proof.context - val supported_provers : Proof.context -> unit - val kill_provers : unit -> unit - val running_provers : unit -> unit - val messages : int option -> unit end; structure Sledgehammer_Prover : SLEDGEHAMMER_PROVER = @@ -111,7 +106,6 @@ verbose : bool, overlord : bool, spy : bool, - blocking : bool, provers : string list, type_enc : string option, strict : bool, @@ -201,8 +195,4 @@ writeln ("Supported provers: " ^ commas (local_provers @ remote_provers) ^ ".") end -fun kill_provers () = Async_Manager_Legacy.kill_threads SledgehammerN "prover" -fun running_provers () = Async_Manager_Legacy.running_threads SledgehammerN "prover" -val messages = Async_Manager_Legacy.thread_messages SledgehammerN "prover" - end; diff -r d84b4d39bce1 -r 69022bbcd012 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Fri Oct 02 23:22:49 2015 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Sat Oct 03 18:38:25 2015 +0200 @@ -88,8 +88,8 @@ val facts = facts |> maps (fn (n, ths) => map (pair n) ths) val params = - {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = true, - provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans, + {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers, + type_enc = type_enc, strict = strict, lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE, max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances,