From 164c6861860e6b52818c031f901ffeff91fca16a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 26 Jan 2016 16:56:33 +0100 Subject: Imported Upstream version 8.5 --- tools/compat5.ml | 2 +- tools/compat5.mlp | 2 +- tools/compat5b.ml | 2 +- tools/compat5b.mlp | 2 +- tools/coq_makefile.ml | 2 +- tools/coq_tex.ml | 2 +- tools/coqc.ml | 2 +- tools/coqdep.ml | 61 +++++++++++++++++++++++++++++++---------------- tools/coqdep_boot.ml | 14 +++++------ tools/coqdep_common.ml | 38 ++++++++++++++++++++++------- tools/coqdep_common.mli | 24 ++++++++++++++++--- tools/coqdep_lexer.mli | 2 +- tools/coqdep_lexer.mll | 2 +- tools/coqdoc/alpha.ml | 2 +- tools/coqdoc/alpha.mli | 2 +- tools/coqdoc/cdglobals.ml | 2 +- tools/coqdoc/cpretty.mli | 2 +- tools/coqdoc/cpretty.mll | 2 +- tools/coqdoc/index.ml | 2 +- tools/coqdoc/index.mli | 2 +- tools/coqdoc/main.ml | 2 +- tools/coqdoc/output.ml | 2 +- tools/coqdoc/output.mli | 2 +- tools/coqdoc/tokens.ml | 2 +- tools/coqdoc/tokens.mli | 2 +- tools/coqmktop.ml | 4 ++-- tools/coqwc.mll | 2 +- tools/coqworkmgr.ml | 2 +- tools/fake_ide.ml | 2 +- tools/gallina.ml | 2 +- tools/gallina_lexer.mll | 2 +- 31 files changed, 126 insertions(+), 67 deletions(-) (limited to 'tools') diff --git a/tools/compat5.ml b/tools/compat5.ml index 041ced00..33c1cd60 100644 --- a/tools/compat5.ml +++ b/tools/compat5.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* +\n"; - eprintf " extra options:\n"; - eprintf " -coqlib dir : set the coq standard library directory\n"; - eprintf " -exclude-dir f : skip subdirectories named 'f' during -R search\n"; + eprintf " usage: coqdep [options] +\n"; + eprintf " options:\n"; + eprintf " -c : Also print the dependencies of caml modules (=ocamldep).\n"; + (* Does not work anymore *) + (* eprintf " -w : Print informations on missing or wrong \"Declare + ML Module\" commands in coq files.\n"; *) + (* Does not work anymore: *) + (* eprintf " -D : Prints the missing ocmal module names. No dependency computed.\n"; *) + eprintf " -boot : For coq developpers, prints dependencies over coq library files (omitted by default).\n"; + eprintf " -sort : output the given file name ordered by dependencies\n"; + eprintf " -noglob | -no-glob : \n"; + eprintf " -I dir -as logname : add (non recursively) dir to coq load path under logical name logname\n"; + eprintf " -I dir : add (non recursively) dir to ocaml path\n"; + eprintf " -R dir -as logname : add and import dir recursively to coq load path under logical name logname\n"; (* deprecate? *) + eprintf " -R dir logname : add and import dir recursively to coq load path under logical name logname\n"; + eprintf " -Q dir logname : add (recusively) and open (non recursively) dir to coq load path under logical name logname\n"; eprintf " -dumpgraph f : print a dot dependency graph in file 'f'\n"; + eprintf " -dumpgraphbox f : print a dot dependency graph box in file 'f'\n"; + eprintf " -exclude-dir dir : skip subdirectories named 'dir' during -R/-Q search\n"; + eprintf " -coqlib dir : set the coq standard library directory\n"; + eprintf " -suffix s : \n"; + eprintf " -slash : deprecated, no effect\n"; exit 1 let split_period = Str.split (Str.regexp (Str.quote ".")) @@ -442,16 +459,17 @@ let rec parse = function | "-boot" :: ll -> option_boot := true; parse ll | "-sort" :: ll -> option_sort := true; parse ll | ("-noglob" | "-no-glob") :: ll -> option_noglob := true; parse ll - | "-I" :: r :: "-as" :: ln :: ll -> add_dir add_known r []; - add_dir add_known r (split_period ln); - parse ll + | "-I" :: r :: "-as" :: ln :: ll -> + add_rec_dir_no_import add_known r []; + add_rec_dir_no_import add_known r (split_period ln); + parse ll | "-I" :: r :: "-as" :: [] -> usage () | "-I" :: r :: ll -> add_caml_dir r; parse ll | "-I" :: [] -> usage () - | "-R" :: r :: "-as" :: ln :: ll -> add_rec_dir add_known r (split_period ln); parse ll + | "-R" :: r :: "-as" :: ln :: ll -> add_rec_dir_import add_known r (split_period ln); parse ll | "-R" :: r :: "-as" :: [] -> usage () - | "-R" :: r :: ln :: ll -> add_rec_dir add_known r (split_period ln); parse ll - | "-Q" :: r :: ln :: ll -> add_dir add_known r (split_period ln); parse ll + | "-R" :: r :: ln :: ll -> add_rec_dir_import add_known r (split_period ln); parse ll + | "-Q" :: r :: ln :: ll -> add_rec_dir_no_import add_known r (split_period ln); parse ll | "-R" :: ([] | [_]) -> usage () | "-dumpgraph" :: f :: ll -> option_dump := Some (false, f); parse ll | "-dumpgraphbox" :: f :: ll -> option_dump := Some (true, f); parse ll @@ -471,23 +489,26 @@ let rec parse = function let coqdep () = if Array.length Sys.argv < 2 then usage (); parse (List.tl (Array.to_list Sys.argv)); + (* Add current dir with empty logical path if not set by options above. *) + (try ignore (Coqdep_common.find_dir_logpath (Sys.getcwd())) + with Not_found -> add_norec_dir_import add_known "." []); if not Coq_config.has_natdynlink then option_natdynlk := false; (* NOTE: These directories are searched from last to first *) if !option_boot then begin - add_rec_dir add_known "theories" ["Coq"]; - add_rec_dir add_known "plugins" ["Coq"]; - add_rec_dir (fun _ -> add_caml_known) "theories" ["Coq"]; - add_rec_dir (fun _ -> add_caml_known) "plugins" ["Coq"]; + add_rec_dir_import add_known "theories" ["Coq"]; + add_rec_dir_import add_known "plugins" ["Coq"]; + add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"]; + add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"]; end else begin Envars.set_coqlib ~fail:Errors.error; let coqlib = Envars.coqlib () in - add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"]; - add_rec_dir add_coqlib_known (coqlib//"plugins") ["Coq"]; + add_rec_dir_import add_coqlib_known (coqlib//"theories") ["Coq"]; + add_rec_dir_import add_coqlib_known (coqlib//"plugins") ["Coq"]; let user = coqlib//"user-contrib" in - if Sys.file_exists user then add_dir add_coqlib_known user []; - List.iter (fun s -> add_dir add_coqlib_known s []) + if Sys.file_exists user then add_rec_dir_no_import add_coqlib_known user []; + List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s []) (Envars.xdg_dirs (fun x -> Pp.msg_warning (Pp.str x))); - List.iter (fun s -> add_dir add_coqlib_known s []) Envars.coqpath; + List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s []) Envars.coqpath; end; List.iter (fun (f,d) -> add_mli_known f d ".mli") !mliAccu; List.iter (fun (f,d) -> add_mllib_known f d ".mllib") !mllibAccu; diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml index 64ce66d2..6fc82683 100644 --- a/tools/coqdep_boot.ml +++ b/tools/coqdep_boot.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* add_caml_known) "." ["Coq"]; + add_rec_dir_import add_known "." []; + add_rec_dir_import (fun _ -> add_caml_known) "." ["Coq"]; end else begin - add_rec_dir add_known "theories" ["Coq"]; - add_rec_dir add_known "plugins" ["Coq"]; + add_rec_dir_import add_known "theories" ["Coq"]; + add_rec_dir_import add_known "plugins" ["Coq"]; add_caml_dir "tactics"; - add_rec_dir (fun _ -> add_caml_known) "theories" ["Coq"]; - add_rec_dir (fun _ -> add_caml_known) "plugins" ["Coq"]; + add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"]; + add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"]; end; if !option_c then mL_dependencies (); coq_dependencies () diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index c1111375..58c8e884 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* dir | None -> "." in absolute_dir dir // basename +(** [find_dir_logpath dir] Return the logical path of directory [dir] + if it has been given one. Raise [Not_found] otherwise. In + particular we can check if "." has been attributed a logical path + after processing all options and silently give the default one if + it hasn't. We may also use this to warn if ap hysical path is met + twice.*) +let register_dir_logpath,find_dir_logpath = + let tbl: (string, string list) Hashtbl.t = Hashtbl.create 19 in + let reg physdir logpath = Hashtbl.add tbl (absolute_dir physdir) logpath in + let fnd physdir = Hashtbl.find tbl (absolute_dir physdir) in + reg,fnd + let file_name s = function | None -> s | Some "." -> s @@ -339,7 +351,8 @@ let escape = Buffer.contents s' let compare_file f1 f2 = - absolute_dir (Filename.dirname f1) = absolute_dir (Filename.dirname f2) + absolute_file_name (Filename.basename f1) (Some (Filename.dirname f1)) + = absolute_file_name (Filename.basename f2) (Some (Filename.dirname f2)) let canonize f = let f' = absolute_dir (Filename.dirname f) // Filename.basename f in @@ -514,11 +527,13 @@ let add_known recur phys_dir log_dir f = List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths | _ -> () -(* Visits all the directories under [dir], including [dir], - or just [dir] if [recur=false] *) - +(** Visit directory [phys_dir] (recursively unless [recur=false]) and + apply function add_file to each regular file encountered. + [log_dir] is the logical name of the [phys_dir]. + [add_file] takes both directory names and the file. *) let rec add_directory recur add_file phys_dir log_dir = let dirh = opendir phys_dir in + register_dir_logpath phys_dir log_dir; try while true do let f = readdir dirh in @@ -531,24 +546,29 @@ let rec add_directory recur add_file phys_dir log_dir = if StrSet.mem f !norec_dirnames then () else if StrSet.mem phys_f !norec_dirs then () - else + else (* TODO: warn if already seen this physycal dir? *) add_directory recur add_file phys_f (log_dir@[f]) | S_REG -> add_file phys_dir log_dir f | _ -> () done with End_of_file -> closedir dirh +(** Simply add this directory and imports it, no subdirs. This is used + by the implicit adding of the current path (which is not recursive). *) +let add_norec_dir_import add_file phys_dir log_dir = + try add_directory false (add_file true) phys_dir log_dir with Unix_error _ -> () + (** -Q semantic: go in subdirs but only full logical paths are known. *) -let add_dir add_file phys_dir log_dir = +let add_rec_dir_no_import add_file phys_dir log_dir = try add_directory true (add_file false) phys_dir log_dir with Unix_error _ -> () (** -R semantic: go in subdirs and suffixes of logical paths are known. *) -let add_rec_dir add_file phys_dir log_dir = +let add_rec_dir_import add_file phys_dir log_dir = handle_unix_error (add_directory true (add_file true) phys_dir) log_dir (** -I semantic: do not go in subdirs. *) let add_caml_dir phys_dir = - handle_unix_error (add_directory true add_caml_known phys_dir) [] + handle_unix_error (add_directory false add_caml_known phys_dir) [] let rec treat_file old_dirname old_name = diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index d610a055..97bdfaef 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* string list + val option_c : bool ref val option_noglob : bool ref val option_boot : bool ref @@ -47,9 +55,19 @@ val add_directory : bool -> (string -> string list -> string -> unit) -> string -> string list -> unit val add_caml_dir : string -> unit -val add_dir : + +(** Simply add this directory and imports it, no subdirs. This is used + by the implicit adding of the current path. *) +val add_norec_dir_import : + (bool -> string -> string list -> string -> unit) -> string -> string list -> unit + +(** -Q semantic: go in subdirs but only full logical paths are known. *) +val add_rec_dir_no_import : (bool -> string -> string list -> string -> unit) -> string -> string list -> unit -val add_rec_dir : + +(** -R semantic: go in subdirs and suffixes of logical paths are known. *) +val add_rec_dir_import : (bool -> string -> string list -> string -> unit) -> string -> string list -> unit + val treat_file : dir -> string -> unit val error_cannot_parse : string -> int * int -> 'a diff --git a/tools/coqdep_lexer.mli b/tools/coqdep_lexer.mli index 84c9ba79..bb17fdf9 100644 --- a/tools/coqdep_lexer.mli +++ b/tools/coqdep_lexer.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*