aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-12-18 18:57:34 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-12-18 18:57:34 +0100
commit6af0969228e57c611e5a0876efe613055de342cd (patch)
treecfeb33115bb53bc41c588cf75dc70ef515eceff9 /plugins
parent3690e568a36f8b418ec9c253a3188403f53021ba (diff)
parent6734614d8ace6860e3deb1861611ba4b012cfae1 (diff)
Merge PR #6380: Add tactics to reset and display the Ltac profile
Diffstat (limited to 'plugins')
-rw-r--r--plugins/ltac/profile_ltac_tactics.ml421
1 files changed, 20 insertions, 1 deletions
diff --git a/plugins/ltac/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.ml4
index f09566063..58e3a3a57 100644
--- a/plugins/ltac/profile_ltac_tactics.ml4
+++ b/plugins/ltac/profile_ltac_tactics.ml4
@@ -18,6 +18,15 @@ DECLARE PLUGIN "ltac_plugin"
let tclSET_PROFILING b =
Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> set_profiling b))
+let tclRESET_PROFILE =
+ Proofview.tclLIFT (Proofview.NonLogical.make reset_profile)
+
+let tclSHOW_PROFILE ~cutoff =
+ Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> print_results ~cutoff))
+
+let tclSHOW_PROFILE_TACTIC s =
+ Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> print_results_tactic s))
+
TACTIC EXTEND start_ltac_profiling
| [ "start" "ltac" "profiling" ] -> [ tclSET_PROFILING true ]
END
@@ -26,8 +35,18 @@ TACTIC EXTEND stop_ltac_profiling
| [ "stop" "ltac" "profiling" ] -> [ tclSET_PROFILING false ]
END
+TACTIC EXTEND reset_ltac_profile
+| [ "reset" "ltac" "profile" ] -> [ tclRESET_PROFILE ]
+END
+
+TACTIC EXTEND show_ltac_profile
+| [ "show" "ltac" "profile" ] -> [ tclSHOW_PROFILE ~cutoff:!Flags.profile_ltac_cutoff ]
+| [ "show" "ltac" "profile" "cutoff" int(n) ] -> [ tclSHOW_PROFILE ~cutoff:(float_of_int n) ]
+| [ "show" "ltac" "profile" string(s) ] -> [ tclSHOW_PROFILE_TACTIC s ]
+END
+
VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF
- [ "Reset" "Ltac" "Profile" ] -> [ reset_profile() ]
+ [ "Reset" "Ltac" "Profile" ] -> [ reset_profile () ]
END
VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY