aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/cWarnings.ml4
-rw-r--r--lib/cWarnings.mli2
-rw-r--r--lib/control.ml5
-rw-r--r--lib/control.mli5
-rw-r--r--lib/coqProject_file.ml415
-rw-r--r--lib/flags.ml11
-rw-r--r--lib/flags.mli35
-rw-r--r--lib/loc.ml5
-rw-r--r--lib/loc.mli4
-rw-r--r--lib/rtree.ml28
-rw-r--r--lib/rtree.mli11
-rw-r--r--lib/spawn.ml2
-rw-r--r--lib/stateid.ml10
-rw-r--r--lib/system.ml18
-rw-r--r--lib/system.mli20
15 files changed, 103 insertions, 72 deletions
diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
index 92c86eaea3..fda25a0a60 100644
--- a/lib/cWarnings.ml
+++ b/lib/cWarnings.ml
@@ -22,11 +22,8 @@ type t = {
let warnings : (string, t) Hashtbl.t = Hashtbl.create 97
let categories : (string, string list) Hashtbl.t = Hashtbl.create 97
-let current_loc = ref None
let flags = ref ""
-let set_current_loc loc = current_loc := loc
-
let get_flags () = !flags
let add_warning_in_category ~name ~category =
@@ -170,7 +167,6 @@ let create ~name ~category ?(default=Enabled) pp =
set_flags !flags;
fun ?loc x ->
let w = Hashtbl.find warnings name in
- let loc = Option.append loc !current_loc in
match w.status with
| Disabled -> ()
| AsError -> CErrors.user_err ?loc (pp x)
diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli
index fa96b18c8c..f97a53c4d7 100644
--- a/lib/cWarnings.mli
+++ b/lib/cWarnings.mli
@@ -10,8 +10,6 @@
type status = Disabled | Enabled | AsError
-val set_current_loc : Loc.t option -> unit
-
val create : name:string -> category:string -> ?default:status ->
('a -> Pp.t) -> ?loc:Loc.t -> 'a -> unit
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 8491873e07..7e0065beba 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -57,10 +57,7 @@ let in_toplevel = ref false
let profile = false
-let ide_slave = ref false
-
let raw_print = ref false
-let univ_print = ref false
let we_are_parsing = ref false
@@ -160,11 +157,3 @@ let print_mod_uid = ref false
let profile_ltac = ref false
let profile_ltac_cutoff = ref 2.0
-
-let dump_bytecode = ref false
-let set_dump_bytecode = (:=) dump_bytecode
-let get_dump_bytecode () = !dump_bytecode
-
-let dump_lambda = ref false
-let set_dump_lambda = (:=) dump_lambda
-let get_dump_lambda () = !dump_lambda
diff --git a/lib/flags.mli b/lib/flags.mli
index 85aaf879f3..02d8a3adc1 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -10,6 +10,25 @@
(** Global options of the system. *)
+(** WARNING: don't add new entries to this file!
+
+ This file is own its way to deprecation in favor of a purely
+ functional state, but meanwhile it will contain options that are
+ truly global to the system such as [compat] or [debug]
+
+ If you are thinking about adding a global flag, well, just
+ don't. First of all, options make testins exponentially more
+ expensive, due to the growth of flag combinations. So please make
+ some effort in order for your idea to work in a configuration-free
+ manner.
+
+ If you absolutely must pass an option to your new system, then do
+ so as a functional argument so flags are exposed to unit
+ testing. Then, register such parameters with the proper
+ state-handling mechanism of the top-level subsystem of Coq.
+
+ *)
+
(** Command-line flags *)
val boot : bool ref
@@ -33,18 +52,12 @@ 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
(* Set Printing All flag. For some reason it is a global flag *)
val raw_print : bool ref
-(* Univ print flag, never set anywere. Maybe should belong to Univ? *)
-val univ_print : bool ref
-
type compat_version = V8_6 | V8_7 | Current
val compat_version : compat_version ref
val version_compare : compat_version -> compat_version -> int
@@ -129,13 +142,3 @@ val print_mod_uid : bool ref
val profile_ltac : bool ref
val profile_ltac_cutoff : float ref
-
-(** Dump the bytecode after compilation (for debugging purposes) *)
-val dump_bytecode : bool ref
-val set_dump_bytecode : bool -> unit
-val get_dump_bytecode : unit -> bool
-
-(** Dump the VM lambda code after compilation (for debugging purposes) *)
-val dump_lambda : bool ref
-val set_dump_lambda : bool -> unit
-val get_dump_lambda : unit -> bool
diff --git a/lib/loc.ml b/lib/loc.ml
index 6f5283aab8..1a09091bff 100644
--- a/lib/loc.ml
+++ b/lib/loc.ml
@@ -62,6 +62,11 @@ let merge_opt l1 l2 = match l1, l2 with
| None, Some l -> Some l
| Some l1, Some l2 -> Some (merge l1 l2)
+let finer l1 l2 = match l1, l2 with
+ | None, _ -> false
+ | Some l , None -> true
+ | Some l1, Some l2 -> l1.fname = l2.fname && merge l1 l2 = l2
+
let unloc loc = (loc.bp, loc.ep)
let shift_loc kb kp loc = { loc with bp = loc.bp + kb ; ep = loc.ep + kp }
diff --git a/lib/loc.mli b/lib/loc.mli
index 813c45fbb3..23df1ebd9a 100644
--- a/lib/loc.mli
+++ b/lib/loc.mli
@@ -42,6 +42,10 @@ val merge : t -> t -> t
val merge_opt : t option -> t option -> t option
(** Merge locations, usually generating the largest possible span *)
+val finer : t option -> t option -> bool
+(** Answers [true] when the first location is more defined, or, when
+ both defined, included in the second one *)
+
val shift_loc : int -> int -> t -> t
(** [shift_loc loc n p] shifts the beginning of location by [n] and
the end by [p]; it is assumed that the shifts do not change the
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 05:33:33 +0000