summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/cErrors.ml4
-rw-r--r--lib/cErrors.mli2
-rw-r--r--lib/cWarnings.ml6
-rw-r--r--lib/coqProject_file.ml (renamed from lib/coqProject_file.ml4)79
-rw-r--r--lib/envars.ml2
-rw-r--r--lib/flags.ml21
-rw-r--r--lib/flags.mli37
-rw-r--r--lib/future.ml6
-rw-r--r--lib/future.mli4
-rw-r--r--lib/lib.mllib1
-rw-r--r--lib/pp.ml75
-rw-r--r--lib/pp.mli19
-rw-r--r--lib/pp_diff.ml303
-rw-r--r--lib/pp_diff.mli116
-rw-r--r--lib/rtree.ml28
-rw-r--r--lib/rtree.mli11
-rw-r--r--lib/spawn.ml59
-rw-r--r--lib/spawn.mli4
-rw-r--r--lib/stateid.ml10
-rw-r--r--lib/system.ml22
-rw-r--r--lib/system.mli20
-rw-r--r--lib/util.ml4
22 files changed, 690 insertions, 143 deletions
diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index 97502211..811fcf40 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -47,8 +47,6 @@ exception AlreadyDeclared of Pp.t (* for already declared Schemes *)
let alreadydeclared pps = raise (AlreadyDeclared(pps))
exception Timeout
-exception Drop
-exception Quit
let handle_stack = ref []
@@ -126,7 +124,7 @@ end
let noncritical = function
| Sys.Break | Out_of_memory | Stack_overflow
| Assert_failure _ | Match_failure _ | Anomaly _
- | Timeout | Drop | Quit -> false
+ | Timeout -> false
| Invalid_argument "equal: functional value" -> false
| _ -> true
[@@@ocaml.warning "+52"]
diff --git a/lib/cErrors.mli b/lib/cErrors.mli
index ec34dd62..4e2fe762 100644
--- a/lib/cErrors.mli
+++ b/lib/cErrors.mli
@@ -53,8 +53,6 @@ val invalid_arg : ?loc:Loc.t -> string -> 'a
val todo : string -> unit
exception Timeout
-exception Drop
-exception Quit
(** [register_handler h] registers [h] as a handler.
When an expression is printed with [print e], it
diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
index fda25a0a..0cf989e4 100644
--- a/lib/cWarnings.ml
+++ b/lib/cWarnings.ml
@@ -120,7 +120,7 @@ let uniquize_flags_rev flags =
(** [normalize_flags] removes redundant warnings. Unknown warnings are kept
because they may be declared in a plugin that will be linked later. *)
-let normalize_flags ~silent warnings =
+let normalize_flags warnings =
let warnings = cut_before_all_rev warnings in
uniquize_flags_rev warnings
@@ -130,7 +130,7 @@ let normalize_flags_string s =
if is_none_keyword s then s
else
let flags = flags_of_string s in
- let flags = normalize_flags ~silent:false flags in
+ let flags = normalize_flags flags in
string_of_flags flags
let parse_warnings items =
@@ -146,7 +146,7 @@ let parse_flags s =
else begin
Flags.make_warn true;
let flags = flags_of_string s in
- let flags = normalize_flags ~silent:true flags in
+ let flags = normalize_flags flags in
parse_warnings flags;
string_of_flags flags
end
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml
index d6c340f6..c2bcd73f 100644
--- a/lib/coqProject_file.ml4
+++ b/lib/coqProject_file.ml
@@ -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 }
@@ -82,30 +90,50 @@ let rec post_canonize f =
exception Parsing_error of string
-let rec parse_string = parser
- | [< '' ' | '\n' | '\t' >] -> ""
- | [< 'c; s >] -> (String.make 1 c)^(parse_string s)
- | [< >] -> ""
-and parse_string2 = parser
- | [< ''"' >] -> ""
- | [< 'c; s >] -> (String.make 1 c)^(parse_string2 s)
- | [< >] -> raise (Parsing_error "unterminated string")
-and parse_skip_comment = parser
- | [< ''\n'; s >] -> s
- | [< 'c; s >] -> parse_skip_comment s
- | [< >] -> [< >]
-and parse_args = parser
- | [< '' ' | '\n' | '\t'; s >] -> parse_args s
- | [< ''#'; s >] -> parse_args (parse_skip_comment s)
- | [< ''"'; str = parse_string2; s >] -> ("" ^ str) :: parse_args s
- | [< 'c; str = parse_string; s >] -> ((String.make 1 c) ^ str) :: (parse_args s)
- | [< >] -> []
+let buffer buf =
+ let ans = Buffer.contents buf in
+ let () = Buffer.clear buf in
+ ans
+
+let rec parse_string buf s = match Stream.next s with
+| ' ' | '\n' | '\t' -> buffer buf
+| c ->
+ let () = Buffer.add_char buf c in
+ parse_string buf s
+| exception Stream.Failure -> buffer buf
+
+and parse_string2 buf s = match Stream.next s with
+| '"' -> buffer buf
+| c ->
+ let () = Buffer.add_char buf c in
+ parse_string2 buf s
+| exception Stream.Failure -> raise (Parsing_error "unterminated string")
+
+and parse_skip_comment s = match Stream.next s with
+| '\n' -> ()
+| _ -> parse_skip_comment s
+| exception Stream.Failure -> ()
+
+and parse_args buf accu s = match Stream.next s with
+| ' ' | '\n' | '\t' -> parse_args buf accu s
+| '#' ->
+ let () = parse_skip_comment s in
+ parse_args buf accu s
+| '"' ->
+ let str = parse_string2 buf s in
+ parse_args buf (str :: accu) s
+| c ->
+ let () = Buffer.add_char buf c in
+ let str = parse_string buf s in
+ parse_args buf (str :: accu) s
+| exception Stream.Failure -> accu
let parse f =
let c = open_in f in
- let res = parse_args (Stream.of_channel c) in
+ let buf = Buffer.create 64 in
+ let res = parse_args buf [] (Stream.of_channel c) in
close_in c;
- res
+ List.rev res
;;
(* Copy from minisys.ml, since we don't see that file here *)
@@ -122,7 +150,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);
@@ -135,12 +163,12 @@ let process_cmd_line orig_dir proj args =
error "Use \"-install none\" instead of \"-no-install\""
| "-custom" :: _ ->
error "Use \"-extra[-phony] target deps command\" instead of \"-custom command deps target\""
-
+
| ("-no-opt"|"-byte") :: r -> aux { proj with use_ocamlopt = false } r
| ("-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 +195,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
@@ -182,7 +209,7 @@ let process_cmd_line orig_dir proj args =
error "Output file must be in the current directory";
if proj.makefile <> None then
error "Option -o given more than once";
- aux { proj with makefile = Some file } r
+ aux { proj with makefile = Some file } r
| v :: "=" :: def :: r ->
aux { proj with defs = proj.defs @ [sourced (v,def)] } r
| "-arg" :: a :: r ->
diff --git a/lib/envars.ml b/lib/envars.ml
index be82bfe9..3ee0c710 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -110,6 +110,7 @@ let check_file_else ~dir ~file oth =
if Sys.file_exists (path / file) then path else oth ()
let guess_coqlib fail =
+ getenv_else "COQLIB" (fun () ->
let prelude = "theories/Init/Prelude.vo" in
check_file_else ~dir:Coq_config.coqlibsuffix ~file:prelude
(fun () ->
@@ -117,6 +118,7 @@ let guess_coqlib fail =
then Coq_config.coqlib
else
fail "cannot guess a path for Coq libraries; please use -coqlib option")
+ )
(** coqlib is now computed once during coqtop initialization *)
diff --git a/lib/flags.ml b/lib/flags.ml
index 8491873e..458186b7 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
@@ -69,25 +66,25 @@ 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_6 | V8_7 | Current
+type compat_version = V8_7 | V8_8 | Current
let compat_version = ref Current
let version_compare v1 v2 = match v1, v2 with
- | V8_6, V8_6 -> 0
- | V8_6, _ -> -1
- | _, V8_6 -> 1
| V8_7, V8_7 -> 0
| V8_7, _ -> -1
| _, V8_7 -> 1
+ | V8_8, V8_8 -> 0
+ | V8_8, _ -> -1
+ | _, V8_8 -> 1
| Current, Current -> 0
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_6 -> "8.6"
| V8_7 -> "8.7"
+ | V8_8 -> "8.8"
| Current -> "current"
(* Translate *)
@@ -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 85aaf879..9562e8fc 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,19 +52,13 @@ 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
+type compat_version = V8_7 | V8_8 | Current
val compat_version : compat_version ref
val version_compare : compat_version -> compat_version -> int
val version_strictly_greater : compat_version -> bool
@@ -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/future.ml b/lib/future.ml
index 7a5b6f69..b372bedc 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -49,7 +49,7 @@ end
module UUIDMap = Map.Make(UUID)
module UUIDSet = Set.Make(UUID)
-type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation]
+type 'a assignment = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation]
(* Val is not necessarily a final state, so the
computation restarts from the state stocked into Val *)
@@ -103,7 +103,7 @@ let from_here ?(fix_exn=id) v = create fix_exn (Val v)
let fix_exn_of ck = let _, _, fix_exn, _ = get ck in fix_exn
let create_delegate ?(blocking=true) ~name fix_exn =
- let assignement signal ck = fun v ->
+ let assignment signal ck = fun v ->
let _, _, fix_exn, c = get ck in
assert (match !c with Delegated _ -> true | _ -> false);
begin match v with
@@ -118,7 +118,7 @@ let create_delegate ?(blocking=true) ~name fix_exn =
(fun () -> Mutex.lock lock; Condition.wait cond lock; Mutex.unlock lock),
(fun () -> Mutex.lock lock; Condition.broadcast cond; Mutex.unlock lock) in
let ck = create ~name fix_exn (Delegated wait) in
- ck, assignement signal ck
+ ck, assignment signal ck
(* TODO: get rid of try/catch to be stackless *)
let rec compute ck : 'a value =
diff --git a/lib/future.mli b/lib/future.mli
index d9e8c87b..55f05518 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -70,10 +70,10 @@ val fix_exn_of : 'a computation -> fix_exn
(* Run remotely, returns the function to assign.
If not blocking (the default) it raises NotReady if forced before the
delegate assigns it. *)
-type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation]
+type 'a assignment = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation]
val create_delegate :
?blocking:bool -> name:string ->
- fix_exn -> 'a computation * ('a assignement -> unit)
+ fix_exn -> 'a computation * ('a assignment -> unit)
(* Given a computation that is_exn, replace it by another one *)
val replace : 'a computation -> 'a computation -> unit
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 08918594..41b3622a 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -6,6 +6,7 @@ Control
Util
Pp
+Pp_diff
Stateid
Loc
Feedback
diff --git a/lib/pp.ml b/lib/pp.ml
index cd81f6e7..7f132686 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -139,7 +139,7 @@ let v n s = Ppcmd_box(Pp_vbox n,s)
let hv n s = Ppcmd_box(Pp_hvbox n,s)
let hov n s = Ppcmd_box(Pp_hovbox n,s)
-(* Opening and closed of tags *)
+(* Opening and closing of tags *)
let tag t s = Ppcmd_tag(t,s)
(* In new syntax only double quote char is escaped by repeating it *)
@@ -167,6 +167,20 @@ let rec pr_com ft s =
Some s2 -> Format.pp_force_newline ft (); pr_com ft s2
| None -> ()
+let start_pfx = "start."
+let end_pfx = "end."
+
+let split_pfx pfx str =
+ let (str_len, pfx_len) = (String.length str, String.length pfx) in
+ if str_len >= pfx_len && (String.sub str 0 pfx_len) = pfx then
+ (pfx, String.sub str pfx_len (str_len - pfx_len)) else ("", str);;
+
+let split_tag tag =
+ let (pfx, ttag) = split_pfx start_pfx tag in
+ if pfx <> "" then (pfx, ttag) else
+ let (pfx, ttag) = split_pfx end_pfx tag in
+ (pfx, ttag);;
+
(* pretty printing functions *)
let pp_with ft pp =
let cpp_open_box = function
@@ -297,3 +311,62 @@ let prvect_with_sep sep elem v = prvecti_with_sep sep (fun _ -> elem) v
let prvect elem v = prvect_with_sep mt elem v
let surround p = hov 1 (str"(" ++ p ++ str")")
+
+(*** DEBUG code ***)
+
+let db_print_pp fmt pp =
+ let open Format in
+ let block_type fmt btype =
+ let (bt, v) =
+ match btype with
+ | Pp_hbox v -> ("Pp_hbox", v)
+ | Pp_vbox v -> ("Pp_vbox", v)
+ | Pp_hvbox v -> ("Pp_hvbox", v)
+ | Pp_hovbox v -> ("Pp_hovbox", v)
+ in
+ fprintf fmt "%s %d" bt v
+ in
+ let rec db_print_pp_r indent pp =
+ let ind () = fprintf fmt "%s" (String.make (2 * indent) ' ') in
+ ind();
+ match pp with
+ | Ppcmd_empty ->
+ fprintf fmt "Ppcmd_empty@;"
+ | Ppcmd_string str ->
+ fprintf fmt "Ppcmd_string '%s'@;" str
+ | Ppcmd_glue list ->
+ fprintf fmt "Ppcmd_glue@;";
+ List.iter (fun x -> db_print_pp_r (indent + 1) (repr x)) list;
+ | Ppcmd_box (block, pp) ->
+ fprintf fmt "Ppcmd_box %a@;" block_type block;
+ db_print_pp_r (indent + 1) (repr pp);
+ | Ppcmd_tag (tag, pp) ->
+ fprintf fmt "Ppcmd_tag %s@;" tag;
+ db_print_pp_r (indent + 1) (repr pp);
+ | Ppcmd_print_break (i, j) ->
+ fprintf fmt "Ppcmd_print_break %d %d@;" i j
+ | Ppcmd_force_newline ->
+ fprintf fmt "Ppcmd_force_newline@;"
+ | Ppcmd_comment list ->
+ fprintf fmt "Ppcmd_comment@;";
+ List.iter (fun x -> ind(); (fprintf fmt "%s@;" x)) list
+ in
+ pp_open_vbox fmt 0;
+ db_print_pp_r 0 pp;
+ pp_close_box fmt ();
+ pp_print_flush fmt ()
+
+let db_string_of_pp pp =
+ Format.asprintf "%a" db_print_pp pp
+
+let rec flatten pp =
+ match pp with
+ | Ppcmd_glue l -> Ppcmd_glue (List.concat (List.map
+ (fun x -> let x = flatten x in
+ match x with
+ | Ppcmd_glue l2 -> l2
+ | p -> [p])
+ l))
+ | Ppcmd_box (block, pp) -> Ppcmd_box (block, flatten pp)
+ | Ppcmd_tag (tag, pp) -> Ppcmd_tag (tag, flatten pp)
+ | p -> p
diff --git a/lib/pp.mli b/lib/pp.mli
index f3a0a29b..ed31daa5 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -189,3 +189,22 @@ val pr_vertical_list : ('b -> t) -> 'b list -> t
val pp_with : Format.formatter -> t -> unit
val string_of_ppcmds : t -> string
+
+
+(** Tag prefix to start a multi-token diff span *)
+val start_pfx : string
+
+(** Tag prefix to end a multi-token diff span *)
+val end_pfx : string
+
+(** Split a tag into prefix and base tag *)
+val split_tag : string -> string * string
+
+(** Print the Pp in tree form for debugging *)
+val db_print_pp : Format.formatter -> t -> unit
+
+(** Print the Pp in tree form for debugging, return as a string *)
+val db_string_of_pp : t -> string
+
+(** Combine nested Ppcmd_glues *)
+val flatten : t -> t
diff --git a/lib/pp_diff.ml b/lib/pp_diff.ml
new file mode 100644
index 00000000..7b4b1eab
--- /dev/null
+++ b/lib/pp_diff.ml
@@ -0,0 +1,303 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \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) *)
+(************************************************************************)
+
+(* DEBUG/UNIT TEST *)
+let cfprintf oc = Printf.(kfprintf (fun oc -> fprintf oc "") oc)
+let log_out_ch = ref stdout
+let cprintf s = cfprintf !log_out_ch s
+
+
+module StringDiff = Diff2.Make(struct
+ type elem = String.t
+ type t = elem array
+ let get t i = Array.get t i
+ let length t = Array.length t
+end)
+
+type diff_type =
+ [ `Removed
+ | `Added
+ | `Common
+ ]
+
+type diff_list = StringDiff.elem Diff2.edit list
+
+(* debug print diff data structure *)
+let db_print_diffs fmt diffs =
+ let open Format in
+ let print_diff = function
+ | `Common (opos, npos, s) ->
+ fprintf fmt "Common '%s' opos = %d npos = %d\n" s opos npos;
+ | `Removed (pos, s) ->
+ fprintf fmt "Removed '%s' opos = %d\n" s pos;
+ | `Added (pos, s) ->
+ fprintf fmt "Added '%s' npos = %d\n" s pos;
+ in
+ pp_open_vbox fmt 0;
+ List.iter print_diff diffs;
+ pp_close_box fmt ();
+ pp_print_flush fmt ()
+
+let string_of_diffs diffs =
+ Format.asprintf "%a" db_print_diffs diffs
+
+(* Adjust the diffs returned by the Myers algorithm to reduce the span of the
+changes. This gives more natural-looking diffs.
+
+While the Myers algorithm minimizes the number of changes between two
+sequences, it doesn't minimize the span of the changes. For example,
+representing elements in common in lower case and inserted elements in upper
+case (but ignoring case in the algorithm), ABabC and abABC both have 3 changes
+(A, B and C). However the span of the first sequence is 5 elements (ABabC)
+while the span of the second is 3 elements (ABC).
+
+The algorithm modifies the changes iteratively, for example ABabC -> aBAbC -> abABC
+
+dtype: identifies which of Added OR Removed to use; the other one is ignored.
+diff_list: output from the Myers algorithm
+*)
+let shorten_diff_span dtype diff_list =
+ let changed = ref false in
+ let diffs = Array.of_list diff_list in
+ let len = Array.length diffs in
+ let vinfo index =
+ match diffs.(index) with
+ | `Common (opos, npos, s) -> (`Common, opos, npos, s)
+ | `Removed (pos, s) -> (`Removed, pos, 0, s)
+ | `Added (pos, s) -> (`Added, 0, pos, s) in
+ let get_variant index =
+ let (v, _, _, _) = vinfo index in
+ v in
+ let get_str index =
+ let (_, _, _, s) = vinfo index in
+ s in
+
+ let iter start len lt incr = begin
+ let src = ref start in
+ let dst = ref start in
+ while (lt !src len) do
+ if (get_variant !src) = dtype then begin
+ if (lt !dst !src) then
+ dst := !src;
+ while (lt !dst len) && (get_variant !dst) <> `Common do
+ dst := !dst + incr;
+ done;
+ if (lt !dst len) && (get_str !src) = (get_str !dst) then begin
+ (* swap diff *)
+ let (_, c_opos, c_npos, str) = vinfo !dst
+ and (_, v_opos, v_npos, _) = vinfo !src in
+ changed := true;
+ if dtype = `Added then begin
+ diffs.(!src) <- `Common (c_opos, v_npos, str);
+ diffs.(!dst) <- `Added (c_npos, str);
+ end else begin
+ diffs.(!src) <- `Common (v_opos, c_npos, str);
+ diffs.(!dst) <- `Removed (c_opos, str)
+ end
+ end
+ end;
+ src := !src + incr
+ done
+ end in
+
+ iter 0 len (<) 1; (* left to right *)
+ iter (len-1) (-1) (>) (-1); (* right to left *)
+ if !changed then Array.to_list diffs else diff_list;;
+
+let has_changes diffs =
+ let rec has_changes_r diffs added removed =
+ match diffs with
+ | `Added _ :: t -> has_changes_r t true removed
+ | `Removed _ :: t -> has_changes_r t added true
+ | h :: t -> has_changes_r t added removed
+ | [] -> (added, removed) in
+ has_changes_r diffs false false;;
+
+(* get the Myers diff of 2 lists of strings *)
+let diff_strs old_strs new_strs =
+ let diffs = List.rev (StringDiff.diff old_strs new_strs) in
+ shorten_diff_span `Removed (shorten_diff_span `Added diffs);;
+
+(* Default string tokenizer. Makes each character a separate strin.
+Whitespace is not ignored. Doesn't handle UTF-8 differences well. *)
+let def_tokenize_string s =
+ let limit = (String.length s) - 1 in
+ let strs : string list ref = ref [] in
+ for i = 0 to limit do
+ strs := (String.make 1 s.[i]) :: !strs
+ done;
+ List.rev !strs
+
+(* get the Myers diff of 2 strings *)
+let diff_str ?(tokenize_string=def_tokenize_string) old_str new_str =
+ let old_toks = Array.of_list (tokenize_string old_str)
+ and new_toks = Array.of_list (tokenize_string new_str) in
+ diff_strs old_toks new_toks;;
+
+let get_dinfo = function
+ | `Common (_, _, s) -> (`Common, s)
+ | `Removed (_, s) -> (`Removed, s)
+ | `Added (_, s) -> (`Added, s)
+
+[@@@ocaml.warning "-32"]
+let string_of_diff_type = function
+ | `Common -> "Common"
+ | `Removed -> "Removed"
+ | `Added -> "Added"
+[@@@ocaml.warning "+32"]
+
+let wrap_in_bg diff_tag pp =
+ let open Pp in
+ (tag (Pp.start_pfx ^ diff_tag ^ ".bg") (str "")) ++ pp ++
+ (tag (Pp.end_pfx ^ diff_tag ^ ".bg") (str ""))
+
+exception Diff_Failure of string
+
+let add_diff_tags which pp diffs =
+ let open Pp in
+ let diff_tag = if which = `Added then "diff.added" else "diff.removed" in
+ let diffs : diff_list ref = ref diffs in
+ let in_diff = ref false in (* true = buf chars need a tag *)
+ let in_span = ref false in (* true = last pp had a start tag *)
+ let trans = ref false in (* true = this diff starts/ends highlight *)
+ let buf = Buffer.create 16 in
+ let acc_pp = ref [] in
+ let diff_str, diff_ind, diff_len = ref "", ref 0, ref 0 in
+ let prev_dtype, dtype, next_dtype = ref `Common, ref `Common, ref `Common in
+ let is_white c = List.mem c [' '; '\t'; '\n'; '\r'] in
+
+ let skip () =
+ while !diffs <> [] &&
+ (let (t, _) = get_dinfo (List.hd !diffs) in
+ t <> `Common && t <> which)
+ do
+ diffs := List.tl !diffs
+ done
+ in
+
+ let put_tagged case =
+ if Buffer.length buf > 0 then begin
+ let pp = str (Buffer.contents buf) in
+ Buffer.clear buf;
+ let tagged = match case with
+ | "" -> pp
+ | "tag" -> tag diff_tag pp
+ | "start" -> in_span := true; tag (start_pfx ^ diff_tag) pp
+ | "end" -> in_span := false; tag (end_pfx ^ diff_tag) pp
+ | _ -> raise (Diff_Failure "invalid tag id in put_tagged, should be impossible") in
+ acc_pp := tagged :: !acc_pp
+ end
+ in
+
+ let output_pps () =
+ let next_diff_char_hl = if !diff_ind < !diff_len then !dtype = which else !next_dtype = which in
+ let tag = if not !in_diff then ""
+ else if !in_span then
+ if next_diff_char_hl then "" else "end"
+ else
+ if next_diff_char_hl then "start" else "tag" in
+ put_tagged tag; (* flush any remainder *)
+ let l = !acc_pp in
+ acc_pp := [];
+ match List.length l with
+ | 0 -> str ""
+ | 1 -> List.hd l
+ | _ -> seq (List.rev l)
+ in
+
+ let maybe_next_diff () =
+ if !diff_ind = !diff_len && (skip(); !diffs <> []) then begin
+ let (t, s) = get_dinfo (List.hd !diffs) in
+ diff_str := s; diff_ind := 0; diff_len := String.length !diff_str;
+ diffs := List.tl !diffs; skip();
+ prev_dtype := !dtype;
+ dtype := t;
+ next_dtype := (match !diffs with
+ | diff2 :: _ -> let (nt, _) = get_dinfo diff2 in nt
+ | [] -> `Common);
+ trans := !dtype <> !prev_dtype
+ end;
+ in
+
+ let s_char c =
+ maybe_next_diff ();
+ (* matching first should handle tokens with spaces, e.g. in comments/strings *)
+ if !diff_ind < !diff_len && c = !diff_str.[!diff_ind] then begin
+ if !dtype = which && !trans && !diff_ind = 0 then begin
+ put_tagged "";
+ in_diff := true
+ end;
+ Buffer.add_char buf c;
+ diff_ind := !diff_ind + 1;
+ if !dtype = which && !dtype <> !next_dtype && !diff_ind = !diff_len then begin
+ put_tagged (if !in_span then "end" else "tag");
+ in_diff := false
+ end
+ end else if is_white c then
+ Buffer.add_char buf c
+ else begin
+ cprintf "mismatch: expected '%c' but got '%c'\n" !diff_str.[!diff_ind] c;
+ raise (Diff_Failure "string mismatch, shouldn't happen")
+ end
+ in
+
+ (* rearrange so existing tags are inside diff tags, provided that those tags
+ only contain Ppcmd_string's. Other cases (e.g. tag of a box) are not supported. *)
+ (* todo: Is there a better way to do this in OCaml without multiple 'repr's? *)
+ let reorder_tags child pp_tag pp =
+ match repr child with
+ | Ppcmd_tag (t1, pp) -> tag t1 (tag pp_tag pp)
+ | Ppcmd_glue l ->
+ if List.exists (fun x ->
+ match repr x with
+ | Ppcmd_tag (_, _) -> true
+ | _ -> false) l
+ then seq (List.map (fun x ->
+ match repr x with
+ | Ppcmd_tag (t2, pp2) -> tag t2 (tag pp_tag pp2)
+ | pp2 -> tag pp_tag (unrepr pp2)) l)
+ else child
+ | _ -> tag pp_tag child
+ in
+
+ let rec add_tags_r pp =
+ let r_pp = repr pp in
+ match r_pp with
+ | Ppcmd_string s -> String.iter s_char s; output_pps ()
+ | Ppcmd_glue l -> seq (List.map add_tags_r l)
+ | Ppcmd_box (block_type, pp) -> unrepr (Ppcmd_box (block_type, add_tags_r pp))
+ | Ppcmd_tag (pp_tag, pp) -> reorder_tags (add_tags_r pp) pp_tag pp
+ | _ -> pp
+ in
+ let (has_added, has_removed) = has_changes !diffs in
+ let rv = add_tags_r pp in
+ skip ();
+ if !diffs <> [] then
+ raise (Diff_Failure "left-over diff info at end of Pp.t, should be impossible");
+ if has_added || has_removed then wrap_in_bg diff_tag rv else rv;;
+
+let diff_pp ?(tokenize_string=def_tokenize_string) o_pp n_pp =
+ let open Pp in
+ let o_str = string_of_ppcmds o_pp in
+ let n_str = string_of_ppcmds n_pp in
+ let diffs = diff_str ~tokenize_string o_str n_str in
+ (add_diff_tags `Removed o_pp diffs, add_diff_tags `Added n_pp diffs);;
+
+let diff_pp_combined ?(tokenize_string=def_tokenize_string) ?(show_removed=false) o_pp n_pp =
+ let open Pp in
+ let o_str = string_of_ppcmds o_pp in
+ let n_str = string_of_ppcmds n_pp in
+ let diffs = diff_str ~tokenize_string o_str n_str in
+ let (_, has_removed) = has_changes diffs in
+ let added = add_diff_tags `Added n_pp diffs in
+ if show_removed && has_removed then
+ let removed = add_diff_tags `Removed o_pp diffs in
+ (v 0 (removed ++ cut() ++ added))
+ else added;;
diff --git a/lib/pp_diff.mli b/lib/pp_diff.mli
new file mode 100644
index 00000000..03468271
--- /dev/null
+++ b/lib/pp_diff.mli
@@ -0,0 +1,116 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \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) *)
+(************************************************************************)
+
+(**
+Computes the differences between 2 Pp's and adds additional tags to a Pp
+to highlight them. Strings are split into tokens using the Coq lexer,
+then the lists of tokens are diffed using the Myers algorithm. A fixup routine,
+shorten_diff_span, shortens the span of the diff result in some cases.
+
+Highlights use 4 tags to specify the color and underline/strikeout. These are
+"diffs.added", "diffs.removed", "diffs.added.bg" and "diffs.removed.bg". The
+first two are for added or removed text; the last two are for unmodified parts
+of a modified item. Diffs that span multiple strings in the Pp are tagged with
+"start.diff.*" and "end.diff.*", but only on the first and last strings of the span.
+
+If the inputs are not acceptable to the lexer, break the strings into
+lists of tokens and call diff_strs, then add_diff_tags with a Pp.t that matches
+the input lists of strings. Tokens that the lexer doesn't return exactly as they
+appeared in the input will raise an exception in add_diff_tags (e.g. comments
+and quoted strings). Fixing that requires tweaking the lexer.
+
+Limitations/Possible enhancements:
+
+- Make diff_pp immune to unlexable strings by adding a flag to the lexer.
+*)
+
+(** Compute the diff between two Pp.t structures and return
+versions of each with diffs highlighted as (old, new) *)
+val diff_pp : ?tokenize_string:(string -> string list) -> Pp.t -> Pp.t -> Pp.t * Pp.t
+
+(** Compute the diff between two Pp.t structures and return
+a highlighted Pp.t. If [show_removed] is true, show separate lines for
+removals and additions, otherwise only show additions *)
+val diff_pp_combined : ?tokenize_string:(string -> string list) -> ?show_removed:bool -> Pp.t -> Pp.t -> Pp.t
+
+(** Raised if the diff fails *)
+exception Diff_Failure of string
+
+module StringDiff :
+sig
+ type elem = String.t
+ type t = elem array
+end
+
+type diff_type =
+ [ `Removed
+ | `Added
+ | `Common
+ ]
+
+type diff_list = StringDiff.elem Diff2.edit list
+
+(** Compute the difference between 2 strings in terms of tokens, using the
+lexer to identify tokens.
+
+If the strings are not lexable, this routine will raise Diff_Failure.
+(I expect to modify the lexer soon so this won't happen.)
+
+Therefore you should catch any exceptions. The workaround for now is for the
+caller to tokenize the strings itself and then call diff_strs.
+*)
+val diff_str : ?tokenize_string:(string -> string list) -> string -> string -> StringDiff.elem Diff2.edit list
+
+(** Compute the differences between 2 lists of strings, treating the strings
+in the lists as indivisible units.
+*)
+val diff_strs : StringDiff.t -> StringDiff.t -> StringDiff.elem Diff2.edit list
+
+(** Generate a new Pp that adds tags marking diffs to a Pp structure:
+which: either `Added or `Removed, indicates which type of diffs to add
+pp: the original structure. For `Added, must be the new pp passed to diff_pp
+ For `Removed, must be the old pp passed to diff_pp. Passing the wrong one
+ will likely raise Diff_Failure.
+diffs: the diff list returned by diff_pp
+
+Diffs of single strings in the Pp are tagged with "diff.added" or "diff.removed".
+Diffs that span multiple strings in the Pp are tagged with "start.diff.*" or
+"end.diff.*", but only on the first and last strings of the span.
+
+Ppcmd_strings will be split into multiple Ppcmd_strings if a diff starts or ends
+in the middle of the string. Whitespace just before or just after a diff will
+not be part of the highlight.
+
+Prexisting tags in pp may contain only a single Ppcmd_string. Those tags will be
+placed inside the diff tags to ensure proper nesting of tags within spans of
+"start.diff.*" ... "end.diff.*".
+
+Under some "impossible" conditions, this routine may raise Diff_Failure.
+If you want to make your call especially bulletproof, catch this
+exception, print a user-visible message, then recall this routine with
+the first argument set to None, which will skip the diff.
+*)
+val add_diff_tags : diff_type -> Pp.t -> StringDiff.elem Diff2.edit list -> Pp.t
+
+(** Returns a boolean pair (added, removed) for [diffs] where a true value
+indicates that something was added/removed in the diffs.
+*)
+val has_changes : diff_list -> bool * bool
+
+val get_dinfo : StringDiff.elem Diff2.edit -> diff_type * string
+
+(** Returns a modified [pp] with the background highlighted with
+"start.<diff_tag>.bg" and "end.<diff_tag>.bg" tags at the beginning
+and end of the returned Pp.t
+*)
+val wrap_in_bg : string -> Pp.t -> Pp.t
+
+(** Displays the diffs to a printable format for debugging *)
+val string_of_diffs : diff_list -> string
diff --git a/lib/rtree.ml b/lib/rtree.ml
index 0e371025..e1c6a4c4 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 8edfc3d3..5ab14f60 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 63e9e452..0652623b 100644
--- a/lib/spawn.ml
+++ b/lib/spawn.ml
@@ -15,14 +15,12 @@ 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 ()
-type req = ReqDie | ReqStats | Hello of int * int
-type resp = RespStats of Gc.stat
+type req = ReqDie | Hello of int * int
module type Control = sig
type handle
val kill : handle -> unit
- val stats : handle -> Gc.stat
val wait : handle -> Unix.process_status
val unixpid : handle -> int
val uid : handle -> string
@@ -43,7 +41,6 @@ module type MainLoopModel = sig
end
(* Common code *)
-let assert_ b s = if not b then CErrors.anomaly (Pp.str s)
(* According to http://caml.inria.fr/mantis/view.php?id=5325
* you can't use the same socket for both writing and reading (may change
@@ -125,14 +122,26 @@ let filter_args args =
Array.of_list (aux (Array.to_list args))
let spawn_with_control prefer_sock env prog args =
- let control_sock, control_sock_name = mk_socket_channel () in
- let extra = [| "-control-channel"; control_sock_name |] in
- let args = Array.append extra (filter_args args) in
+ (* on non-Unix systems we create a control channel *)
+ let not_Unix = Sys.os_type <> "Unix" in
+ let args = filter_args args in
+ let args, control_sock =
+ if not_Unix then
+ let control_sock, control_sock_name = mk_socket_channel () in
+ let extra = [| "-control-channel"; control_sock_name |] in
+ Array.append extra args, Some control_sock
+ else
+ args, None in
let (pid, cin, cout, s), is_sock =
- if Sys.os_type <> "Unix" || prefer_sock
+ if not_Unix (* pipes only work well on Unix *) || prefer_sock
then spawn_sock env prog args, true
else spawn_pipe env prog args, false in
- let _, oob_resp, oob_req = accept control_sock in
+ let oob_resp, oob_req =
+ if not_Unix then
+ let _, oob_resp, oob_req = accept (Option.get control_sock) in
+ Some oob_resp, Some oob_req
+ else
+ None, None in
pid, oob_resp, oob_req, cin, cout, s, is_sock
let output_death_sentence pid oob_req =
@@ -146,8 +155,8 @@ module Async(ML : MainLoopModel) = struct
type process = {
cin : in_channel;
cout : out_channel;
- oob_resp : in_channel;
- oob_req : out_channel;
+ oob_resp : in_channel option;
+ oob_req : out_channel option;
gchan : ML.async_chan;
pid : int;
mutable watch : ML.watch_id option;
@@ -166,11 +175,11 @@ let kill ({ pid = unixpid; oob_resp; oob_req; cin; cout; alive; watch } as p) =
if not alive then prerr_endline "This process is already dead"
else begin try
Option.iter ML.remove_watch watch;
- output_death_sentence (uid p) oob_req;
+ Option.iter (output_death_sentence (uid p)) oob_req;
close_in_noerr cin;
close_out_noerr cout;
- close_in_noerr oob_resp;
- close_out_noerr oob_req;
+ Option.iter close_in_noerr oob_resp;
+ Option.iter close_out_noerr oob_req;
if Sys.os_type = "Unix" then Unix.kill unixpid 9;
p.watch <- None
with e -> prerr_endline ("kill: "^Printexc.to_string e) end
@@ -199,12 +208,6 @@ let spawn ?(prefer_sock=prefer_sock) ?(env=Unix.environment ())
);
p, cout
-let stats { oob_req; oob_resp; alive } =
- assert_ alive "This process is dead.";
- output_value oob_req ReqStats;
- flush oob_req;
- input_value oob_resp
-
let rec wait p =
(* On windows kill is not reliable, so wait may never return. *)
if Sys.os_type = "Unix" then
@@ -221,8 +224,8 @@ module Sync () = struct
type process = {
cin : in_channel;
cout : out_channel;
- oob_resp : in_channel;
- oob_req : out_channel;
+ oob_resp : in_channel option;
+ oob_req : out_channel option;
pid : int;
mutable alive : bool;
}
@@ -242,20 +245,14 @@ let kill ({ pid = unixpid; oob_req; oob_resp; cin; cout; alive } as p) =
p.alive <- false;
if not alive then prerr_endline "This process is already dead"
else begin try
- output_death_sentence (uid p) oob_req;
+ Option.iter (output_death_sentence (uid p)) oob_req;
close_in_noerr cin;
close_out_noerr cout;
- close_in_noerr oob_resp;
- close_out_noerr oob_req;
+ Option.iter close_in_noerr oob_resp;
+ Option.iter close_out_noerr oob_req;
if Sys.os_type = "Unix" then Unix.kill unixpid 9;
with e -> prerr_endline ("kill: "^Printexc.to_string e) end
-let stats { oob_req; oob_resp; alive } =
- assert_ alive "This process is dead.";
- output_value oob_req ReqStats;
- flush oob_req;
- let RespStats g = input_value oob_resp in g
-
let rec wait p =
(* On windows kill is not reliable, so wait may never return. *)
if Sys.os_type = "Unix" then
diff --git a/lib/spawn.mli b/lib/spawn.mli
index c7a56349..944aa27a 100644
--- a/lib/spawn.mli
+++ b/lib/spawn.mli
@@ -25,7 +25,6 @@ module type Control = sig
type handle
val kill : handle -> unit
- val stats : handle -> Gc.stat
val wait : handle -> Unix.process_status
val unixpid : handle -> int
@@ -76,6 +75,5 @@ end
(* This is exported to separate the Spawned module, that for simplicity assumes
* Threads so it is in a separate file *)
-type req = ReqDie | ReqStats | Hello of int * int
+type req = ReqDie | Hello of int * int
val proto_version : int
-type resp = RespStats of Gc.stat
diff --git a/lib/stateid.ml b/lib/stateid.ml
index a258d505..5485c4bf 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 dfede29e..4bc56beb 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -83,7 +83,9 @@ let file_exists_respecting_case path f =
let rec aux f =
let bf = Filename.basename f in
let df = Filename.dirname f in
- (String.equal df "." || aux df)
+ (* When [df] is the same as [f], it means that the root of the file system
+ has been reached. There is no point in looking further up. *)
+ (String.equal df "." || String.equal f df || aux df)
&& exists_in_dir_respecting_case (Filename.concat path df) bf
in (!trust_file_cache || Sys.file_exists (Filename.concat path f)) && aux f
@@ -116,18 +118,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 +302,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.executable_name 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 3349dfea..a3428003 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
diff --git a/lib/util.ml b/lib/util.ml
index 7d7d380b..38d73d34 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -38,8 +38,8 @@ let is_blank = function
module Empty =
struct
- type t
- let abort (x : t) = assert false
+ type t = { abort : 'a. 'a }
+ let abort (x : t) = x.abort
end
(* Strings *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-26 06:39:08 +0000