From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- lib/cErrors.ml | 4 +- lib/cErrors.mli | 2 - lib/cWarnings.ml | 6 +- lib/coqProject_file.ml | 282 ++++++++++++++++++++++++++++++++++++++++++++ lib/coqProject_file.ml4 | 255 ---------------------------------------- lib/envars.ml | 2 + lib/flags.ml | 21 +--- lib/flags.mli | 37 +++--- lib/future.ml | 6 +- lib/future.mli | 4 +- lib/lib.mllib | 1 + lib/pp.ml | 75 +++++++++++- lib/pp.mli | 19 +++ lib/pp_diff.ml | 303 ++++++++++++++++++++++++++++++++++++++++++++++++ lib/pp_diff.mli | 116 ++++++++++++++++++ lib/rtree.ml | 28 +++-- lib/rtree.mli | 11 +- lib/spawn.ml | 59 +++++----- lib/spawn.mli | 4 +- lib/stateid.ml | 10 +- lib/system.ml | 22 ++-- lib/system.mli | 20 +++- lib/util.ml | 4 +- 23 files changed, 919 insertions(+), 372 deletions(-) create mode 100644 lib/coqProject_file.ml delete mode 100644 lib/coqProject_file.ml4 create mode 100644 lib/pp_diff.ml create mode 100644 lib/pp_diff.mli (limited to 'lib') 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.ml b/lib/coqProject_file.ml new file mode 100644 index 00000000..c2bcd73f --- /dev/null +++ b/lib/coqProject_file.ml @@ -0,0 +1,282 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* 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 buf = Buffer.create 64 in + let res = parse_args buf [] (Stream.of_channel c) in + close_in c; + List.rev res +;; + +(* Copy from minisys.ml, since we don't see that file here *) +let exists_dir dir = + let rec strip_trailing_slash dir = + let len = String.length dir in + if len > 0 && (dir.[len-1] = '/' || dir.[len-1] = '\\') + then strip_trailing_slash (String.sub dir 0 (len-1)) else dir in + try Sys.is_directory (strip_trailing_slash dir) with Sys_error _ -> false + + +let process_cmd_line orig_dir proj args = + let parsing_project_file = ref (proj.project_file <> None) in + 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 "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); + canonical_path = CUnix.canonical_path_name p } in + let rec aux proj = function + | [] -> proj + | "-impredicative-set" :: _ -> + error "Use \"-arg -impredicative-set\" instead of \"-impredicative-set\"" + | "-no-install" :: _ -> + 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 + (warning "-install set more than once.@\n%!"); + let install = match d with + | "user" -> UserInstall + | "none" -> NoInstall + | "global" -> TraditionalInstall + | _ -> error ("invalid option \""^d^"\" passed to -install") in + aux { proj with install_kind = Some install } r + | "-extra" :: target :: dependencies :: command :: r -> + let tgt = { target; dependencies; phony = false; command } in + aux { proj with extra_targets = proj.extra_targets @ [sourced tgt] } r + | "-extra-phony" :: target :: dependencies :: command :: r -> + let tgt = { target; dependencies; phony = true; command } in + aux { proj with extra_targets = proj.extra_targets @ [sourced tgt] } r + + | "-Q" :: d :: lp :: r -> + aux { proj with q_includes = proj.q_includes @ [sourced (mk_path d,lp)] } r + | "-I" :: d :: r -> + aux { proj with ml_includes = proj.ml_includes @ [sourced (mk_path d)] } r + | "-R" :: d :: lp :: r -> + aux { proj with r_includes = proj.r_includes @ [sourced (mk_path d,lp)] } r + + | "-f" :: file :: r -> + if !parsing_project_file then + raise (Parsing_error ("Invalid option -f in project file " ^ Option.get proj.project_file)); + let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in + let () = match proj.project_file with + | None -> () + | 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 + parsing_project_file := false; + aux proj r + + | "-o" :: file :: r -> + if !parsing_project_file then + raise (Parsing_error ("Invalid option -o in project file " ^ Option.get proj.project_file)); + if String.contains file '/' then + 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 + | v :: "=" :: def :: r -> + aux { proj with defs = proj.defs @ [sourced (v,def)] } r + | "-arg" :: a :: r -> + aux { proj with extra_args = proj.extra_args @ [sourced a] } r + | f :: r -> + let f = CUnix.correct_path f orig_dir in + let proj = + if exists_dir f then { proj with subdirs = proj.subdirs @ [sourced f] } + else match CUnix.get_extension f with + | ".v" -> + { proj with v_files = proj.v_files @ [sourced f] } + | ".ml" -> { proj with ml_files = proj.ml_files @ [sourced f] } + | ".ml4" -> { proj with ml4_files = proj.ml4_files @ [sourced f] } + | ".mli" -> { proj with mli_files = proj.mli_files @ [sourced f] } + | ".mllib" -> { proj with mllib_files = proj.mllib_files @ [sourced f] } + | ".mlpack" -> { proj with mlpack_files = proj.mlpack_files @ [sourced f] } + | _ -> raise (Parsing_error ("Unknown option "^f)) in + aux proj r + in + aux proj args + + (******************************* API ************************************) + +let cmdline_args_to_project ~curdir args = + process_cmd_line curdir (mk_project None None None true) args + +let read_project_file f = + process_cmd_line (Filename.dirname f) + (mk_project (Some f) None (Some NoInstall) true) (parse f) + +let rec find_project_file ~from ~projfile_name = + let fname = Filename.concat from projfile_name in + if Sys.file_exists fname then Some fname + else + let newdir = Filename.dirname from in + if newdir = from then None + else find_project_file ~from:newdir ~projfile_name +;; + +let all_files { v_files; ml_files; mli_files; ml4_files; + mllib_files; mlpack_files } = + v_files @ mli_files @ ml4_files @ ml_files @ mllib_files @ mlpack_files + +let map_sourced_list f l = List.map (fun x -> f x.thing) l +;; + +let map_cmdline f l = CList.map_filter (function + | {thing=x; source=CmdLine} -> Some (f x) + | {source=ProjectFile} -> None) l + +let coqtop_args_from_project + { ml_includes; r_includes; q_includes; extra_args } += + let map = map_sourced_list in + let args = + map (fun { canonical_path = i } -> ["-I"; i]) ml_includes @ + map (fun ({ canonical_path = i }, l) -> ["-Q"; i; l]) q_includes @ + map (fun ({ canonical_path = p }, l) -> ["-R"; p; l]) r_includes @ + [map (fun x -> x) extra_args] in + List.flatten args +;; + +let filter_cmdline l = CList.map_filter + (function {thing; source=CmdLine} -> Some thing | {source=ProjectFile} -> None) + l +;; + +let forget_source {thing} = thing + +(* vim:set ft=ocaml: *) diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4 deleted file mode 100644 index d6c340f6..00000000 --- a/lib/coqProject_file.ml4 +++ /dev/null @@ -1,255 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* ] -> "" - | [< '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 parse f = - let c = open_in f in - let res = parse_args (Stream.of_channel c) in - close_in c; - res -;; - -(* Copy from minisys.ml, since we don't see that file here *) -let exists_dir dir = - let rec strip_trailing_slash dir = - let len = String.length dir in - if len > 0 && (dir.[len-1] = '/' || dir.[len-1] = '\\') - then strip_trailing_slash (String.sub dir 0 (len-1)) else dir in - try Sys.is_directory (strip_trailing_slash dir) with Sys_error _ -> false - - -let process_cmd_line orig_dir proj args = - let parsing_project_file = ref (proj.project_file <> None) in - 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 mk_path d = - let p = CUnix.correct_path d orig_dir in - { path = CUnix.remove_path_dot (post_canonize p); - canonical_path = CUnix.canonical_path_name p } in - let rec aux proj = function - | [] -> proj - | "-impredicative-set" :: _ -> - error "Use \"-arg -impredicative-set\" instead of \"-impredicative-set\"" - | "-no-install" :: _ -> - 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."); - let install = match d with - | "user" -> UserInstall - | "none" -> NoInstall - | "global" -> TraditionalInstall - | _ -> error ("invalid option \""^d^"\" passed to -install") in - aux { proj with install_kind = Some install } r - | "-extra" :: target :: dependencies :: command :: r -> - let tgt = { target; dependencies; phony = false; command } in - aux { proj with extra_targets = proj.extra_targets @ [sourced tgt] } r - | "-extra-phony" :: target :: dependencies :: command :: r -> - let tgt = { target; dependencies; phony = true; command } in - aux { proj with extra_targets = proj.extra_targets @ [sourced tgt] } r - - | "-Q" :: d :: lp :: r -> - aux { proj with q_includes = proj.q_includes @ [sourced (mk_path d,lp)] } r - | "-I" :: d :: r -> - aux { proj with ml_includes = proj.ml_includes @ [sourced (mk_path d)] } r - | "-R" :: d :: lp :: r -> - aux { proj with r_includes = proj.r_includes @ [sourced (mk_path d,lp)] } r - - | "-f" :: file :: r -> - if !parsing_project_file then - raise (Parsing_error ("Invalid option -f in project file " ^ Option.get proj.project_file)); - 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.") - in - parsing_project_file := true; - let proj = aux { proj with project_file = Some file } (parse file) in - parsing_project_file := false; - aux proj r - - | "-o" :: file :: r -> - if !parsing_project_file then - raise (Parsing_error ("Invalid option -o in project file " ^ Option.get proj.project_file)); - if String.contains file '/' then - 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 - | v :: "=" :: def :: r -> - aux { proj with defs = proj.defs @ [sourced (v,def)] } r - | "-arg" :: a :: r -> - aux { proj with extra_args = proj.extra_args @ [sourced a] } r - | f :: r -> - let f = CUnix.correct_path f orig_dir in - let proj = - if exists_dir f then { proj with subdirs = proj.subdirs @ [sourced f] } - else match CUnix.get_extension f with - | ".v" -> - { proj with v_files = proj.v_files @ [sourced f] } - | ".ml" -> { proj with ml_files = proj.ml_files @ [sourced f] } - | ".ml4" -> { proj with ml4_files = proj.ml4_files @ [sourced f] } - | ".mli" -> { proj with mli_files = proj.mli_files @ [sourced f] } - | ".mllib" -> { proj with mllib_files = proj.mllib_files @ [sourced f] } - | ".mlpack" -> { proj with mlpack_files = proj.mlpack_files @ [sourced f] } - | _ -> raise (Parsing_error ("Unknown option "^f)) in - aux proj r - in - aux proj args - - (******************************* API ************************************) - -let cmdline_args_to_project ~curdir args = - process_cmd_line curdir (mk_project None None None true) args - -let read_project_file f = - process_cmd_line (Filename.dirname f) - (mk_project (Some f) None (Some NoInstall) true) (parse f) - -let rec find_project_file ~from ~projfile_name = - let fname = Filename.concat from projfile_name in - if Sys.file_exists fname then Some fname - else - let newdir = Filename.dirname from in - if newdir = from then None - else find_project_file ~from:newdir ~projfile_name -;; - -let all_files { v_files; ml_files; mli_files; ml4_files; - mllib_files; mlpack_files } = - v_files @ mli_files @ ml4_files @ ml_files @ mllib_files @ mlpack_files - -let map_sourced_list f l = List.map (fun x -> f x.thing) l -;; - -let map_cmdline f l = CList.map_filter (function - | {thing=x; source=CmdLine} -> Some (f x) - | {source=ProjectFile} -> None) l - -let coqtop_args_from_project - { ml_includes; r_includes; q_includes; extra_args } -= - let map = map_sourced_list in - let args = - map (fun { canonical_path = i } -> ["-I"; i]) ml_includes @ - map (fun ({ canonical_path = i }, l) -> ["-Q"; i; l]) q_includes @ - map (fun ({ canonical_path = p }, l) -> ["-R"; p; l]) r_includes @ - [map (fun x -> x) extra_args] in - List.flatten args -;; - -let filter_cmdline l = CList.map_filter - (function {thing; source=CmdLine} -> Some thing | {source=ProjectFile} -> None) - l -;; - -let forget_source {thing} = thing - -(* vim:set ft=ocaml: *) 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 *) +(* 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 *) +(* 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..bg" and "end..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 *) -- cgit v1.2.3