--- a/NEWS Fri Jan 04 21:16:08 2013 +0100
+++ b/NEWS Fri Jan 04 21:24:47 2013 +0100
@@ -143,7 +143,7 @@
Sledgehammer manual for details.
- Polished Isar proofs generated with "isar_proofs" option.
- Rationalized type encodings ("type_enc" option).
- - Renamed "kill_provers" subcommand to "kill".
+ - Renamed "kill_provers" subcommand to "kill_all".
- Renamed options:
isar_proof ~> isar_proofs
isar_shrink_factor ~> isar_shrink
--- a/src/Doc/Sledgehammer/document/root.tex Fri Jan 04 21:16:08 2013 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Fri Jan 04 21:24:47 2013 +0100
@@ -675,7 +675,7 @@
currently running automatic provers, including elapsed runtime and remaining
time until timeout.
-\item[\labelitemi] \textbf{\textit{kill}:} Terminates all running
+\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
@@ -711,9 +711,6 @@
\item[\labelitemi] \textbf{\textit{running\_learners}:} Prints information about
currently running machine learners, including elapsed runtime and remaining
time until timeout.
-
-\item[\labelitemi] \textbf{\textit{kill\_learners}:} Terminates all running
-machine learners.
\end{enum}
Sledgehammer's behavior can be influenced by various \qty{options}, which can be
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Fri Jan 04 21:16:08 2013 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Fri Jan 04 21:24:47 2013 +0100
@@ -451,6 +451,7 @@
fun size_matters_for _ Ts = not (forall
(fn Type (tyco, []) => is_some (try (unprefix "Enum.finite") tyco) | _ => false) Ts)
+ (*FIXME eliminate dynamic name reference*)
val test_goals =
Quickcheck_Common.generator_test_goal_terms ("random", (size_matters_for, compile_generator_expr));
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jan 04 21:16:08 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jan 04 21:24:47 2013 +0100
@@ -37,7 +37,7 @@
val minN = "min"
val messagesN = "messages"
val supported_proversN = "supported_provers"
-val killN = "kill"
+val kill_allN = "kill_all"
val running_proversN = "running_provers"
val running_learnersN = "running_learners"
val refresh_tptpN = "refresh_tptp"
@@ -395,7 +395,7 @@
messages opt_i
else if subcommand = supported_proversN then
supported_provers ctxt
- else if subcommand = killN then
+ else if subcommand = kill_allN then
(kill_provers (); kill_learners ())
else if subcommand = running_proversN then
running_provers ()
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jan 04 21:16:08 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jan 04 21:24:47 2013 +0100
@@ -307,7 +307,7 @@
local
-val version = "*** MaSh version 20121227a ***"
+val version = "*** MaSh version 20130104a ***"
exception Too_New of unit
@@ -401,29 +401,25 @@
(*** Isabelle helpers ***)
-fun parent_of_local_thm th =
- let
- val thy = th |> Thm.theory_of_thm
- val facts = thy |> Global_Theory.facts_of
- val space = facts |> Facts.space_of
- fun id_of s = #id (Name_Space.the_entry space s)
- fun max_id (s', _) (s, id) =
- let val id' = id_of s' in if id > id' then (s, id) else (s', id') end
- in ("", ~1) |> Facts.fold_static max_id facts |> fst end
+val local_prefix = "local" ^ Long_Name.separator
-val local_prefix = "local" ^ Long_Name.separator
+fun elided_backquote_thm threshold th =
+ elide_string threshold
+ (backquote_thm (Proof_Context.init_global (Thm.theory_of_thm th)) th)
fun nickname_of_thm th =
if Thm.has_name_hint th then
let val hint = Thm.get_name_hint th in
- (* FIXME: There must be a better way to detect local facts. *)
+ (* There must be a better way to detect local facts. *)
case try (unprefix local_prefix) hint of
SOME suf =>
- parent_of_local_thm th ^ Long_Name.separator ^ Long_Name.separator ^ suf
+ Context.theory_name (Thm.theory_of_thm th) ^ Long_Name.separator ^
+ Long_Name.separator ^ suf ^ Long_Name.separator ^
+ elided_backquote_thm 50 th
| NONE => hint
end
else
- backquote_thm (Proof_Context.init_global (Thm.theory_of_thm th)) th
+ elided_backquote_thm 200 th
fun find_suggested_facts suggs facts =
let
@@ -486,10 +482,8 @@
val skos_feature = ("skos", 2.0 (* FUDGE *))
fun theory_ord p =
- if Theory.eq_thy p then
- EQUAL
- else if Theory.subthy p then
- LESS
+ if Theory.subthy p then
+ if Theory.eq_thy p then EQUAL else LESS
else if Theory.subthy (swap p) then
GREATER
else case int_ord (pairself (length o Theory.ancestors_of) p) of
@@ -1055,7 +1049,7 @@
(* Generate more suggestions than requested, because some might be thrown out
later for various reasons. *)
-fun generous_max_facts max_facts = max_facts + Int.min (50, max_facts)
+fun generous_max_facts max_facts = max_facts + Int.min (50, max_facts div 2)
(* The threshold should be large enough so that MaSh doesn't kick in for Auto
Sledgehammer and Try. *)