diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/acyclicGraph.ml | 5 | ||||
| -rw-r--r-- | lib/control.ml | 18 | ||||
| -rw-r--r-- | lib/control.mli | 11 | ||||
| -rw-r--r-- | lib/envars.ml | 1 | ||||
| -rw-r--r-- | lib/flags.ml | 6 | ||||
| -rw-r--r-- | lib/flags.mli | 2 | ||||
| -rw-r--r-- | lib/rtree.ml | 5 | ||||
| -rw-r--r-- | lib/rtree.mli | 6 | ||||
| -rw-r--r-- | lib/util.ml | 6 | ||||
| -rw-r--r-- | lib/util.mli | 4 |
10 files changed, 36 insertions, 28 deletions
diff --git a/lib/acyclicGraph.ml b/lib/acyclicGraph.ml index 7d04c8f5a1..e1dcfcc6ce 100644 --- a/lib/acyclicGraph.ml +++ b/lib/acyclicGraph.ml @@ -721,7 +721,10 @@ module Make (Point:Point) = struct let rmap, csts = PSet.fold (fun u (rmap,csts) -> let arcu = repr g u in if PSet.mem arcu.canon kept then - PMap.add arcu.canon arcu.canon rmap, Constraint.add (u,Eq,arcu.canon) csts + let csts = if Point.equal u arcu.canon then csts + else Constraint.add (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 diff --git a/lib/control.ml b/lib/control.ml index ffb3584f1e..9054507e46 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -89,3 +89,21 @@ let timeout_fun_ref = ref timeout_fun let set_timeout f = timeout_fun_ref := f let timeout n f e = !timeout_fun_ref.timeout n f e + +let protect_sigalrm f x = + let timed_out = ref false in + let timeout_handler _ = timed_out := true in + try + let old_handler = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in + try + let res = f x in + Sys.set_signal Sys.sigalrm old_handler; + match !timed_out, old_handler with + | true, Sys.Signal_handle f -> f Sys.sigalrm; res + | _, _ -> res + with e -> + let e = Backtrace.add_backtrace e in + Sys.set_signal Sys.sigalrm old_handler; + Exninfo.iraise e + with Invalid_argument _ -> (* This happens on Windows, as handling SIGALRM does not seem supported *) + f x diff --git a/lib/control.mli b/lib/control.mli index 59e2a15158..640d41a4f7 100644 --- a/lib/control.mli +++ b/lib/control.mli @@ -29,3 +29,14 @@ val timeout : int -> ('a -> 'b) -> 'a -> exn -> 'b API and it is scheduled to go away. *) type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> exn -> 'b } val set_timeout : timeout -> unit + +(** [protect_sigalrm f x] computes [f x], but if SIGALRM is received during that + computation, the signal handler is executed only once the computation is + terminated. Otherwise said, it makes the execution of [f] atomic w.r.t. + handling of SIGALRM. + + This is useful for example to prevent the implementation of `Timeout` to + interrupt I/O routines, generating ill-formed output. + +*) +val protect_sigalrm : ('a -> 'b) -> 'a -> 'b diff --git a/lib/envars.ml b/lib/envars.ml index 0f4670688b..af8e45b137 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -178,6 +178,7 @@ let print_config ?(prefix_var_name="") f coq_src_subdirs = 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; + fprintf f "%sWARN=%s\n" prefix_var_name "-warn-error +a-3"; fprintf f "%sHASNATDYNLINK=%s\n" prefix_var_name (if Coq_config.has_natdynlink then "true" else "false"); fprintf f "%sCOQ_SRC_SUBDIRS=%s\n" prefix_var_name (String.concat " " coq_src_subdirs) diff --git a/lib/flags.ml b/lib/flags.ml index 6718e7a954..452433d271 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -62,14 +62,11 @@ let we_are_parsing = ref false (* Current means no particular compatibility consideration. For correct comparisons, this constructor should remain the last one. *) -type compat_version = V8_7 | V8_8 | V8_9 | Current +type compat_version = V8_8 | V8_9 | Current let compat_version = ref Current let version_compare v1 v2 = match v1, v2 with - | V8_7, V8_7 -> 0 - | V8_7, _ -> -1 - | _, V8_7 -> 1 | V8_8, V8_8 -> 0 | V8_8, _ -> -1 | _, V8_8 -> 1 @@ -82,7 +79,6 @@ 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 - | V8_7 -> "8.7" | V8_8 -> "8.8" | V8_9 -> "8.9" | Current -> "current" diff --git a/lib/flags.mli b/lib/flags.mli index bf8846417b..a70a23b902 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -52,7 +52,7 @@ val we_are_parsing : bool ref (* Set Printing All flag. For some reason it is a global flag *) val raw_print : bool ref -type compat_version = V8_7 | V8_8 | V8_9 | Current +type compat_version = V8_8 | V8_9 | Current val compat_version : compat_version ref val version_compare : compat_version -> compat_version -> int val version_strictly_greater : compat_version -> bool diff --git a/lib/rtree.ml b/lib/rtree.ml index e1c6a4c4d6..66d9eba3f7 100644 --- a/lib/rtree.ml +++ b/lib/rtree.ml @@ -115,8 +115,6 @@ struct end -let smartmap = Smart.map - (** Structural equality test, parametrized by an equality on elements *) let rec raw_eq cmp t t' = match t, t' with @@ -149,9 +147,6 @@ let equiv cmp cmp' = let equal cmp t t' = t == t' || raw_eq cmp t t' || equiv cmp cmp t t' -(** Deprecated alias *) -let eq_rtree = equal - (** Intersection of rtrees of same arity *) let rec inter cmp interlbl def n histo t t' = try diff --git a/lib/rtree.mli b/lib/rtree.mli index 5ab14f6039..67519aa387 100644 --- a/lib/rtree.mli +++ b/lib/rtree.mli @@ -77,15 +77,9 @@ val incl : ('a -> 'a -> bool) -> ('a -> 'a -> 'a option) -> 'a -> 'a t -> 'a t - (** See also [Smart.map] *) val map : ('a -> 'b) -> 'a t -> 'b t -val smartmap : ('a -> 'a) -> 'a t -> 'a t -(** @deprecated Same as [Smart.map] *) - (** A rather simple minded pretty-printer *) val pp_tree : ('a -> Pp.t) -> 'a t -> Pp.t -val eq_rtree : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool -(** @deprecated Same as [Rtree.equal] *) - module Smart : sig diff --git a/lib/util.ml b/lib/util.ml index 0389336258..38d73d3453 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -20,12 +20,6 @@ let on_pi1 f (a,b,c) = (f a,b,c) let on_pi2 f (a,b,c) = (a,f b,c) let on_pi3 f (a,b,c) = (a,b,f c) -(* Comparing pairs *) - -let pair_compare cmpx cmpy (x1,y1 as p1) (x2,y2 as p2) = - if p1 == p2 then 0 else - let c = cmpx x1 x2 in if c == 0 then cmpy y1 y2 else c - (* Projections from triplets *) let pi1 (a,_,_) = a diff --git a/lib/util.mli b/lib/util.mli index fa3b622621..1eb60f509a 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -17,10 +17,6 @@ val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c val on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b val map_pair : ('a -> 'b) -> 'a * 'a -> 'b * 'b -(** Comparing pairs *) - -val pair_compare : ('a -> 'a -> int) -> ('b -> 'b -> int) -> ('a * 'b -> 'a * 'b -> int) - (** Mapping under triple *) val on_pi1 : ('a -> 'b) -> 'a * 'c * 'd -> 'b * 'c * 'd |