Add a [Redirect] vernacular command

The command [Redirect "filename" (...)] redirects all the output of
[(...)]  to file "filename.out". This is useful for storing the results of
an [Eval compute], for redirecting the results of a large search, for
automatically generating traces of interesting developments, and so on.

11 files changed, 40 insertions, 4 deletions

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 0a28a93a4..aa0291a23 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -877,6 +877,9 @@ go();;
 This command executes the vernacular command \textrm{\textsl{command}}
 and display the time needed to execute it.
 
+\subsection[\tt Time \textrm{\textsl{command}}.]{\tt Redirect "\textrm{\textsl{file}}" \textrm{\textsl{command}}.\comindex{Redirect}
+\label{redirect}}
+This command executes the vernacular command \textrm{\textsl{command}}, redirecting its output to ``\textrm{\textsl{file}}.out''.
 
 \subsection[\tt Timeout \textrm{\textsl{int}} \textrm{\textsl{command}}.]{\tt Timeout \textrm{\textsl{int}} \textrm{\textsl{command}}.\comindex{Timeout}
 \label{timeout}}
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 450b1af0f..d7b269a1d 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -273,6 +273,7 @@ type vernac_expr =
   (* Control *)
   | VernacLoad of verbose_flag * string
   | VernacTime of vernac_list
+  | VernacRedirect of string * vernac_list
   | VernacTimeout of int * vernac_expr
   | VernacFail of vernac_expr
   | VernacError of exn (* always fails *)
diff --git a/lib/pp.ml b/lib/pp.ml
index 9667f7270..30bc30a9a 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -448,6 +448,27 @@ let logger = ref std_logger
 let make_pp_emacs() = print_emacs:=true; logger:=emacs_logger
 let make_pp_nonemacs() = print_emacs:=false; logger := std_logger
 
+let ft_logger old_logger ft ~id level mesg = match level with
+  | Debug _ -> msgnl_with ft (debugbody mesg)
+  | Info -> msgnl_with ft (infobody mesg)
+  | Notice -> msgnl_with ft mesg
+  | Warning -> old_logger ~id:id level mesg
+  | Error -> old_logger ~id:id level mesg
+
+let with_output_to_file fname func input =
+  let old_logger = !logger in
+  let channel = open_out (String.concat "." [fname; "out"]) in
+  logger := ft_logger old_logger (Format.formatter_of_out_channel channel);
+  try
+    let output = func input in
+    logger := old_logger;
+    close_out channel;
+    output
+  with reraise ->
+    let reraise = Backtrace.add_backtrace reraise in
+    logger := old_logger;
+    close_out channel;
+    Exninfo.iraise reraise
 
 let feedback_id = ref (Feedback.Edit 0)
 let feedback_route = ref Feedback.default_route
diff --git a/lib/pp.mli b/lib/pp.mli
index e20e5ca82..3b1123a9d 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -12,6 +12,8 @@
 val make_pp_emacs:unit -> unit
 val make_pp_nonemacs:unit -> unit
 
+val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
+
 (** Pretty-printers. *)
 
 type std_ppcmds
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index cf7f6af28..09059b410 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -79,6 +79,7 @@ GEXTEND Gram
   GLOBAL: vernac gallina_ext tactic_mode noedit_mode subprf subgoal_command;
   vernac: FIRST
     [ [ IDENT "Time"; l = vernac_list -> VernacTime l
+      | IDENT "Redirect"; s = ne_string; l = vernac_list -> VernacRedirect (s, l)
       | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v)
       | IDENT "Fail"; v = vernac -> VernacFail v
 
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index c6b1b672f..832c08fe0 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -627,6 +627,8 @@ module Make
           )
         | VernacTime v ->
           return (keyword "Time" ++ spc() ++ pr_vernac_list v)
+        | VernacRedirect (s, v) ->
+          return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_list v)
         | VernacTimeout(n,v) ->
           return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac v)
         | VernacFail v ->
diff --git a/stm/stm.ml b/stm/stm.ml
index f36b757f2..977156475 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -86,7 +86,7 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } =
     | VernacResetName _ | VernacResetInitial | VernacBack _
     | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _
     | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true
-    | VernacTime el -> List.for_all (fun (_,e) -> internal_command e) el
+    | VernacTime el | VernacRedirect (_,el) -> List.for_all (fun (_,e) -> internal_command e) el
     | _ -> false in
   if internal_command expr then begin
     prerr_endline ("ignoring " ^ string_of_ppcmds(pr_vernac expr))
@@ -1472,7 +1472,7 @@ end = struct (* {{{ *)
     let e, etac, time, fail =
       let rec find time fail = function
         | VernacSolve(_,_,re,b) -> re, b, time, fail
-        | VernacTime [_,e] -> find true fail e
+        | VernacTime [_,e] | VernacRedirect (_,[_,e]) -> find true fail e
         | VernacFail e -> find time true e
         | _ -> errorlabstrm "Stm" (str"unsupported") in find false false e in
     Hooks.call Hooks.with_fail fail (fun () ->
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index 180f20ae8..9edc1f1c7 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -490,6 +490,9 @@ let rec tmpp v loc =
   | VernacTime l ->
       xmlApply loc (Element("time",[],[]) ::
                     List.map (fun(loc,e) ->tmpp e loc) l)
+  | VernacRedirect (s, l) ->
+      xmlApply loc (Element("redirect",["path", s],[]) ::
+                      List.map (fun(loc,e) ->tmpp e loc) l)
   | VernacTimeout (s,e) ->
       xmlApply loc (Element("timeout",["val",string_of_int s],[]) ::
                     [tmpp e loc])
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 783ff2e11..2b5eb8683 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -86,7 +86,7 @@ let rec classify_vernac e =
 	make_polymorphic (classify_vernac e)
       else classify_vernac e
     | VernacTimeout (_,e) -> classify_vernac e
-    | VernacTime e -> classify_vernac_list e
+    | VernacTime e | VernacRedirect (_, e) -> classify_vernac_list e
     | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
         (match classify_vernac e with
         | ( VtQuery _ | VtProofStep _ | VtSideff _
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index b3694d0e9..11cb047e0 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -27,7 +27,7 @@ let rec is_navigation_vernac = function
   | VernacBacktrack _
   | VernacBackTo _
   | VernacBack _ -> true
-  | VernacTime l ->
+  | VernacRedirect (_, l) | VernacTime l ->
     List.exists
       (fun (_,c) -> is_navigation_vernac c) l (* Time Back* is harmless *)
   | c -> is_deep_navigation_vernac c
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f33c71d8a..4300d5e24 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1849,6 +1849,7 @@ let interp ?proof locality poly c =
   | VernacLoad _ -> assert false
   | VernacFail _ -> assert false
   | VernacTime _ -> assert false
+  | VernacRedirect _ -> assert false
   | VernacTimeout _ -> assert false
   | VernacStm _ -> assert false
 
@@ -2127,6 +2128,8 @@ let interp ?(verbosely=true) ?proof (loc,c) =
     | VernacTimeout (n,v) ->
         current_timeout := Some n;
         aux ?locality ?polymorphism isprogcmd v
+    | VernacRedirect (s, v) ->
+         Pp.with_output_to_file s (aux_list ?locality ?polymorphism isprogcmd) v;
     | VernacTime v ->
         System.with_time !Flags.time
           (aux_list ?locality ?polymorphism isprogcmd) v;