diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /tools/coqdep.ml | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'tools/coqdep.ml')
-rw-r--r-- | tools/coqdep.ml | 517 |
1 files changed, 76 insertions, 441 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 91a7e6d0..fe930a1d 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -6,207 +6,46 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqdep.ml 12916 2010-04-10 15:18:17Z herbelin $ *) +(* $Id$ *) open Printf open Coqdep_lexer -open Unix +open Coqdep_common -let stderr = Pervasives.stderr -let stdout = Pervasives.stdout +(** The basic parts of coqdep (i.e. the parts used by [coqdep -boot]) + are now in [Coqdep_common]. The code that remains here concerns + the other options. Calling this complete coqdep with the [-boot] + option should be equivalent to calling [coqdep_boot]. +*) -let option_c = ref false let option_D = ref false let option_w = ref false -let option_i = ref false let option_sort = ref false -let option_glob = ref false -let option_slash = ref false -let suffixe = ref ".vo" -let suffixe_spec = ref ".vi" - -type dir = string option - -(* filename for printing *) -let (//) s1 s2 = - if !option_slash then s1^"/"^s2 else Filename.concat s1 s2 - -let (/) = Filename.concat - -let file_concat l = - if l=[] then "<empty>" else - List.fold_left (//) (List.hd l) (List.tl l) - -let make_ml_module_name filename = - (* Computes a ML Module name from its physical name *) - let fn = try Filename.chop_extension filename with _ -> filename in - let bn = Filename.basename fn in - String.capitalize bn - -(* Files specified on the command line *) -let mlAccu = ref ([] : (string * string * dir) list) -and mliAccu = ref ([] : (string * string * dir) list) -and vAccu = ref ([] : (string * string) list) - -(* Queue operations *) -let addQueue q v = q := v :: !q - -let safe_hash_add clq q (k,v) = - try - let v2 = Hashtbl.find q k in - if v<>v2 then - let rec add_clash = function - (k1,l1)::cltl when k=k1 -> (k1,v::l1)::cltl - | cl::cltl -> cl::add_clash cltl - | [] -> [(k,[v;v2])] in - clq := add_clash !clq; - (* overwrite previous bindings, as coqc does *) - Hashtbl.add q k v - with Not_found -> Hashtbl.add q k v - -(* Files found in the loadpaths *) - -let mlKnown = (Hashtbl.create 19 : (string, dir) Hashtbl.t) -let mliKnown = (Hashtbl.create 19 : (string, dir) Hashtbl.t) -let vKnown = (Hashtbl.create 19 : (string list, string) Hashtbl.t) -let coqlibKnown = (Hashtbl.create 19 : (string list, unit) Hashtbl.t) - -let clash_v = ref ([]: (string list * string list) list) - - -let warning_module_notfound f s = - eprintf "*** Warning : in file %s, library " f; - eprintf "%s.v is required and has not been found in loadpath !\n" - (String.concat "." s); - flush stderr - -let warning_notfound f s = - eprintf "*** Warning : in file %s, the file " f; - eprintf "%s.v is required and has not been found !\n" s; - flush stderr - -let warning_clash file dir = - match List.assoc dir !clash_v with - (f1::f2::fl) -> - let f = Filename.basename f1 in - let d1 = Filename.dirname f1 in - let d2 = Filename.dirname f2 in - let dl = List.map Filename.dirname (List.rev fl) in - eprintf - "*** Warning : in file %s, \n required library %s is ambiguous!\n (found %s.v in " - file (String.concat "." dir) f; - List.iter (fun s -> eprintf "%s, " s) dl; - eprintf "%s and %s)\n" d2 d1 - | _ -> assert false - -let safe_assoc verbose file k = - if verbose && List.mem_assoc k !clash_v then warning_clash file k; - Hashtbl.find vKnown k - -let absolute_dir dir = - let current = Sys.getcwd () in - Sys.chdir dir; - let dir' = Sys.getcwd () in - Sys.chdir current; - dir' - -let absolute_file_name basename odir = - let dir = match odir with Some dir -> dir | None -> "." in - absolute_dir dir // basename - -let file_name = function - | (s,None) -> file_concat s - | (s,Some ".") -> file_concat s - | (s,Some d) -> d // file_concat s - -let traite_fichier_ML md ext = - try - let chan = open_in (md ^ ext) in - let buf = Lexing.from_channel chan in - let deja_vu = ref [md] in - let a_faire = ref "" in - let a_faire_opt = ref "" in - begin try - while true do - let (Use_module str) = caml_action buf in - if List.mem str !deja_vu then - () - else begin - addQueue deja_vu str; - begin try - let mlidir = Hashtbl.find mliKnown str in - let filename = file_name ([str],mlidir) in - a_faire := !a_faire ^ " " ^ filename ^ ".cmi"; - with Not_found -> - try - let mldir = Hashtbl.find mlKnown str in - let filename = file_name ([str],mldir) in - a_faire := !a_faire ^ " " ^ filename ^ ".cmo"; - with Not_found -> () - end; - begin try - let mldir = Hashtbl.find mlKnown str in - let filename = file_name ([str],mldir) in - a_faire_opt := !a_faire_opt ^ " " ^ filename ^ ".cmx" - with Not_found -> - try - let mlidir = Hashtbl.find mliKnown str in - let filename = file_name ([str],mlidir) in - a_faire_opt := !a_faire_opt ^ " " ^ filename ^ ".cmi" - with Not_found -> () - end +let rec warning_mult suf iter = + let tab = Hashtbl.create 151 in + let check f d = + begin try + let d' = Hashtbl.find tab f in + if (Filename.dirname (file_name f d)) + <> (Filename.dirname (file_name f d')) then begin + eprintf "*** Warning : the file %s is defined twice!\n" (f ^ suf); + flush stderr end - done - with Fin_fichier -> () - end; - close_in chan; - (!a_faire, !a_faire_opt) - with Sys_error _ -> ("","") - -let cut_prefix p s = - let lp = String.length p in - let ls = String.length s in - if ls >= lp && String.sub s 0 lp = p then String.sub s lp (ls - lp) else s - -(* Makefile's escaping rules are awful: $ is escaped by doubling and - other special characters are escaped by backslash prefixing while - backslashes themselves must be escaped only if part of a sequence - followed by a special character (i.e. in case of ambiguity with a - use of it as escaping character). Moreover (even if not crucial) - it is apparently not possible to directly escape ';' and leading '\t'. *) - -let escape = - let s' = Buffer.create 10 in - fun s -> - Buffer.clear s'; - for i = 0 to String.length s - 1 do - let c = s.[i] in - if c = ' ' or c = '#' or c = ':' (* separators and comments *) - or c = '%' (* pattern *) - or c = '?' or c = '[' or c = ']' or c = '*' (* expansion in filenames *) - or i=0 && c = '~' && (String.length s = 1 || s.[1] = '/' || - 'A' <= s.[1] && s.[1] <= 'Z' || - 'a' <= s.[1] && s.[1] <= 'z') (* homedir expansion *) - then begin - let j = ref (i-1) in - while !j >= 0 && s.[!j] = '\\' do - Buffer.add_char s' '\\'; decr j (* escape all preceding '\' *) - done; - Buffer.add_char s' '\\'; - end; - if c = '$' then Buffer.add_char s' '$'; - Buffer.add_char s' c - done; - Buffer.contents s' - -let canonize f = - let f' = absolute_dir (Filename.dirname f) // Filename.basename f in - match List.filter (fun (_,full) -> f' = full) !vAccu with - | (f,_) :: _ -> f - | _ -> f + with Not_found -> () end; + Hashtbl.add tab f d + in + iter check + +let add_coqlib_known phys_dir log_dir f = + match get_extension f [".vo"] with + | (basename,".vo") -> + let name = log_dir@[basename] in + Hashtbl.add coqlibKnown [basename] (); + Hashtbl.add coqlibKnown name () + | _ -> () -let sort () = +let sort () = let seen = Hashtbl.create 97 in let rec loop file = let file = canonize file in @@ -217,13 +56,13 @@ let sort () = try while true do match coq_action lb with - | Require (_, sl) -> - List.iter - (fun s -> - try loop (Hashtbl.find vKnown s) + | Require sl -> + List.iter + (fun s -> + try loop (Hashtbl.find vKnown s) with Not_found -> ()) sl - | RequireString (_, s) -> loop s + | RequireString s -> loop s | _ -> () done with Fin_fichier -> @@ -233,82 +72,17 @@ let sort () = in List.iter (fun (name,_) -> loop name) !vAccu -let traite_fichier_Coq verbose f = - try - let chan = open_in f in - let buf = Lexing.from_channel chan in - let deja_vu_v = ref ([]: string list list) - and deja_vu_ml = ref ([] : string list) in - try - while true do - let tok = coq_action buf in - match tok with - | Require (spec,strl) -> - List.iter (fun str -> - if not (List.mem str !deja_vu_v) then begin - addQueue deja_vu_v str; - try - let file_str = safe_assoc verbose f str in - printf " %s%s" (canonize file_str) - (if spec then !suffixe_spec else !suffixe) - with Not_found -> - if verbose && not (Hashtbl.mem coqlibKnown str) then - warning_module_notfound f str - end) strl - | RequireString (spec,s) -> - let str = Filename.basename s in - if not (List.mem [str] !deja_vu_v) then begin - addQueue deja_vu_v [str]; - try - let file_str = Hashtbl.find vKnown [str] in - printf " %s%s" (canonize file_str) - (if spec then !suffixe_spec else !suffixe) - with Not_found -> - if not (Hashtbl.mem coqlibKnown [str]) then - warning_notfound f s - end - | Declare sl -> - List.iter - (fun str -> - let s = make_ml_module_name str in - if not (List.mem s !deja_vu_ml) then begin - addQueue deja_vu_ml s; - try - let mldir = Hashtbl.find mlKnown s in - let filename = file_name ([String.uncapitalize s],mldir) in - if Coq_config.has_natdynlink then - printf " %s.cmo %s.cmxs" filename filename - else - printf " %s.cmo" filename - with Not_found -> () - end) - sl - | Load str -> - let str = Filename.basename str in - if not (List.mem [str] !deja_vu_v) then begin - addQueue deja_vu_v [str]; - try - let file_str = Hashtbl.find vKnown [str] in - printf " %s.v" (canonize file_str) - with Not_found -> () - end - done - with Fin_fichier -> (); - close_in chan - with Sys_error _ -> () - - let (dep_tab : (string,string list) Hashtbl.t) = Hashtbl.create 151 - -let mL_dep_list b f = - try + +let mL_dep_list b f = + try Hashtbl.find dep_tab f with Not_found -> - let deja_vu = ref ([] : string list) in - try - let chan = open_in f in - let buf = Lexing.from_channel chan in - try + let deja_vu = ref ([] : string list) in + try + let chan = open_in f in + let buf = Lexing.from_channel chan in + try while true do let (Use_module str) = caml_action buf in if str = b then begin @@ -319,14 +93,14 @@ let mL_dep_list b f = if not (List.mem str !deja_vu) then addQueue deja_vu str done; [] with Fin_fichier -> begin - close_in chan; + close_in chan; let rl = List.rev !deja_vu in Hashtbl.add dep_tab f rl; rl end with Sys_error _ -> [] -let affiche_Declare f dcl = +let affiche_Declare f dcl = printf "\n*** In file %s: \n" f; printf "Declare ML Module"; List.iter (fun str -> printf " \"%s\"" str) dcl; @@ -341,33 +115,33 @@ let warning_Declare f dcl = eprintf ".\n"; flush stderr -let traite_Declare f = +let traite_Declare f = let decl_list = ref ([] : string list) in let rec treat = function - | s :: ll -> - let s' = make_ml_module_name s in - if (Hashtbl.mem mlKnown s') & not (List.mem s' !decl_list) then begin - let mldir = Hashtbl.find mlKnown s in - let fullname = file_name ([(String.uncapitalize s')],mldir) in - let depl = mL_dep_list s (fullname ^ ".ml") in - treat depl; - decl_list := s :: !decl_list - end; - treat ll + | s :: ll -> + let s' = basename_noext s in + (match search_ml_known s with + | Some mldir when not (List.mem s' !decl_list) -> + let fullname = file_name (String.uncapitalize s') mldir in + let depl = mL_dep_list s (fullname ^ ".ml") in + treat depl; + decl_list := s :: !decl_list + | _ -> ()); + treat ll | [] -> () in try let chan = open_in f in let buf = Lexing.from_channel chan in - begin try + begin try while true do let tok = coq_action buf in (match tok with - | Declare sl -> + | Declare sl -> decl_list := []; treat sl; decl_list := List.rev !decl_list; - if !option_D then + if !option_D then affiche_Declare f !decl_list else if !decl_list <> sl then warning_Declare f !decl_list @@ -377,200 +151,61 @@ let traite_Declare f = close_in chan with Sys_error _ -> () -let file_mem (f,_,d) = - let rec loop = function - | (f1,_,d1) :: l -> (f1 = f && d1 = d) || (loop l) - | _ -> false - in - loop - -let mL_dependencies () = - List.iter - (fun ((name,ext,dirname) as pairname) -> - let fullname = file_name ([name],dirname) in - let (dep,dep_opt) = traite_fichier_ML fullname ext in - printf "%s.cmo: %s%s" fullname fullname ext; - if file_mem pairname !mliAccu then printf " %s.cmi" fullname; - printf "%s\n" dep; - printf "%s.cmx: %s%s" fullname fullname ext; - if file_mem pairname !mliAccu then printf " %s.cmi" fullname; - printf "%s\n" dep_opt; - flush stdout) - (List.rev !mlAccu); - List.iter - (fun ((name,ext,dirname)) -> - let fullname = file_name ([name],dirname) in - let (dep,_) = traite_fichier_ML fullname ext in - printf "%s.cmi: %s%s" fullname fullname ext; - printf "%s\n" dep; - flush stdout) - (List.rev !mliAccu) - -let coq_dependencies () = - List.iter - (fun (name,_) -> - let glob = if !option_glob then " "^name^".glob" else "" in - printf "%s%s%s: %s.v" name !suffixe glob name; - traite_fichier_Coq true (name ^ ".v"); - printf "\n"; - if !option_i then begin - printf "%s%s%s: %s.v" name !suffixe_spec glob name; - traite_fichier_Coq false (name ^ ".v"); - printf "\n"; - end; - flush stdout) - (List.rev !vAccu) - let declare_dependencies () = List.iter (fun (name,_) -> - traite_Declare (name^".v"); + traite_Declare (name^".v"); flush stdout) (List.rev !vAccu) -let rec warning_mult suf l = - let tab = Hashtbl.create 151 in - Hashtbl.iter - (fun f d -> - begin try - let d' = Hashtbl.find tab f in - if (Filename.dirname (file_name ([f],d))) - <> (Filename.dirname (file_name ([f],d'))) then begin - eprintf "*** Warning : the file %s is defined twice!\n" (f ^ suf); - flush stderr - end - with Not_found -> () end; - Hashtbl.add tab f d) - l - let usage () = eprintf "[ usage: coqdep [-w] [-I dir] [-R dir coqdir] [-coqlib dir] [-c] [-i] [-D] <filename>+ ]\n"; flush stderr; exit 1 -let add_coqlib_known phys_dir log_dir f = - if Filename.check_suffix f ".vo" then - let basename = Filename.chop_suffix f ".vo" in - let name = log_dir@[basename] in - Hashtbl.add coqlibKnown [basename] (); - Hashtbl.add coqlibKnown name () - -let rec suffixes = function - | [] -> assert false - | [name] -> [[name]] - | dir::suffix as l -> l::suffixes suffix - -let add_known phys_dir log_dir f = - if (Filename.check_suffix f ".ml" || Filename.check_suffix f ".mli" || Filename.check_suffix f ".ml4") then - let basename = make_ml_module_name f in - Hashtbl.add mlKnown basename (Some phys_dir) - else if Filename.check_suffix f ".v" then - let basename = Filename.chop_suffix f ".v" in - let name = log_dir@[basename] in - let file = phys_dir//basename in - let paths = suffixes name in - List.iter - (fun n -> safe_hash_add clash_v vKnown (n,file)) paths - -(* Visits all the directories under [dir], including [dir], - or just [dir] if [recur=false] *) - -let rec add_directory recur add_file phys_dir log_dir = - let dirh = opendir phys_dir in - try - while true do - let f = readdir dirh in - (* we avoid . .. and all hidden files and subdirs (e.g. .svn, _darcs) *) - if f.[0] <> '.' && f.[0] <> '_' then - let phys_f = phys_dir//f in - match try (stat phys_f).st_kind with _ -> S_BLK with - | S_DIR when recur -> 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 - -let add_dir add_file phys_dir log_dir = - try add_directory false add_file phys_dir log_dir with Unix_error _ -> () - -let add_rec_dir add_file phys_dir log_dir = - handle_unix_error (add_directory true add_file phys_dir) log_dir - -let rec treat_file old_dirname old_name = - let name = Filename.basename old_name - and new_dirname = Filename.dirname old_name in - let dirname = - match (old_dirname,new_dirname) with - | (d, ".") -> d - | (None,d) -> Some d - | (Some d1,d2) -> Some (d1//d2) - in - let complete_name = file_name ([name],dirname) in - match try (stat complete_name).st_kind with _ -> S_BLK with - | S_DIR -> - (if name.[0] <> '.' then - let dir=opendir complete_name in - let newdirname = - match dirname with - | None -> name - | Some d -> d//name - in - try - while true do treat_file (Some newdirname) (readdir dir) done - with End_of_file -> closedir dir) - | S_REG -> - if Filename.check_suffix name ".ml" then - let basename = Filename.chop_suffix name ".ml" in - addQueue mlAccu (basename,".ml",dirname) - else if Filename.check_suffix name ".ml4" then - let basename = Filename.chop_suffix name ".ml4" in - addQueue mlAccu (basename,".ml4",dirname) - else if Filename.check_suffix name ".mli" then - let basename = Filename.chop_suffix name ".mli" in - addQueue mliAccu (basename,".mli",dirname) - else if Filename.check_suffix name ".v" then - let basename = Filename.chop_suffix name ".v" in - let name = file_name ([basename],dirname) in - addQueue vAccu (name, absolute_file_name basename dirname) - | _ -> () - let rec parse = function | "-c" :: ll -> option_c := true; parse ll | "-D" :: ll -> option_D := true; parse ll | "-w" :: ll -> option_w := true; parse ll - | "-i" :: ll -> option_i := true; parse ll | "-boot" :: ll -> Flags.boot := true; parse ll | "-sort" :: ll -> option_sort := true; parse ll - | "-glob" :: ll -> option_glob := true; parse ll + | ("-noglob" | "-no-glob") :: ll -> option_noglob := true; parse ll + | "-I" :: r :: "-as" :: ln :: ll -> add_dir add_known r [ln]; parse ll + | "-I" :: r :: "-as" :: [] -> usage () | "-I" :: r :: ll -> add_dir add_known r []; parse ll | "-I" :: [] -> usage () + | "-R" :: r :: "-as" :: ln :: ll -> add_rec_dir add_known r [ln]; parse ll + | "-R" :: r :: "-as" :: [] -> usage () | "-R" :: r :: ln :: ll -> add_rec_dir add_known r [ln]; parse ll | "-R" :: ([] | [_]) -> usage () | "-coqlib" :: (r :: ll) -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll | "-coqlib" :: [] -> usage () - | "-suffix" :: (s :: ll) -> suffixe := s ; suffixe_spec := s; parse ll + | "-suffix" :: (s :: ll) -> suffixe := s ; parse ll | "-suffix" :: [] -> usage () | "-slash" :: ll -> option_slash := true; parse ll + | ("-h"|"--help"|"-help") :: _ -> usage () | f :: ll -> treat_file None f; parse ll | [] -> () let coqdep () = if Array.length Sys.argv < 2 then usage (); parse (List.tl (Array.to_list Sys.argv)); + if not Coq_config.has_natdynlink then option_natdynlk := false; if !Flags.boot then begin add_rec_dir add_known "theories" ["Coq"]; - add_rec_dir add_known "contrib" ["Coq"] + add_rec_dir add_known "plugins" ["Coq"] end else begin let coqlib = Envars.coqlib () in - add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"]; - add_rec_dir add_coqlib_known (coqlib//"contrib") ["Coq"]; - add_dir add_coqlib_known (coqlib//"user-contrib") [] + add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"]; + add_rec_dir add_coqlib_known (coqlib//"plugins") ["Coq"]; + add_dir add_coqlib_known (coqlib//"user-contrib") [] end; - List.iter (fun (f,_,d) -> Hashtbl.add mliKnown f d) !mliAccu; - List.iter (fun (f,_,d) -> Hashtbl.add mlKnown f d) !mlAccu; - warning_mult ".mli" mliKnown; - warning_mult ".ml" mlKnown; + List.iter (fun (f,d) -> add_mli_known f d) !mliAccu; + List.iter (fun (f,d) -> add_mllib_known f d) !mllibAccu; + List.iter (fun (f,_,d) -> add_ml_known f d) !mlAccu; + warning_mult ".mli" iter_mli_known; + warning_mult ".ml" iter_ml_known; if !option_sort then begin sort (); exit 0 end; if !option_c && not !option_D then mL_dependencies (); if not !option_D then coq_dependencies (); |