--- 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.
--- 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
--- 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}
--- 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 *}
--- 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
--- 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
--- 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) =
--- 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;
--- 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))
--- 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"])]);
--- 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
--- 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;
--- 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;
--- 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,