aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/acyclicGraph.ml171
-rw-r--r--lib/cDebug.ml92
-rw-r--r--lib/cDebug.mli50
-rw-r--r--lib/cErrors.ml5
-rw-r--r--lib/cWarnings.ml6
-rw-r--r--lib/cWarnings.mli7
-rw-r--r--lib/control.ml43
-rw-r--r--lib/control.mli4
-rw-r--r--lib/dune4
-rw-r--r--lib/envars.ml5
-rw-r--r--lib/flags.ml1
-rw-r--r--lib/flags.mli1
-rw-r--r--lib/lib.mllib1
-rw-r--r--lib/pp.mli49
-rw-r--r--lib/spawn.ml2
-rw-r--r--lib/stateid.ml3
-rw-r--r--lib/stateid.mli7
-rw-r--r--lib/util.ml7
-rw-r--r--lib/util.mli9
19 files changed, 370 insertions, 97 deletions
diff --git a/lib/acyclicGraph.ml b/lib/acyclicGraph.ml
index 14c08da35d..17299c72eb 100644
--- a/lib/acyclicGraph.ml
+++ b/lib/acyclicGraph.ml
@@ -58,15 +58,59 @@ module Make (Point:Point) = struct
*)
- module PMap = Point.Map
- module PSet = Point.Set
+ module Index :
+ sig
+ type t
+ val equal : t -> t -> bool
+ module Set : CSig.SetS with type elt = t
+ module Map : CMap.ExtS with type key = t and module Set := Set
+ type table
+ val empty : table
+ val fresh : Point.t -> table -> t * table
+ val mem : Point.t -> table -> bool
+ val find : Point.t -> table -> t
+ val repr : t -> table -> Point.t
+ end =
+ struct
+ type t = int
+ let equal = Int.equal
+ module Set = Int.Set
+ module Map = Int.Map
+
+ type table = {
+ tab_len : int;
+ tab_fwd : Point.t Int.Map.t;
+ tab_bwd : int Point.Map.t
+ }
+
+ let empty = {
+ tab_len = 0;
+ tab_fwd = Int.Map.empty;
+ tab_bwd = Point.Map.empty;
+ }
+ let mem x t = Point.Map.mem x t.tab_bwd
+ let find x t = Point.Map.find x t.tab_bwd
+ let repr n t = Int.Map.find n t.tab_fwd
+
+ let fresh x t =
+ let () = assert (not @@ mem x t) in
+ let n = t.tab_len in
+ n, {
+ tab_len = n + 1;
+ tab_fwd = Int.Map.add n x t.tab_fwd;
+ tab_bwd = Point.Map.add x n t.tab_bwd;
+ }
+ end
+
+ module PMap = Index.Map
+ module PSet = Index.Set
module Constraint = Point.Constraint
type status = NoMark | Visited | WeakVisited | ToMerge
(* Comparison on this type is pointer equality *)
type canonical_node =
- { canon: Point.t;
+ { canon: Index.t;
ltle: bool PMap.t; (* true: strict (lt) constraint.
false: weak (le) constraint. *)
gtge: PSet.t;
@@ -81,12 +125,13 @@ module Make (Point:Point) = struct
type entry =
| Canonical of canonical_node
- | Equiv of Point.t
+ | Equiv of Index.t
type t =
{ entries : entry PMap.t;
index : int;
- n_nodes : int; n_edges : int }
+ n_nodes : int; n_edges : int;
+ table : Index.table }
(** Used to cleanup mutable marks if a traversal function is
interrupted before it has the opportunity to do it itself. *)
@@ -121,7 +166,8 @@ module Make (Point:Point) = struct
| _ -> assert false) g.entries;
index = g.index;
n_nodes = g.n_nodes - 1;
- n_edges = g.n_edges }
+ n_edges = g.n_edges;
+ table = g.table }
(* Low-level function : changes data associated with a canonical node.
Resets the mutable fields in the old record, in order to avoid breaking
@@ -145,7 +191,10 @@ module Make (Point:Point) = struct
| Canonical arc -> arc
| exception Not_found ->
CErrors.anomaly ~label:"Univ.repr"
- Pp.(str"Universe " ++ Point.pr u ++ str" undefined.")
+ Pp.(str"Universe " ++ Point.pr (Index.repr u g.table) ++ str" undefined.")
+
+ let repr_node g u =
+ repr g (Index.find u g.table)
exception AlreadyDeclared
@@ -168,6 +217,7 @@ module Make (Point:Point) = struct
(* Checks most of the invariants of the graph. For debugging purposes. *)
let check_invariants ~required_canonical g =
+ let required_canonical u = required_canonical (Index.repr u g.table) in
let n_edges = ref 0 in
let n_nodes = ref 0 in
PMap.iter (fun l u ->
@@ -188,7 +238,7 @@ module Make (Point:Point) = struct
PMap.exists (fun l _ -> u == repr g l) v.ltle))
) u.gtge;
assert (u.status = NoMark);
- assert (Point.equal l u.canon);
+ assert (Index.equal l u.canon);
assert (u.ilvl > g.index);
assert (not (PMap.mem u.canon u.ltle));
incr n_nodes
@@ -200,7 +250,7 @@ module Make (Point:Point) = struct
let clean_ltle g ltle =
PMap.fold (fun u strict acc ->
let uu = (repr g u).canon in
- if Point.equal uu u then acc
+ if Index.equal uu u then acc
else (
let acc = PMap.remove u (fst acc) in
if not strict && PMap.mem uu acc then (acc, true)
@@ -210,7 +260,7 @@ module Make (Point:Point) = struct
let clean_gtge g gtge =
PSet.fold (fun u acc ->
let uu = (repr g u).canon in
- if Point.equal uu u then acc
+ if Index.equal uu u then acc
else PSet.add uu (PSet.remove u (fst acc)), true)
gtge (gtge, false)
@@ -314,7 +364,7 @@ module Make (Point:Point) = struct
| Visited -> false, to_revert | ToMerge -> true, to_revert
| NoMark ->
let to_revert = x::to_revert in
- if Point.equal x.canon v then
+ if Index.equal x.canon v then
begin x.status <- ToMerge; true, to_revert end
else
begin
@@ -425,7 +475,7 @@ module Make (Point:Point) = struct
(* Inserting shortcuts for old nodes. *)
let g = List.fold_left (fun g n ->
- if Point.equal n.canon root.canon then g else enter_equiv g n.canon root.canon)
+ if Index.equal n.canon root.canon then g else enter_equiv g n.canon root.canon)
g to_merge
in
@@ -481,11 +531,10 @@ module Make (Point:Point) = struct
raise e
let add ?(rank=0) v g =
- try
- let _arcv = PMap.find v g.entries in
- raise AlreadyDeclared
- with Not_found ->
- assert (g.index > min_int);
+ if Index.mem v g.table then raise AlreadyDeclared
+ else
+ let () = assert (g.index > min_int) in
+ let v, table = Index.fresh v g.table in
let node = {
canon = v;
ltle = PMap.empty;
@@ -497,17 +546,18 @@ module Make (Point:Point) = struct
}
in
let entries = PMap.add v (Canonical node) g.entries in
- { entries; index = g.index - 1; n_nodes = g.n_nodes + 1; n_edges = g.n_edges }
+ { entries; index = g.index - 1; n_nodes = g.n_nodes + 1; n_edges = g.n_edges; table }
exception Undeclared of Point.t
let check_declared g us =
- let check l = if not (PMap.mem l g.entries) then raise (Undeclared l) in
- PSet.iter check us
+ let check l = if not (Index.mem l g.table) then raise (Undeclared l) in
+ Point.Set.iter check us
exception Found_explanation of (constraint_type * Point.t) list
let get_explanation strict u v g =
- let v = repr g v in
+ let u = Index.find u g.table in
+ let v = repr_node g v in
let visited_strict = ref PMap.empty in
let rec traverse strict u =
if u == v then
@@ -527,6 +577,7 @@ module Make (Point:Point) = struct
| None -> ()
| Some exp ->
let typ = if strictu' then Lt else Le in
+ let u' = Index.repr u' g.table in
raise (Found_explanation ((typ, u') :: exp)))
u.ltle;
None
@@ -534,7 +585,7 @@ module Make (Point:Point) = struct
end
in
let u = repr g u in
- if u == v then [(Eq, v.canon)]
+ if u == v then [(Eq, Index.repr v.canon g.table)]
else match traverse strict u with Some exp -> exp | None -> assert false
let get_explanation strict u v g =
@@ -608,21 +659,27 @@ module Make (Point:Point) = struct
let check_eq g u v =
u == v ||
- let arcu = repr g u and arcv = repr g v in
+ let arcu = repr_node g u and arcv = repr_node g v in
arcu == arcv
let check_smaller g strict u v =
- search_path strict (repr g u) (repr g v) g
+ search_path strict (repr_node g u) (repr_node g v) g
let check_leq g u v = check_smaller g false u v
let check_lt g u v = check_smaller g true u v
(* enforce_eq g u v will force u=v if possible, will fail otherwise *)
- let rec enforce_eq u v g =
- let ucan = repr g u in
- let vcan = repr g v in
- if topo_compare ucan vcan = 1 then enforce_eq v u g
+ let enforce_eq u v g =
+ let ucan = repr_node g u in
+ let vcan = repr_node g v in
+ if ucan == vcan then g
+ else if topo_compare ucan vcan = 1 then
+ let ucan = vcan and vcan = ucan in
+ let g = insert_edge false ucan vcan g in (* Cannot fail *)
+ try insert_edge false vcan ucan g
+ with CycleDetected ->
+ Point.error_inconsistency Eq v u (get_explanation true v u g)
else
let g = insert_edge false ucan vcan g in (* Cannot fail *)
try insert_edge false vcan ucan g
@@ -631,35 +688,40 @@ module Make (Point:Point) = struct
(* enforce_leq g u v will force u<=v if possible, will fail otherwise *)
let enforce_leq u v g =
- let ucan = repr g u in
- let vcan = repr g v in
+ let ucan = repr_node g u in
+ let vcan = repr_node g v in
try insert_edge false ucan vcan g
with CycleDetected ->
Point.error_inconsistency Le u v (get_explanation true v u g)
(* enforce_lt u v will force u<v if possible, will fail otherwise *)
let enforce_lt u v g =
- let ucan = repr g u in
- let vcan = repr g v in
+ let ucan = repr_node g u in
+ let vcan = repr_node g v in
try insert_edge true ucan vcan g
with CycleDetected ->
Point.error_inconsistency Lt u v (get_explanation false v u g)
let empty =
- { entries = PMap.empty; index = 0; n_nodes = 0; n_edges = 0 }
+ { entries = PMap.empty; index = 0; n_nodes = 0; n_edges = 0; table = Index.empty }
(* Normalization *)
let constraints_of g =
- let module UF = Unionfind.Make (PSet) (PMap) in
+ let module UF = Unionfind.Make (Point.Set) (Point.Map) in
let uf = UF.create () in
let constraints_of u v acc =
match v with
| Canonical {canon=u; ltle; _} ->
PMap.fold (fun v strict acc->
let typ = if strict then Lt else Le in
+ let u = Index.repr u g.table in
+ let v = Index.repr v g.table in
Constraint.add (u,typ,v) acc) ltle acc
- | Equiv v -> UF.union u v uf; acc
+ | Equiv v ->
+ let u = Index.repr u g.table in
+ let v = Index.repr v g.table in
+ UF.union u v uf; acc
in
let csts = PMap.fold constraints_of g.entries Constraint.empty in
csts, UF.partition uf
@@ -667,16 +729,20 @@ module Make (Point:Point) = struct
(* domain g.entries = kept + removed *)
let constraints_for ~kept g =
(* rmap: partial map from canonical points to kept points *)
+ let add_cst u knd v cst =
+ Constraint.add (Index.repr u g.table, knd, Index.repr v g.table) cst
+ in
+ let kept = Point.Set.fold (fun u accu -> PSet.add (Index.find u g.table) accu) kept PSet.empty in
let rmap, csts = PSet.fold (fun u (rmap,csts) ->
let arcu = repr g u in
if PSet.mem arcu.canon kept then
- let csts = if Point.equal u arcu.canon then csts
- else Constraint.add (u,Eq,arcu.canon) csts
+ let csts = if Index.equal u arcu.canon then csts
+ else add_cst u Eq arcu.canon csts
in
PMap.add arcu.canon arcu.canon rmap, csts
else
match PMap.find arcu.canon rmap with
- | v -> rmap, Constraint.add (u,Eq,v) csts
+ | v -> rmap, add_cst u Eq v csts
| exception Not_found -> PMap.add arcu.canon u rmap, csts)
kept (PMap.empty,Constraint.empty)
in
@@ -687,7 +753,7 @@ module Make (Point:Point) = struct
(match PMap.find v.canon rmap with
| v ->
let d = if strict then Lt else Le in
- let csts = Constraint.add (u,d,v) csts in
+ let csts = add_cst u d v csts in
add_from u csts todo
| exception Not_found ->
(* v is not equal to any kept point *)
@@ -703,18 +769,23 @@ module Make (Point:Point) = struct
arc.ltle csts)
kept csts
- let domain g = PMap.domain g.entries
+ let domain g =
+ let fold u _ accu = Point.Set.add (Index.repr u g.table) accu in
+ PMap.fold fold g.entries Point.Set.empty
let choose p g u =
let exception Found of Point.t in
- let ru = (repr g u).canon in
- if p ru then Some ru
+ let ru = (repr_node g u).canon in
+ let ruv = Index.repr ru g.table in
+ if p ruv then Some ruv
else
try PMap.iter (fun v -> function
| Canonical _ -> () (* we already tried [p ru] *)
| Equiv v' ->
let rv = (repr g v').canon in
- if rv == ru && p v then raise (Found v)
+ if rv == ru then
+ let v = Index.repr v g.table in
+ if p v then raise (Found v)
(* NB: we could also try [p v'] but it will come up in the
rest of the iteration regardless. *)
) g.entries; None
@@ -724,10 +795,16 @@ module Make (Point:Point) = struct
type repr = node Point.Map.t
let repr g =
- let map n = match n with
- | Canonical n -> Node n.ltle
- | Equiv u -> Alias u
+ let fold u n accu =
+ let n = match n with
+ | Canonical n ->
+ let fold u lt accu = Point.Map.add (Index.repr u g.table) lt accu in
+ let ltle = PMap.fold fold n.ltle Point.Map.empty in
+ Node ltle
+ | Equiv u -> Alias (Index.repr u g.table)
+ in
+ Point.Map.add (Index.repr u g.table) n accu
in
- Point.Map.map map g.entries
+ PMap.fold fold g.entries Point.Map.empty
end
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 7da95ff3dd..5a38022291 100644
--- a/lib/control.ml
+++ b/lib/control.ml
@@ -29,21 +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 _ = Unix.alarm n in
- let restore_timeout () =
- let _ = Unix.alarm 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 =
@@ -52,7 +63,7 @@ let windows_timeout n f x =
let thread init =
while not !killed do
let cur = Unix.gettimeofday () in
- if float_of_int n <= cur -. init then begin
+ if n <= cur -. init then begin
interrupt := true;
exited := true;
Thread.exit ()
@@ -68,7 +79,7 @@ let windows_timeout n f x =
let cur = Unix.gettimeofday () in
(* The thread did not interrupt, but the computation took longer than
expected. *)
- let () = if float_of_int n <= cur -. init then begin
+ let () = if n <= cur -. init then begin
exited := true;
raise Sys.Break
end in
@@ -83,7 +94,7 @@ let windows_timeout n f x =
let () = killed := true in
Exninfo.iraise e
-type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> 'b option }
+type timeout = { timeout : 'a 'b. float -> ('a -> 'b) -> 'a -> 'b option }
let timeout_fun = match Sys.os_type with
| "Unix" | "Cygwin" -> { timeout = unix_timeout }
diff --git a/lib/control.mli b/lib/control.mli
index 9465d8f0d5..f992d8e8d0 100644
--- a/lib/control.mli
+++ b/lib/control.mli
@@ -24,13 +24,13 @@ val check_for_interrupt : unit -> unit
(** Use this function as a potential yield function. If {!interrupt} has been
set, il will raise [Sys.Break]. *)
-val timeout : int -> ('a -> 'b) -> 'a -> 'b option
+val timeout : float -> ('a -> 'b) -> 'a -> 'b option
(** [timeout n f x] tries to compute [Some (f x)], and if it fails to do so
before [n] seconds, returns [None] instead. *)
(** Set a particular timeout function; warning, this is an internal
API and it is scheduled to go away. *)
-type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> 'b option }
+type timeout = { timeout : 'a 'b. float -> ('a -> 'b) -> 'a -> 'b option }
val set_timeout : timeout -> unit
(** [protect_sigalrm f x] computes [f x], but if SIGALRM is received during that
diff --git a/lib/dune b/lib/dune
index 83783f9b5c..af30c9ae1f 100644
--- a/lib/dune
+++ b/lib/dune
@@ -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/stateid.ml b/lib/stateid.ml
index a1328f156c..2a41cb7866 100644
--- a/lib/stateid.ml
+++ b/lib/stateid.ml
@@ -45,3 +45,6 @@ type ('a,'b) request = {
name : string
}
+let is_valid_ref = ref (fun ~doc:_ (_ : t) -> true)
+let is_valid ~doc id = !is_valid_ref ~doc id
+let set_is_valid f = is_valid_ref := f
diff --git a/lib/stateid.mli b/lib/stateid.mli
index 9b2de9c894..00acc962a2 100644
--- a/lib/stateid.mli
+++ b/lib/stateid.mli
@@ -42,3 +42,10 @@ type ('a,'b) request = {
name : string
}
+(* Asks the document manager if the given state is valid (or belongs to an
+ old version of the document) *)
+val is_valid : doc:int -> t -> bool
+
+(* By default [is_valid] always answers true, but a document manager supporting
+ undo operations like the STM can override this. *)
+val set_is_valid : (doc:int -> t -> bool) -> unit
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 18:19:32 +0000