diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/cAst.ml | 2 | ||||
| -rw-r--r-- | lib/cAst.mli | 2 | ||||
| -rw-r--r-- | lib/cErrors.ml | 6 | ||||
| -rw-r--r-- | lib/control.ml | 24 | ||||
| -rw-r--r-- | lib/control.mli | 11 | ||||
| -rw-r--r-- | lib/envars.ml | 34 |
6 files changed, 59 insertions, 20 deletions
diff --git a/lib/cAst.ml b/lib/cAst.ml index 18fa1c9b0d..30b7fca587 100644 --- a/lib/cAst.ml +++ b/lib/cAst.ml @@ -24,3 +24,5 @@ let map_from_loc f l = let with_val f n = f n.v let with_loc_val f n = f ?loc:n.loc n.v + +let eq f x y = f x.v y.v diff --git a/lib/cAst.mli b/lib/cAst.mli index 2e07d1cd78..025bdf25ab 100644 --- a/lib/cAst.mli +++ b/lib/cAst.mli @@ -22,3 +22,5 @@ val map_from_loc : (?loc:Loc.t -> 'a -> 'b) -> 'a Loc.located -> 'b t val with_val : ('a -> 'b) -> 'a t -> 'b val with_loc_val : (?loc:Loc.t -> 'a -> 'b) -> 'a t -> 'b + +val eq : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool diff --git a/lib/cErrors.ml b/lib/cErrors.ml index cb64e36755..760c07783b 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -37,7 +37,7 @@ let user_err ?loc ?info ?hdr strm = let info = Option.cata (Loc.add_loc info) info loc in Exninfo.iraise (UserError (hdr, strm), info) -exception Timeout +exception Timeout = Control.Timeout (** Only anomalies should reach the bottom of the handler stack. In usual situation, the [handle_stack] is treated as it if was always @@ -135,7 +135,7 @@ let _ = register_handler begin function | UserError(s, pps) -> Some (where s ++ pps) | _ -> None -end + end (** Critical exceptions should not be caught and ignored by mistake by inner functions during a [vernacinterp]. They should be handled @@ -145,7 +145,7 @@ end let noncritical = function | Sys.Break | Out_of_memory | Stack_overflow | Assert_failure _ | Match_failure _ | Anomaly _ - | Timeout -> false + | Control.Timeout -> false | Invalid_argument "equal: functional value" -> false | _ -> true [@@@ocaml.warning "+52"] diff --git a/lib/control.ml b/lib/control.ml index 95ea3935a7..7da95ff3dd 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -16,6 +16,8 @@ let steps = ref 0 let enable_thread_delay = ref false +exception Timeout + let check_for_interrupt () = if !interrupt then begin interrupt := false; raise Sys.Break end; if !enable_thread_delay then begin @@ -27,8 +29,8 @@ let check_for_interrupt () = end (** This function does not work on windows, sigh... *) -let unix_timeout n f x e = - let timeout_handler _ = raise e in +let unix_timeout n f x = + 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 () = @@ -38,13 +40,13 @@ let unix_timeout n f x e = try let res = f x in restore_timeout (); - res - with e -> - let e = Exninfo.capture e in + Some res + with Timeout -> restore_timeout (); - Exninfo.iraise e + None + -let windows_timeout n f x e = +let windows_timeout n f x = let killed = ref false in let exited = ref false in let thread init = @@ -70,18 +72,18 @@ let windows_timeout n f x e = exited := true; raise Sys.Break end in - res + Some res with | Sys.Break -> (* Just in case, it could be a regular Ctrl+C *) if not !exited then begin killed := true; raise Sys.Break end - else raise e + else None | e -> let e = Exninfo.capture e in let () = killed := true in Exninfo.iraise e -type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> exn -> 'b } +type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> 'b option } let timeout_fun = match Sys.os_type with | "Unix" | "Cygwin" -> { timeout = unix_timeout } @@ -90,7 +92,7 @@ let timeout_fun = match Sys.os_type with 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 timeout n f = !timeout_fun_ref.timeout n f let protect_sigalrm f x = let timed_out = ref false in diff --git a/lib/control.mli b/lib/control.mli index 25135934bc..9465d8f0d5 100644 --- a/lib/control.mli +++ b/lib/control.mli @@ -10,6 +10,9 @@ (** Global control of Coq. *) +(** Used to convert signals to exceptions *) +exception Timeout + (** Will periodically call [Thread.delay] if set to true *) val enable_thread_delay : bool ref @@ -21,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 -> exn -> 'b -(** [timeout n f x e] tries to compute [f x], and if it fails to do so - before [n] seconds, it raises [e] instead. *) +val timeout : int -> ('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 -> exn -> 'b } +type timeout = { timeout : 'a 'b. int -> ('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/envars.ml b/lib/envars.ml index 585d5185b4..1702b5d7a2 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -12,7 +12,37 @@ open Util (** {1 Helper functions} *) -let getenv_else s dft = try Sys.getenv s with Not_found -> dft () +let parse_env_line l = + try Scanf.sscanf l "%[^=]=%S" (fun name value -> Some(name,value)) + with _ -> None + +let with_ic file f = + let ic = open_in file in + try + let rc = f ic in + close_in ic; + rc + with e -> close_in ic; raise e + +let getenv_from_file name = + let base = Filename.dirname Sys.executable_name in + try + with_ic (base ^ "/coq_environment.txt") (fun ic -> + let rec find () = + let l = input_line ic in + match parse_env_line l with + | Some(n,v) when n = name -> v + | _ -> find () + in + find ()) + with + | Sys_error s -> raise Not_found + | End_of_file -> raise Not_found + +let system_getenv name = + try Sys.getenv name with Not_found -> getenv_from_file name + +let getenv_else s dft = try system_getenv s with Not_found -> dft () let safe_getenv warning n = getenv_else n (fun () -> @@ -145,7 +175,7 @@ let coqpath = (** {2 Caml paths} *) -let ocamlfind () = Coq_config.ocamlfind +let ocamlfind () = getenv_else "OCAMLFIND" (fun () -> Coq_config.ocamlfind) (** {1 XDG utilities} *) |