diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/control.ml | 5 | ||||
| -rw-r--r-- | lib/control.mli | 5 | ||||
| -rw-r--r-- | lib/coqProject_file.ml4 | 15 | ||||
| -rw-r--r-- | lib/flags.ml | 2 | ||||
| -rw-r--r-- | lib/flags.mli | 3 | ||||
| -rw-r--r-- | lib/rtree.ml | 28 | ||||
| -rw-r--r-- | lib/rtree.mli | 11 | ||||
| -rw-r--r-- | lib/spawn.ml | 2 | ||||
| -rw-r--r-- | lib/stateid.ml | 10 | ||||
| -rw-r--r-- | lib/system.ml | 18 | ||||
| -rw-r--r-- | lib/system.mli | 20 |
11 files changed, 75 insertions, 44 deletions
diff --git a/lib/control.ml b/lib/control.ml index e67cd8b38d..3fbeb168c4 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -85,4 +85,7 @@ let timeout_fun = match Sys.os_type with | "Unix" | "Cygwin" -> { timeout = unix_timeout } | _ -> { timeout = windows_timeout } -let timeout n f e = timeout_fun.timeout n f e +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 diff --git a/lib/control.mli b/lib/control.mli index 415e054625..59e2a15158 100644 --- a/lib/control.mli +++ b/lib/control.mli @@ -24,3 +24,8 @@ val check_for_interrupt : unit -> unit 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. *) + +(** 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 } +val set_timeout : timeout -> unit diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4 index d6c340f691..61eb1dafdf 100644 --- a/lib/coqProject_file.ml4 +++ b/lib/coqProject_file.ml4 @@ -8,6 +8,14 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +(* This needs to go trou feedback as it is invoked from IDEs, but + ideally we would like to make this independent so it can be + bootstrapped. *) + +(* Note the problem with the error invokation below calling exit... *) +(* let error msg = Feedback.msg_error msg *) +let warning msg = Feedback.msg_warning Pp.(str msg) + type arg_source = CmdLine | ProjectFile type 'a sourced = { thing : 'a; source : arg_source } @@ -122,7 +130,7 @@ let process_cmd_line orig_dir proj args = let sourced x = { thing = x; source = if !parsing_project_file then ProjectFile else CmdLine } in let orig_dir = (* avoids turning foo.v in ./foo.v *) if orig_dir = "." then "" else orig_dir in - let error s = Format.eprintf "@[%a]@@\n%!" Pp.pp_with Pp.(str (s^".")); exit 1 in + let error s = (Format.eprintf "Error: @[%s@].@\n%!" s; exit 1) in let mk_path d = let p = CUnix.correct_path d orig_dir in { path = CUnix.remove_path_dot (post_canonize p); @@ -140,7 +148,7 @@ let process_cmd_line orig_dir proj args = | ("-full"|"-opt") :: r -> aux { proj with use_ocamlopt = true } r | "-install" :: d :: r -> if proj.install_kind <> None then - Feedback.msg_warning (Pp.str "-install set more than once."); + (warning "-install set more than once.@\n%!"); let install = match d with | "user" -> UserInstall | "none" -> NoInstall @@ -167,8 +175,7 @@ let process_cmd_line orig_dir proj args = let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in let () = match proj.project_file with | None -> () - | Some _ -> Feedback.msg_warning (Pp.str - "Multiple project files are deprecated.") + | Some _ -> warning "Multiple project files are deprecated.@\n%!" in parsing_project_file := true; let proj = aux { proj with project_file = Some file } (parse file) in diff --git a/lib/flags.ml b/lib/flags.ml index 56940f1cf7..7e0065beba 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -57,8 +57,6 @@ let in_toplevel = ref false let profile = false -let ide_slave = ref false - let raw_print = ref false let we_are_parsing = ref false diff --git a/lib/flags.mli b/lib/flags.mli index 17776d68a4..02d8a3adc1 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -52,9 +52,6 @@ val in_toplevel : bool ref val profile : bool -(* -ide_slave: printing will be more verbose, will affect stm caching *) -val ide_slave : bool ref - (* development flag to detect race conditions, it should go away. *) val we_are_parsing : bool ref diff --git a/lib/rtree.ml b/lib/rtree.ml index 0e371025ea..e1c6a4c4d6 100644 --- a/lib/rtree.ml +++ b/lib/rtree.ml @@ -94,22 +94,28 @@ let is_node t = Node _ -> true | _ -> false - let rec map f t = match t with Param(i,j) -> Param(i,j) | Node (a,sons) -> Node (f a, Array.map (map f) sons) | Rec(j,defs) -> Rec (j, Array.map (map f) defs) -let smartmap f t = match t with - Param _ -> t - | Node (a,sons) -> - let a'=f a and sons' = Array.smartmap (map f) sons in - if a'==a && sons'==sons then t - else Node (a',sons') - | Rec(j,defs) -> - let defs' = Array.smartmap (map f) defs in - if defs'==defs then t - else Rec(j,defs') +module Smart = +struct + + let map f t = match t with + Param _ -> t + | Node (a,sons) -> + let a'=f a and sons' = Array.Smart.map (map f) sons in + if a'==a && sons'==sons then t + else Node (a',sons') + | Rec(j,defs) -> + let defs' = Array.Smart.map (map f) defs in + if defs'==defs then t + else Rec(j,defs') + +end + +let smartmap = Smart.map (** Structural equality test, parametrized by an equality on elements *) diff --git a/lib/rtree.mli b/lib/rtree.mli index 8edfc3d37f..5ab14f6039 100644 --- a/lib/rtree.mli +++ b/lib/rtree.mli @@ -74,13 +74,22 @@ val incl : ('a -> 'a -> bool) -> ('a -> 'a -> 'a option) -> 'a -> 'a t -> 'a t - (** Iterators *) +(** See also [Smart.map] *) val map : ('a -> 'b) -> 'a t -> 'b t -(** [(smartmap f t) == t] if [(f a) ==a ] for all nodes *) 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 + + (** [(Smart.map f t) == t] if [(f a) ==a ] for all nodes *) + val map : ('a -> 'a) -> 'a t -> 'a t + +end diff --git a/lib/spawn.ml b/lib/spawn.ml index 6d2ad37872..63e9e452cb 100644 --- a/lib/spawn.ml +++ b/lib/spawn.ml @@ -10,7 +10,7 @@ let proto_version = 0 let prefer_sock = Sys.os_type = "Win32" -let accept_timeout = 2.0 +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 () diff --git a/lib/stateid.ml b/lib/stateid.ml index a258d50527..5485c4bf19 100644 --- a/lib/stateid.ml +++ b/lib/stateid.ml @@ -11,15 +11,11 @@ type t = int let initial = 1 let dummy = 0 -let fresh, in_range = +let fresh = let cur = ref initial in - (fun () -> incr cur; !cur), (fun id -> id >= 0 && id <= !cur) + fun () -> incr cur; !cur let to_string = string_of_int -let of_int id = - (* Coqide too to parse ids too, but cannot check if they are valid. - * Hence we check for validity only if we are an ide slave. *) - if !Flags.ide_slave then assert (in_range id); - id +let of_int id = id let to_int id = id let newer_than id1 id2 = id1 > id2 diff --git a/lib/system.ml b/lib/system.ml index dfede29e8f..f109c71925 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -116,18 +116,6 @@ let where_in_path ?(warn=true) path filename = let f = Filename.concat lpe filename in if file_exists_respecting_case lpe filename then [lpe,f] else [])) -let where_in_path_rex path rex = - search path (fun lpe -> - try - let files = Sys.readdir lpe in - CList.map_filter (fun name -> - try - ignore(Str.search_forward rex name 0); - Some (lpe,Filename.concat lpe name) - with Not_found -> None) - (Array.to_list files) - with Sys_error _ -> []) - let find_file_in_path ?(warn=true) paths filename = if not (Filename.is_implicit filename) then (* the name is considered to be a physical name and we use the file @@ -312,3 +300,9 @@ let with_time ~batch f x = let msg2 = if batch then "" else " (failure)" in Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); raise e + +let get_toplevel_path top = + let dir = Filename.dirname Sys.argv.(0) in + let exe = if Sys.(os_type = "Win32" || os_type = "Cygwin") then ".exe" else "" in + let eff = if Dynlink.is_native then ".opt" else ".byte" in + dir ^ Filename.dir_sep ^ top ^ eff ^ exe diff --git a/lib/system.mli b/lib/system.mli index 3349dfea30..a34280037c 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -50,8 +50,6 @@ val is_in_path : CUnix.load_path -> string -> bool val is_in_system_path : string -> bool val where_in_path : ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string -val where_in_path_rex : - CUnix.load_path -> Str.regexp -> (CUnix.physical_path * string) list val find_file_in_path : ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string @@ -107,3 +105,21 @@ val time_difference : time -> time -> float (** in seconds *) val fmt_time_difference : time -> time -> Pp.t val with_time : batch:bool -> ('a -> 'b) -> 'a -> 'b + +(** [get_toplevel_path program] builds a complete path to the + executable denoted by [program]. This involves: + + - locating the directory: we don't rely on PATH as to make calls to + /foo/bin/coqtop chose the right /foo/bin/coqproofworker + + - adding the proper suffixes: .opt/.byte depending on the current + mode, + .exe if in windows. + + Note that this function doesn't check that the executable actually + exists. This is left back to caller, as well as the choice of + fallback strategy. We could add a fallback strategy here but it is + better not to as in most cases if this function fails to construct + the right name you want you execution to fail rather than fall into + choosing some random binary from the system-wide installation of + Coq. *) +val get_toplevel_path : string -> string |