diff options
Diffstat (limited to 'ltac/profile_ltac_tactics.ml4')
-rw-r--r-- | ltac/profile_ltac_tactics.ml4 | 40 |
1 files changed, 40 insertions, 0 deletions
diff --git a/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4 new file mode 100644 index 00000000..8cb76d81 --- /dev/null +++ b/ltac/profile_ltac_tactics.ml4 @@ -0,0 +1,40 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i camlp4deps: "grammar/grammar.cma" i*) + +(** Ltac profiling entrypoints *) + +open Profile_ltac +open Stdarg + +DECLARE PLUGIN "profile_ltac_plugin" + +let tclSET_PROFILING b = + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> set_profiling b)) + +TACTIC EXTEND start_ltac_profiling +| [ "start" "ltac" "profiling" ] -> [ tclSET_PROFILING true ] +END + +TACTIC EXTEND stop_profiling +| [ "stop" "ltac" "profiling" ] -> [ tclSET_PROFILING false ] +END + +VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF + [ "Reset" "Ltac" "Profile" ] -> [ reset_profile() ] +END + +VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY +| [ "Show" "Ltac" "Profile" ] -> [ print_results ~cutoff:!Flags.profile_ltac_cutoff ] +| [ "Show" "Ltac" "Profile" "CutOff" int(n) ] -> [ print_results ~cutoff:(float_of_int n) ] +END + +VERNAC COMMAND EXTEND ShowLtacProfileTactic CLASSIFIED AS QUERY + [ "Show" "Ltac" "Profile" string(s) ] -> [ print_results_tactic s ] +END |