1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40

(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
(*   \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