From e8b9ee76af721c32b2d5cfcdae4ecbf47b341545 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 27 Sep 2016 17:16:39 +0200 Subject: Fix #5061: Warnings flag has no discernible value The default value of the warnings flag was printed as an empty string, now replaced by "default". --- lib/cWarnings.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib') diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml index 78fa84f333..720f54606c 100644 --- a/lib/cWarnings.ml +++ b/lib/cWarnings.ml @@ -21,7 +21,7 @@ let warnings : (string, t) Hashtbl.t = Hashtbl.create 97 let categories : (string, string list) Hashtbl.t = Hashtbl.create 97 let current_loc = ref Loc.ghost -let flags = ref "" +let flags = ref "default" let set_current_loc = (:=) current_loc -- cgit v1.2.3 From e1df1b77f8c72636b6e347f41f6f38976c86e909 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 28 Sep 2016 16:32:42 +0200 Subject: -profile-ltac-cutoff alike Show Ltac Profile Cutoff (#5100) With this command line flag one can profile ltac in files /and/ trim the results without actually touching the files. --- lib/flags.ml | 1 + lib/flags.mli | 1 + 2 files changed, 2 insertions(+) (limited to 'lib') diff --git a/lib/flags.ml b/lib/flags.ml index 13525165ab..d29064c97f 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -226,6 +226,7 @@ let print_mod_uid = ref false let tactic_context_compat = ref false let profile_ltac = ref false +let profile_ltac_cutoff = ref 0.0 let dump_bytecode = ref false let set_dump_bytecode = (:=) dump_bytecode diff --git a/lib/flags.mli b/lib/flags.mli index 8fe64d24fa..839c252cbb 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -149,6 +149,7 @@ val tactic_context_compat : bool ref context vs. appcontext) is set. *) val profile_ltac : bool ref +val profile_ltac_cutoff : float ref (** Dump the bytecode after compilation (for debugging purposes) *) val dump_bytecode : bool ref -- cgit v1.2.3 From 6d20e4c136fb2726ec8577bdfee051ecacdf8261 Mon Sep 17 00:00:00 2001 From: Yves Bertot Date: Wed, 28 Sep 2016 16:24:51 +0200 Subject: fix bug 3683 : adds references to the web site for the bug tracker in error messages --- lib/cErrors.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'lib') diff --git a/lib/cErrors.ml b/lib/cErrors.ml index 1459141d1e..c69c7e4001 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -93,7 +93,9 @@ let print_backtrace e = match Backtrace.get_backtrace e with let print_anomaly askreport e = if askreport then - hov 0 (str "Anomaly: " ++ raw_anomaly e ++ spc () ++ str "Please report.") + hov 0 (str "Anomaly: " ++ raw_anomaly e ++ spc () ++ + strbrk "Please report at " ++ str Coq_config.wwwbugtracker ++ + str ".") else hov 0 (raw_anomaly e) -- cgit v1.2.3 From edb55a94fc5c0473e57f5a61c0c723194c2ff414 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 27 Sep 2016 17:15:10 +0200 Subject: Fix bug #4798: compat notations should not modify the parser. This is a quick fix. The Metasyntax module should be thoroughly revised in trunk, because it starts featuring a lot of spaghetti code and redundant data. --- lib/flags.ml | 27 ++++++++++++++++----------- lib/flags.mli | 1 + 2 files changed, 17 insertions(+), 11 deletions(-) (limited to 'lib') diff --git a/lib/flags.ml b/lib/flags.ml index d29064c97f..af55e9e2bb 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -112,17 +112,22 @@ type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | Current let compat_version = ref Current -let version_strictly_greater v = match !compat_version, v with -| V8_2, (V8_2 | V8_3 | V8_4 | V8_5 | Current) -> false -| V8_3, (V8_3 | V8_4 | V8_5 | Current) -> false -| V8_4, (V8_4 | V8_5 | Current) -> false -| V8_5, (V8_5 | Current) -> false -| Current, Current -> false -| V8_3, V8_2 -> true -| V8_4, (V8_2 | V8_3) -> true -| V8_5, (V8_2 | V8_3 | V8_4) -> true -| Current, (V8_2 | V8_3 | V8_4 | V8_5) -> true - +let version_compare v1 v2 = match v1, v2 with +| V8_2, V8_2 -> 0 +| V8_2, (V8_3 | V8_4 | V8_5 | Current) -> -1 +| V8_3, V8_2 -> 1 +| V8_3, V8_3 -> 0 +| V8_3, (V8_4 | V8_5 | Current) -> -1 +| V8_4, (V8_2 | V8_3) -> 1 +| V8_4, V8_4 -> 0 +| V8_4, (V8_5 | Current) -> -1 +| V8_5, (V8_2 | V8_3 | V8_4) -> 1 +| V8_5, V8_5 -> 0 +| V8_5, Current -> -1 +| Current, Current -> 0 +| Current, (V8_2 | V8_3 | V8_4 | V8_5) -> 1 + +let version_strictly_greater v = version_compare !compat_version v > 0 let version_less_or_equal v = not (version_strictly_greater v) let pr_version = function diff --git a/lib/flags.mli b/lib/flags.mli index 839c252cbb..9dc0c9c048 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -64,6 +64,7 @@ val univ_print : bool ref type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | Current val compat_version : compat_version ref +val version_compare : compat_version -> compat_version -> int val version_strictly_greater : compat_version -> bool val version_less_or_equal : compat_version -> bool val pr_version : compat_version -> string -- cgit v1.2.3 From 46daf37ed46397b03a30fa2d89b62ffcc2c8d166 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 29 Sep 2016 14:32:50 -0400 Subject: Set the default LtacProf cutoff to 2% This was the original value from Tobias' code. When a user passes -profile-ltac on the command line, or inserts [Show Ltac Profile] in the document, the most useful default behavior is to not overload them with useless information. When GUI clients want to display fancier profiling information, there is no cost to the user to requiring them to specify what cutoff they want. If the GUI client does not have any special LtacProf handling, the most useful presentation is again the one that cuts off the display at 2% total time. --- lib/flags.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib') diff --git a/lib/flags.ml b/lib/flags.ml index af55e9e2bb..65873e5214 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -231,7 +231,7 @@ let print_mod_uid = ref false let tactic_context_compat = ref false let profile_ltac = ref false -let profile_ltac_cutoff = ref 0.0 +let profile_ltac_cutoff = ref 2.0 let dump_bytecode = ref false let set_dump_bytecode = (:=) dump_bytecode -- cgit v1.2.3