# HG changeset patch
# User blanchet
# Date 1379709570 -7200
# Node ID 8d1a059ebcdbeccd02d15e503948ab4b81a89eef
# Parent  be91786f2419538930960145b79157da27c25b60
reduce the number of emitted MaSh commands (among others to facilitate debugging)

diff -r be91786f2419 -r 8d1a059ebcdb src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Fri Sep 20 22:39:30 2013 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Fri Sep 20 22:39:30 2013 +0200
@@ -1079,6 +1079,11 @@
 empirically found to be appropriate for the prover. Typical values range between
 50 and 1000.
 
+For the MaSh-related commands \textit{learn\_isar}, \textit{learn\_prover},
+\textit{relearn\_isar}, and \textit{relearn\_prover}, this option specifies the
+maximum number of facts from the background library that should be learned
+($\infty$ by default).
+
 \opdefault{fact\_thresholds}{float\_pair}{\upshape 0.45~0.85}
 Specifies the thresholds above which facts are considered relevant by the
 relevance filter. The first threshold is used for the first iteration of the
diff -r be91786f2419 -r 8d1a059ebcdb src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Sep 20 22:39:30 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Sep 20 22:39:30 2013 +0200
@@ -38,10 +38,10 @@
   sig
     val unlearn : Proof.context -> bool -> unit
     val learn :
-      Proof.context -> bool
+      Proof.context -> bool -> bool
       -> (string * string list * string list * string list) list -> unit
     val relearn :
-      Proof.context -> bool -> (string * string list) list -> unit
+      Proof.context -> bool -> bool -> (string * string list) list -> unit
     val query :
       Proof.context -> bool -> int
       -> (string * string list * string list * string list) list
@@ -278,19 +278,19 @@
     ()
   end
 
-fun learn _ _ [] = ()
-  | learn ctxt overlord learns =
+fun learn _ _ _ [] = ()
+  | learn ctxt overlord save learns =
     (trace_msg ctxt (fn () => "MaSh learn " ^
          elide_string 1000 (space_implode " " (map #1 learns)));
-     run_mash_tool ctxt overlord [] false (learns, str_of_learn)
-                   (K ()))
+     run_mash_tool ctxt overlord ([] |> save ? cons save_models_arg) false
+                   (learns, str_of_learn) (K ()))
 
-fun relearn _ _ [] = ()
-  | relearn ctxt overlord relearns =
+fun relearn _ _ _ [] = ()
+  | relearn ctxt overlord save relearns =
     (trace_msg ctxt (fn () => "MaSh relearn " ^
          elide_string 1000 (space_implode " " (map #1 relearns)));
-     run_mash_tool ctxt overlord [] false (relearns, str_of_relearn)
-                   (K ()))
+     run_mash_tool ctxt overlord ([] |> save ? cons save_models_arg) false
+                   (relearns, str_of_relearn) (K ()))
 
 fun query ctxt overlord max_suggs (query as (_, _, _, feats)) =
   (trace_msg ctxt (fn () => "MaSh query " ^ encode_features feats);
@@ -1054,8 +1054,7 @@
                 used_ths |> filter (is_fact_in_graph access_G)
                          |> map nickname_of_thm
             in
-              MaSh.learn ctxt overlord [(name, parents, feats, deps)];
-              MaSh.save ctxt overlord
+              MaSh.learn ctxt overlord true [(name, parents, feats, deps)]
             end);
         (true, "")
       end)
@@ -1116,9 +1115,8 @@
                   (false, SOME names, []) => SOME (map #1 learns @ names)
                 | _ => NONE
             in
-              MaSh.learn ctxt overlord (rev learns);
-              MaSh.relearn ctxt overlord relearns;
-              if save then MaSh.save ctxt overlord else ();
+              MaSh.learn ctxt overlord (save andalso null relearns) (rev learns);
+              MaSh.relearn ctxt overlord save relearns;
               {access_G = access_G, num_known_facts = num_known_facts,
                dirty = dirty}
             end