diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/cDebug.ml | 92 | ||||
| -rw-r--r-- | lib/cDebug.mli | 50 | ||||
| -rw-r--r-- | lib/cErrors.ml | 5 | ||||
| -rw-r--r-- | lib/cWarnings.ml | 6 | ||||
| -rw-r--r-- | lib/cWarnings.mli | 7 | ||||
| -rw-r--r-- | lib/control.ml | 36 | ||||
| -rw-r--r-- | lib/dune | 4 | ||||
| -rw-r--r-- | lib/envars.ml | 5 | ||||
| -rw-r--r-- | lib/flags.ml | 1 | ||||
| -rw-r--r-- | lib/flags.mli | 1 | ||||
| -rw-r--r-- | lib/lib.mllib | 1 | ||||
| -rw-r--r-- | lib/pp.mli | 49 | ||||
| -rw-r--r-- | lib/spawn.ml | 2 | ||||
| -rw-r--r-- | lib/util.ml | 7 | ||||
| -rw-r--r-- | lib/util.mli | 9 |
15 files changed, 230 insertions, 45 deletions
diff --git a/lib/cDebug.ml b/lib/cDebug.ml new file mode 100644 index 0000000000..efa7365b91 --- /dev/null +++ b/lib/cDebug.ml @@ -0,0 +1,92 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +type flag = bool ref + +type t = (unit -> Pp.t) -> unit + +let debug = ref CString.Map.empty + +(* Used to remember level of Set Debug "all" for debugs created by + plugins dynlinked after the Set *) +let all_flag = ref false + +let set_debug_backtrace b = + Exninfo.record_backtrace b + +let set_debug_all b = + set_debug_backtrace b; + CString.Map.iter (fun _ flag -> flag := b) !debug; + all_flag := b + +let create_full ~name () = + let anomaly pp = CErrors.anomaly ~label:"CDebug.create" pp in + let () = match name with + | "all"|"backtrace" -> anomaly Pp.(str"The debug name \""++str name++str"\" is reserved.") + | _ -> + if CString.Map.mem name !debug then + anomaly Pp.(str "The debug name \"" ++ str name ++ str "\" is already used.") + in + let pp x = + Feedback.msg_debug Pp.(str "[" ++ str name ++ str "] " ++ x) + in + let flag = ref !all_flag in + debug := CString.Map.add name flag !debug; + let pp x = + if !flag + then pp (x ()) + in + flag, pp + +let create ~name () = + snd (create_full ~name ()) + +let get_flag flag = !flag + +let warn_unknown_debug = CWarnings.create ~name:"unknown-debug-flag" ~category:"option" + Pp.(fun name -> str "There is no debug flag \"" ++ str name ++ str "\".") + +let get_flags () = + let pp_flag name flag = if flag then name else "-"^name in + let flags = + CString.Map.fold + (fun name v acc -> pp_flag name !v :: acc) + !debug [] + in + let all = pp_flag "all" !all_flag in + let bt = pp_flag "backtrace" (Printexc.backtrace_status()) in + String.concat "," (all::bt::flags) + +exception Error + +let parse_flags s = + let parse_flag s = + if CString.is_empty s then raise Error + else if s.[0] = '-' + then String.sub s 1 (String.length s - 1), false + else s, true + in + try + Some (CList.map parse_flag @@ String.split_on_char ',' s) + with Error -> None + +let set_flags s = match parse_flags s with + | None -> CErrors.user_err Pp.(str "Syntax error in debug flags.") + | Some flags -> + let set_one_flag (name,b) = match name with + | "all" -> set_debug_all b + | "backtrace" -> set_debug_backtrace b + | _ -> match CString.Map.find_opt name !debug with + | None -> warn_unknown_debug name + | Some flag -> flag := b + in + List.iter set_one_flag flags + +let misc, pp_misc = create_full ~name:"misc" () diff --git a/lib/cDebug.mli b/lib/cDebug.mli new file mode 100644 index 0000000000..846c4b493b --- /dev/null +++ b/lib/cDebug.mli @@ -0,0 +1,50 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +type flag + +type t = (unit -> Pp.t) -> unit + +(** Creates a debug component, which may be used to print debug + messages. + + A debug component is named by the string [name]. It is either + active or inactive. + + The special component ["all"] may be used to control all components. + + There is also a special component ["backtrace"] to control + backtrace recording. +*) +val create : name:string -> unit -> t + +(** Useful when interacting with a component from code, typically when + doing something more complicated than printing. + + Note that the printer function prints some metadata compared to + [ fun pp -> if get_flag flag then Feedback.msg_debug (pp ()) ] + *) +val create_full : name:string -> unit -> flag * t + +val get_flag : flag -> bool + +(** [get_flags] and [set_flags] use the user syntax: a comma separated + list of activated "component" and "-component"s. [get_flags] starts + with "all" or "-all" and lists all components after it (even if redundant). *) +val get_flags : unit -> string + +(** Components not mentioned are not affected (use the "all" component + at the start if you want to reset everything). *) +val set_flags : string -> unit + +val set_debug_all : bool -> unit + +val misc : flag +val pp_misc : t diff --git a/lib/cErrors.ml b/lib/cErrors.ml index 760c07783b..1baedb64c9 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -30,6 +30,7 @@ let anomaly ?loc ?info ?label pp = let info = Option.cata (Loc.add_loc info) info loc in Exninfo.iraise (Anomaly (label, pp), info) +(* TODO remove the option *) exception UserError of string option * Pp.t (* User errors *) let user_err ?loc ?info ?hdr strm = @@ -46,7 +47,7 @@ exception Timeout = Control.Timeout let where = function | None -> mt () | Some s -> - if !Flags.debug then str "in " ++ str s ++ str ":" ++ spc () else mt () + str "in " ++ str s ++ str ":" ++ spc () let raw_anomaly e = match e with | Anomaly (s, pps) -> @@ -133,7 +134,7 @@ let print_no_report e = iprint_no_report (e, Exninfo.info e) let _ = register_handler begin function | UserError(s, pps) -> - Some (where s ++ pps) + Some pps | _ -> None end diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml index cc1fa647f9..ee7dab92bc 100644 --- a/lib/cWarnings.ml +++ b/lib/cWarnings.ml @@ -173,3 +173,9 @@ let create ~name ~category ?(default=Enabled) pp = | Disabled -> () | AsError -> CErrors.user_err ?loc (pp x) | Enabled -> Feedback.msg_warning ?loc (pp x) + +(* Remark: [warn] does not need to start with a comma, but if present + it won't hurt (",," is normalized into ","). *) +let with_warn warn (f:'b -> 'a) x = + let s = get_flags () in + Util.try_finally (fun x -> set_flags (s^","^warn);f x) x set_flags s diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli index ded1f9be3b..b63eed09d0 100644 --- a/lib/cWarnings.mli +++ b/lib/cWarnings.mli @@ -19,3 +19,10 @@ val set_flags : string -> unit (** Cleans up a user provided warnings status string, e.g. removing unknown warnings (in which case a warning is emitted) or subsumed warnings . *) val normalize_flags_string : string -> string + +(** [with_warn "-xxx,+yyy..." f x] calls [f x] after setting the + warnings as specified in the string (keeping other previously set + warnings), and restores current warnings after [f()] returns or + raises an exception. If both f and restoring the warnings raise + exceptions, the latter is raised. *) +val with_warn: string -> ('b -> 'a) -> 'b -> 'a diff --git a/lib/control.ml b/lib/control.ml index ea94bda064..5a38022291 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -29,22 +29,32 @@ let check_for_interrupt () = end (** This function does not work on windows, sigh... *) +(* This function assumes it is the only function calling [setitimer] *) let unix_timeout n f x = let open Unix in let timeout_handler _ = raise Timeout in - let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in - let _ = setitimer ITIMER_REAL {it_interval = 0.; it_value = n} in - let restore_timeout () = - let _ = setitimer ITIMER_REAL { it_interval = 0.; it_value = 0. } in - Sys.set_signal Sys.sigalrm psh - in - try - let res = f x in - restore_timeout (); - Some res - with Timeout -> - restore_timeout (); - None + let old_timer = getitimer ITIMER_REAL in + (* Here we assume that the existing timer will also interrupt us. *) + if old_timer.it_value > 0. && old_timer.it_value <= n then Some (f x) else + let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in + let old_timer = setitimer ITIMER_REAL {it_interval = 0.; it_value = n} in + let restore_timeout () = + let timer_status = getitimer ITIMER_REAL in + let old_timer_value = old_timer.it_value -. n +. timer_status.it_value in + (* We want to make sure that the parent timer triggers, even if somehow the parent timeout + has already passed. This should not happen, but due to timer imprecision it can happen in practice *) + let old_timer_value = if old_timer.it_value <= 0. then 0. else + (if old_timer_value <= 0. then epsilon_float else old_timer_value) in + let _ = setitimer ITIMER_REAL { old_timer with it_value = old_timer_value } in + Sys.set_signal Sys.sigalrm psh + in + try + let res = f x in + restore_timeout (); + Some res + with Timeout -> + restore_timeout (); + None let windows_timeout n f x = @@ -1,7 +1,7 @@ (library (name lib) (synopsis "Coq's Utility Library [coq-specific]") - (public_name coq.lib) + (public_name coq-core.lib) (wrapped false) (modules_without_implementation xml_datatype) - (libraries coq.clib coq.config)) + (libraries coq-core.clib coq-core.config)) diff --git a/lib/envars.ml b/lib/envars.ml index 1702b5d7a2..823d255f58 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -132,7 +132,9 @@ let guess_coqlib fail = if not Coq_config.local && Sys.file_exists (Coq_config.coqlib / prelude) then Coq_config.coqlib else - fail "cannot guess a path for Coq libraries; please use -coqlib option") + fail "cannot guess a path for Coq libraries; please use -coqlib option \ + or ensure you have installed the package contaning Coq's stdlib (coq-stdlib in OPAM) \ + If you intend to use Coq without a standard library, the -boot -noinit options must be used.") ) let coqlib : string option ref = ref None @@ -205,6 +207,7 @@ let print_config ?(prefix_var_name="") f coq_src_subdirs = let open Printf in fprintf f "%sLOCAL=%s\n" prefix_var_name (if Coq_config.local then "1" else "0"); fprintf f "%sCOQLIB=%s/\n" prefix_var_name (coqlib ()); + fprintf f "%sCOQCORELIB=%s/\n" prefix_var_name (if Coq_config.local then coqlib () else coqlib () / "../coq-core/"); fprintf f "%sDOCDIR=%s/\n" prefix_var_name (docdir ()); fprintf f "%sOCAMLFIND=%s\n" prefix_var_name (ocamlfind ()); fprintf f "%sCAMLFLAGS=%s\n" prefix_var_name Coq_config.caml_flags; diff --git a/lib/flags.ml b/lib/flags.ml index 83733cf00d..57e879add7 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -46,7 +46,6 @@ let async_proofs_is_worker () = !async_proofs_worker_id <> "master" let load_vos_libraries = ref false -let debug = ref false let xml_debug = ref false let in_debugger = ref false diff --git a/lib/flags.mli b/lib/flags.mli index ebd23a4d20..e10e2c8cb8 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -40,7 +40,6 @@ val async_proofs_is_worker : unit -> bool val load_vos_libraries : bool ref (** Debug flags *) -val debug : bool ref val xml_debug : bool ref val in_debugger : bool ref val in_toplevel : bool ref diff --git a/lib/lib.mllib b/lib/lib.mllib index 4e08e87084..bbc9966498 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -10,6 +10,7 @@ Loc Feedback CErrors CWarnings +CDebug AcyclicGraph Rtree diff --git a/lib/pp.mli b/lib/pp.mli index 12f1ba9bb2..b3c2301d34 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -10,30 +10,31 @@ (** Coq document type. *) -(** Pretty printing guidelines ******************************************) -(* *) -(* `Pp.t` is the main pretty printing document type *) -(* in the Coq system. Documents are composed laying out boxes, and *) -(* users can add arbitrary tag metadata that backends are free *) -(* to interpret. *) -(* *) -(* The datatype has a public view to allow serialization or advanced *) -(* uses, however regular users are _strongly_ warned against its use, *) -(* they should instead rely on the available functions below. *) -(* *) -(* Box order and number is indeed an important factor. Try to create *) -(* a proper amount of boxes. The `++` operator provides "efficient" *) -(* concatenation, but using the list constructors is usually preferred. *) -(* *) -(* That is to say, this: *) -(* *) -(* `hov [str "Term"; hov (pr_term t); str "is defined"]` *) -(* *) -(* is preferred to: *) -(* *) -(* `hov (str "Term" ++ hov (pr_term t) ++ str "is defined")` *) -(* *) -(************************************************************************) +(** +{4 Pretty printing guidelines} + +[Pp.t] is the main pretty printing document type +in the Coq system. Documents are composed laying out boxes, and +users can add arbitrary tag metadata that backends are free +to interpret. + +The datatype has a public view to allow serialization or advanced +uses, however regular users are _strongly_ warned against its use, +they should instead rely on the available functions below. + +Box order and number is indeed an important factor. Try to create +a proper amount of boxes. The [++] operator provides "efficient" +concatenation, but using the list constructors is usually preferred. + +That is to say, this: + +[hov [str "Term"; hov (pr_term t); str "is defined"]] + +is preferred to: + +[hov (str "Term" ++ hov (pr_term t) ++ str "is defined")] +*) + (* XXX: Improve and add attributes *) type pp_tag = string diff --git a/lib/spawn.ml b/lib/spawn.ml index 2fe7b31d04..27b4387b61 100644 --- a/lib/spawn.ml +++ b/lib/spawn.ml @@ -13,7 +13,7 @@ let prefer_sock = Sys.os_type = "Win32" let accept_timeout = 10.0 let pr_err s = Printf.eprintf "(Spawn ,%d) %s\n%!" (Unix.getpid ()) s -let prerr_endline s = if !Flags.debug then begin pr_err s end else () +let prerr_endline s = if CDebug.(get_flag misc) then begin pr_err s end else () type req = ReqDie | Hello of int * int diff --git a/lib/util.ml b/lib/util.ml index 87cc30e557..e8aa0f3e48 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -135,6 +135,13 @@ type 'a delayed = unit -> 'a let delayed_force f = f () +(* finalize - Credit X.Leroy, D.Remy. *) +let try_finally f x finally y = + let res = try f x with exn -> finally y; raise exn in + finally y; + res + + (* Misc *) type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b diff --git a/lib/util.mli b/lib/util.mli index fe34525671..aefb015c38 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -112,6 +112,15 @@ type 'a delayed = unit -> 'a val delayed_force : 'a delayed -> 'a +(** [try_finally f x g y] applies the main code [f] to [x] and + returns the result after having applied the finalization + code [g] to [y]. If the main code raises the exception + [exn], the finalization code is executed and [exn] is raised. + If the finalization code itself fails, the exception + returned is always the one from the finalization code. + Credit X.Leroy, D.Remy. *) +val try_finally: ('a -> 'b) -> 'a -> ('c -> unit) -> 'c -> 'b + (** {6 Enriched exceptions} *) type iexn = Exninfo.iexn |