diff options
author | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-04-23 01:14:49 -0400 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-05-04 13:17:23 +0200 |
commit | 2a295131a1a72dd56e6e7abdeaeca07b1b69ab6d (patch) | |
tree | f23c8dc1ce9238ebf5cb05f61f57aa21dd8ee8ca | |
parent | f19d0c7baf91fb410de77baed391b0a16db9c4e2 (diff) |
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.
-rw-r--r-- | doc/refman/RefMan-oth.tex | 3 | ||||
-rw-r--r-- | intf/vernacexpr.mli | 1 | ||||
-rw-r--r-- | lib/pp.ml | 21 | ||||
-rw-r--r-- | lib/pp.mli | 2 | ||||
-rw-r--r-- | parsing/g_vernac.ml4 | 1 | ||||
-rw-r--r-- | printing/ppvernac.ml | 2 | ||||
-rw-r--r-- | stm/stm.ml | 4 | ||||
-rw-r--r-- | stm/texmacspp.ml | 3 | ||||
-rw-r--r-- | stm/vernac_classifier.ml | 2 | ||||
-rw-r--r-- | toplevel/vernac.ml | 2 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 3 |
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 *) @@ -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; |