diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-07-07 21:34:49 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-07-07 21:34:49 +0200 |
commit | a3503c0aca07f5e7f5785faa7b76123a02ecc2af (patch) | |
tree | ae07277425e50314b0c341752a11af3055a01907 | |
parent | abad0a15ac44cb5b53b87382bb4d587d9800a0f6 (diff) |
Revert "time tac" (committed by mistake).
This reverts commit abad0a15ac44cb5b53b87382bb4d587d9800a0f6.
-rw-r--r-- | intf/tacexpr.mli | 1 | ||||
-rw-r--r-- | lib/system.ml | 16 | ||||
-rw-r--r-- | lib/system.mli | 2 | ||||
-rw-r--r-- | parsing/g_ltac.ml4 | 1 | ||||
-rw-r--r-- | printing/pptactic.ml | 3 | ||||
-rw-r--r-- | proofs/proofview.ml | 13 | ||||
-rw-r--r-- | proofs/proofview.mli | 3 | ||||
-rw-r--r-- | proofs/proofview_monad.mli | 1 | ||||
-rw-r--r-- | tactics/tacintern.ml | 2 | ||||
-rw-r--r-- | tactics/tacinterp.ml | 1 | ||||
-rw-r--r-- | tactics/tacsubst.ml | 1 | ||||
-rw-r--r-- | tactics/tacticals.ml | 3 | ||||
-rw-r--r-- | tactics/tacticals.mli | 1 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 6 |
14 files changed, 5 insertions, 49 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index e64dcb62c..530213b7c 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -209,7 +209,6 @@ and ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr = ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr | TacDo of int or_var * ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr | TacTimeout of int or_var * ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr - | TacTime of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr | TacRepeat of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr | TacProgress of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr | TacShowHyps of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr diff --git a/lib/system.ml b/lib/system.ml index 4188eb2b4..6c357ee36 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -279,19 +279,3 @@ let fmt_time_difference (startreal,ustart,sstart) (stopreal,ustop,sstop) = str "," ++ real (round (sstop -. sstart)) ++ str "s" ++ str ")" - -let with_time time f x = - let tstart = get_time() in - let msg = if time then "" else "Finished transaction in " in - try - let y = f x in - let tend = get_time() in - let msg2 = if time then "" else " (successful)" in - msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); - y - with e -> - let tend = get_time() in - let msg = if time then "" else "Finished failing transaction in " in - let msg2 = if time then "" else " (failure)" in - msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); - raise e diff --git a/lib/system.mli b/lib/system.mli index 9cfb1456f..2e286a40c 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -67,5 +67,3 @@ type time val get_time : unit -> time val time_difference : time -> time -> float (** in seconds *) val fmt_time_difference : time -> time -> Pp.std_ppcmds - -val with_time : bool -> ('a -> 'b) -> 'a -> 'b diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index fa352f8bf..f70a865d7 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -64,7 +64,6 @@ GEXTEND Gram [ IDENT "try"; ta = tactic_expr -> TacTry ta | IDENT "do"; n = int_or_var; ta = tactic_expr -> TacDo (n,ta) | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> TacTimeout (n,ta) - | IDENT "time"; ta = tactic_expr -> TacTime ta | IDENT "repeat"; ta = tactic_expr -> TacRepeat ta | IDENT "progress"; ta = tactic_expr -> TacProgress ta | IDENT "once"; ta = tactic_expr -> TacOnce ta diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 9df9446c3..f6c25d069 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -865,9 +865,6 @@ let rec pr_tac inherited tac = hov 1 (str "timeout " ++ pr_or_var int n ++ spc () ++ pr_tac (ltactical,E) t), ltactical - | TacTime t -> - hov 1 (str "time " ++ pr_tac (ltactical,E) t), - ltactical | TacRepeat t -> hov 1 (str "repeat" ++ spc () ++ pr_tac (ltactical,E) t), ltactical diff --git a/proofs/proofview.ml b/proofs/proofview.ml index da1937ef3..c478bd663 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -579,19 +579,6 @@ let tclTIMEOUT n t = Proof.ret res | Util.Inr e -> tclZERO e -let tclTIME t = - let (>>=) = Proof.bind in - let (>>) = Proof.seq in - let t = Proof.lift (Proofview_monad.NonLogical.ret ()) >> t in - Proof.current >>= fun env -> - Proof.get >>= fun initial -> - Proof.lift begin - Proofview_monad.NonLogical.time !Flags.time (Proof.run t env initial) - end >>= function ((res,s),m) -> - Proof.set s >> - Proof.put m >> - Proof.ret res - let mark_as_unsafe = Proof.put (false,([],[])) diff --git a/proofs/proofview.mli b/proofs/proofview.mli index df833a04f..6a2d81511 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -261,9 +261,6 @@ exception Timeout In case of timeout if fails with [tclZERO Timeout]. *) val tclTIMEOUT : int -> 'a tactic -> 'a tactic -(** [tclTIME t] displays time for each atomic call to t *) -val tclTIME : 'a tactic -> 'a tactic - (** [mark_as_unsafe] signals that the current tactic is unsafe. *) val mark_as_unsafe : unit tactic diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli index 8139d3026..4d4e4470c 100644 --- a/proofs/proofview_monad.mli +++ b/proofs/proofview_monad.mli @@ -38,7 +38,6 @@ module NonLogical : sig val raise : exn -> 'a t val catch : 'a t -> (exn -> 'a t) -> 'a t val timeout : int -> 'a t -> 'a t - val time : bool -> 'a t -> 'a t (* [run] performs effects. *) diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 033e00433..f68f75359 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -613,8 +613,6 @@ and intern_tactic_seq onlytac ist = function | TacRepeat tac -> ist.ltacvars, TacRepeat (intern_pure_tactic ist tac) | TacTimeout (n,tac) -> ist.ltacvars, TacTimeout (intern_or_var ist n,intern_tactic onlytac ist tac) - | TacTime tac -> - ist.ltacvars, TacTime (intern_tactic onlytac ist tac) | TacOr (tac1,tac2) -> ist.ltacvars, TacOr (intern_pure_tactic ist tac1,intern_pure_tactic ist tac2) | TacOnce tac -> diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index b70f21431..c749e2d72 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1023,7 +1023,6 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacThens (t1,tl) -> Tacticals.New.tclTHENS (interp_tactic ist t1) (List.map (interp_tactic ist) tl) | TacDo (n,tac) -> Tacticals.New.tclDO (interp_int_or_var ist n) (interp_tactic ist tac) | TacTimeout (n,tac) -> Tacticals.New.tclTIMEOUT (interp_int_or_var ist n) (interp_tactic ist tac) - | TacTime tac -> Tacticals.New.tclTIME (interp_tactic ist tac) | TacTry tac -> Tacticals.New.tclTRY (interp_tactic ist tac) | TacRepeat tac -> Tacticals.New.tclREPEAT (interp_tactic ist tac) | TacOr (tac1,tac2) -> diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 8ab63c161..4dd4b0aa8 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -230,7 +230,6 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with TacThens (subst_tactic subst t, List.map (subst_tactic subst) tl) | TacDo (n,tac) -> TacDo (n,subst_tactic subst tac) | TacTimeout (n,tac) -> TacTimeout (n,subst_tactic subst tac) - | TacTime tac -> TacTime (subst_tactic subst tac) | TacTry tac -> TacTry (subst_tactic subst tac) | TacInfo tac -> TacInfo (subst_tactic subst tac) | TacRepeat tac -> TacRepeat (subst_tactic subst tac) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 267a34754..fcce6e5eb 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -467,9 +467,6 @@ module New = struct | e -> Proofview.tclZERO e end - let tclTIME t = - Proofview.tclTIME t - let nthDecl m gl = let hyps = Proofview.Goal.hyps gl in try diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 705a7e2cc..48fd44b4a 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -212,7 +212,6 @@ module New : sig val tclWITHHOLES : bool -> ('a -> unit tactic) -> Evd.evar_map -> 'a -> unit tactic val tclTIMEOUT : int -> unit tactic -> unit tactic - val tclTIME : 'a tactic -> 'a tactic val nLastDecls : [ `NF ] Proofview.Goal.t -> int -> named_context diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 5e829a2d9..1d05f4e62 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1965,7 +1965,11 @@ let interp ?(verbosely=true) ?proof (loc,c) = current_timeout := Some n; aux ?locality ?polymorphism isprogcmd v | VernacTime v -> - System.with_time !Flags.time (aux ?locality ?polymorphism isprogcmd) v; + let tstart = System.get_time() in + aux_list ?locality ?polymorphism isprogcmd v; + let tend = System.get_time() in + let msg = if !Flags.time then "" else "Finished transaction in " in + msg_info (str msg ++ System.fmt_time_difference tstart tend) | VernacLoad (_,fname) -> vernac_load (aux false) fname | c -> check_vernac_supports_locality c locality; |