diff options
| -rw-r--r-- | Makefile.build | 2 | ||||
| -rw-r--r-- | Makefile.common | 5 | ||||
| -rw-r--r-- | lib/flags.ml | 1 | ||||
| -rw-r--r-- | lib/flags.mli | 2 | ||||
| -rw-r--r-- | ltac/ltac.mllib | 1 | ||||
| -rw-r--r-- | ltac/profile_ltac.ml (renamed from ltacprof/profile_ltac.ml) | 21 | ||||
| -rw-r--r-- | ltac/profile_ltac.mli (renamed from ltacprof/profile_ltac.mli) | 2 | ||||
| -rw-r--r-- | ltac/profile_ltac_tactics.ml4 | 9 | ||||
| -rw-r--r-- | ltacprof/ltacprof.mllib | 1 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 2 |
10 files changed, 20 insertions, 26 deletions
diff --git a/Makefile.build b/Makefile.build index 4f3077e5d..fc92507e6 100644 --- a/Makefile.build +++ b/Makefile.build @@ -570,7 +570,7 @@ test-suite: world $(ALLSTDLIB).v ################################################################## .PHONY: lib kernel byterun library proofs tactics interp parsing pretyping -.PHONY: engine highparsing stm toplevel ltac ltacprof +.PHONY: engine highparsing stm toplevel ltac lib: lib/clib.cma lib/lib.cma kernel: kernel/kernel.cma diff --git a/Makefile.common b/Makefile.common index e2f67226b..86a7ea847 100644 --- a/Makefile.common +++ b/Makefile.common @@ -62,7 +62,7 @@ CSDPCERT:=plugins/micromega/csdpcert$(EXE) CORESRCDIRS:=\ config lib kernel kernel/byterun library \ - proofs tactics pretyping interp stm ltacprof\ + proofs tactics pretyping interp stm \ toplevel parsing printing intf engine ltac PLUGINS:=\ @@ -167,8 +167,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \ CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \ engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ parsing/parsing.cma printing/printing.cma tactics/tactics.cma \ - stm/stm.cma ltacprof/ltacprof.cma toplevel/toplevel.cma \ - parsing/highparsing.cma ltac/ltac.cma + stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma ltac/ltac.cma TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma diff --git a/lib/flags.ml b/lib/flags.ml index c1ec9738c..4983e4082 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -220,6 +220,7 @@ let native_compiler = ref false let print_mod_uid = ref false let tactic_context_compat = ref false +let profile_ltac = ref false let dump_bytecode = ref false let set_dump_bytecode = (:=) dump_bytecode diff --git a/lib/flags.mli b/lib/flags.mli index 24780f0dc..e13655e4a 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -143,6 +143,8 @@ val tactic_context_compat : bool ref (** Set to [true] to trigger the compatibility bugged context matching (old context vs. appcontext) is set. *) +val profile_ltac : bool ref + (** Dump the bytecode after compilation (for debugging purposes) *) val dump_bytecode : bool ref val set_dump_bytecode : bool -> unit diff --git a/ltac/ltac.mllib b/ltac/ltac.mllib index d8854e6e7..65ed114cf 100644 --- a/ltac/ltac.mllib +++ b/ltac/ltac.mllib @@ -3,6 +3,7 @@ Tacenv Tactic_debug Tacintern Tacentries +Profile_ltac Tacinterp Evar_tactics Tactic_option diff --git a/ltacprof/profile_ltac.ml b/ltac/profile_ltac.ml index 41bde12b1..4f982f1eb 100644 --- a/ltacprof/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -5,15 +5,11 @@ open Util (** [is_profiling] and the profiling info ([stack]) should be synchronized with the document; the rest of the ref cells are either local to individual tactic invocations, or global flags, and need not be synchronized, since no document-level backtracking happens within tactics. We synchronize is_profiling via an option. *) -let is_profiling = ref false +let is_profiling = Flags.profile_ltac let set_profiling b = is_profiling := b let get_profiling () = !is_profiling -let should_display_profile_at_close = ref false -let set_display_profile_at_close b = should_display_profile_at_close := b - - let new_call = ref false let entered_call() = new_call := true let is_new_call() = let b = !new_call in new_call := false; b @@ -293,9 +289,16 @@ let reset_profile() = stack := [{entry=empty_entry(); children=Hashtbl.create 20}]; encountered_multi_success_backtracking := false -let do_print_results_at_close () = - if !should_display_profile_at_close - then print_results () - else () +let do_print_results_at_close () = if get_profiling () then print_results () let _ = Declaremods.append_end_library_hook do_print_results_at_close + +let _ = + let open Goptions in + declare_bool_option + { optsync = true; + optdepr = false; + optname = "Ltac Profiling"; + optkey = ["Ltac"; "Profiling"]; + optread = get_profiling; + optwrite = set_profiling } diff --git a/ltacprof/profile_ltac.mli b/ltac/profile_ltac.mli index 65c067e86..0029b8b55 100644 --- a/ltacprof/profile_ltac.mli +++ b/ltac/profile_ltac.mli @@ -4,8 +4,6 @@ val set_profiling : bool -> unit val get_profiling : unit -> bool -val set_display_profile_at_close : bool -> unit - val entered_call : unit -> unit val print_results : unit -> unit diff --git a/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4 index b83ab8c52..8889bd13c 100644 --- a/ltac/profile_ltac_tactics.ml4 +++ b/ltac/profile_ltac_tactics.ml4 @@ -17,15 +17,6 @@ TACTIC EXTEND stop_profiling | [ "stop" "ltac" "profiling" ] -> [ tclSET_PROFILING false ] END;; -let _ = - Goptions.declare_bool_option - { optsync = true; - optdepr = false; - optname = "Ltac Profiling"; - optkey = ["Ltac"; "Profiling"]; - optread = get_profiling; - optwrite = set_profiling } - VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF [ "Reset" "Ltac" "Profile" ] -> [ reset_profile() ] END diff --git a/ltacprof/ltacprof.mllib b/ltacprof/ltacprof.mllib deleted file mode 100644 index 383e5d285..000000000 --- a/ltacprof/ltacprof.mllib +++ /dev/null @@ -1 +0,0 @@ -Profile_ltac diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index de0f73ff4..aab20650a 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -549,7 +549,7 @@ let parse_args arglist = else native_compiler := true |"-notop" -> unset_toplevel_name () |"-output-context" -> output_context := true - |"-profile-ltac" -> Profile_ltac.set_profiling true; Profile_ltac.set_display_profile_at_close true + |"-profile-ltac" -> Flags.profile_ltac := true |"-q" -> no_load_rc () |"-quiet"|"-silent" -> Flags.make_silent true; Flags.make_warn false |"-quick" -> Flags.compilation_mode := BuildVio |