From 60cd664eb37d017289d468d7e4f826c229cba7f6 Mon Sep 17 00:00:00 2001 From: letouzey Date: Sat, 14 Mar 2009 11:29:38 +0000 Subject: Coqdep: better handling of Declare ML Module (via .mllib) + many cleanups git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11976 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tools/coqdep.ml | 357 ++++++++++++++++++++++++++++--------------------- tools/coqdep_lexer.mll | 6 + 2 files changed, 212 insertions(+), 151 deletions(-) diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 019ee6b1a..a617bce49 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -36,18 +36,42 @@ let file_concat l = if l=[] then "" 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 *) +(** [get_extension f l] checks whether [f] has one of the extensions + listed in [l]. It returns [f] without its extension, alongside with + the extension. When no extension match, [(f,"")] is returned *) + +let rec get_extension f = function + | [] -> (f, "") + | s :: _ when Filename.check_suffix f s -> (Filename.chop_suffix f s, s) + | _ :: l -> get_extension f l + +(** [basename_noext] removes both the directory part and the extension + (if necessary) of a filename *) + +let basename_noext filename = + let fn = Filename.basename filename in + try Filename.chop_extension fn with _ -> fn + +(** ML Files specified on the command line. In the entries: + - the first string is the basename of the file, without extension nor + directory part + - the second string of [mlAccu] is the extension (either .ml or .ml4) + - the [dir] part is the directory, with None used as the current directory +*) + +let mlAccu = ref ([] : (string * string * dir) list) +and mliAccu = ref ([] : (string * dir) list) +and mllibAccu = ref ([] : (string * dir) list) + +(** Coq files specifies on the command line: + - first string is the full filename, with only its extension removed + - second string is the absolute version of the previous (via getcwd) +*) + +let vAccu = ref ([] : (string * string) list) + +(** Queue operations *) + let addQueue q v = q := v :: !q let safe_hash_add clq q (k,v) = @@ -61,16 +85,32 @@ let safe_hash_add clq q (k,v) = clq := add_clash !clq with Not_found -> Hashtbl.add q k v -(* Files found in the loadpaths *) +(** Files found in the loadpaths. + For the ML files, the string is the basename without extension. + To allow ML source filename to be potentially capitalized, + we perform a double search. +*) + +let mkknown () = + let h = (Hashtbl.create 19 : (string, dir) Hashtbl.t) in + let add x s = Hashtbl.add h x s + and iter f = Hashtbl.iter f h + and search x = + try Some (Hashtbl.find h (String.uncapitalize x)) + with Not_found -> + try Some (Hashtbl.find h (String.capitalize x)) + with Not_found -> None + in add, iter, search + +let add_ml_known, iter_ml_known, search_ml_known = mkknown () +let add_mli_known, iter_mli_known, search_mli_known = mkknown () +let add_mllib_known, _, search_mllib_known = mkknown () -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" @@ -82,6 +122,11 @@ let warning_notfound f s = eprintf "%s.v is required and has not been found !\n" s; flush stderr +let warning_declare f s = + eprintf "*** Warning : in file %s, Declared ML Module " f; + eprintf "%s has not been found !\n" s; + flush stderr + let warning_clash file dir = match List.assoc dir !clash_v with (f1::f2::fl) -> @@ -110,11 +155,25 @@ let absolute_dir 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 file_name s = function + | None -> s + | Some "." -> s + | Some d -> d // s + +let depend_ML str = + match search_mli_known str, search_ml_known str with + | Some mlidir, Some mldir -> + let mlifile = file_name str mlidir + and mlfile = file_name str mldir in + (" "^mlifile^".cmi"," "^mlfile^".cmx") + | None, Some mldir -> + let mlfile = file_name str mldir in + (" "^mlfile^".cmo"," "^mlfile^".cmx") + | Some mlidir, None -> + let mlifile = file_name str mlidir in + (" "^mlifile^".cmi"," "^mlifile^".cmi") + | None, None -> "", "" let traite_fichier_ML md ext = try @@ -130,28 +189,9 @@ let traite_fichier_ML md ext = () 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 byte,opt = depend_ML str in + a_faire := !a_faire ^ byte; + a_faire_opt := !a_faire_opt ^ opt end done with Fin_fichier -> () @@ -160,6 +200,22 @@ let traite_fichier_ML md ext = (!a_faire, !a_faire_opt) with Sys_error _ -> ("","") +let traite_fichier_mllib md ext = + try + let chan = open_in (md ^ ext) in + let list = mllib_list (Lexing.from_channel chan) in + let a_faire = ref "" in + let a_faire_opt = ref "" in + List.iter + (fun str -> match search_ml_known str with + | Some mldir -> + let file = file_name str mldir in + a_faire := !a_faire^" "^file^".cmo"; + a_faire_opt := !a_faire_opt^" "^file^".cmx" + | None -> ()) list; + (!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 @@ -185,7 +241,7 @@ let sort () = | Require sl -> List.iter (fun s -> - try loop (Hashtbl.find vKnown s) + try loop (Hashtbl.find vKnown s) with Not_found -> ()) sl | RequireString s -> loop s @@ -230,33 +286,26 @@ let traite_fichier_Coq verbose f = 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 -> - (** The .cmxs we want to load dynamically may come - from a .cmxa, that has no corresponding .ml file. - Idem with bytecode .cma. What dependency should - we produce then ? For the moment, we suppose the - .cmxs and .cma are at the same location. *) - let mldir = Some (Filename.dirname f) in - let filename = file_name ([String.uncapitalize s],mldir) in - if Coq_config.has_natdynlink then - printf " %s.cma %s.cmxs" filename filename - else - printf " %s.cma" filename - end) - sl + | Declare sl -> + let declare suff dir s = + let base = file_name s dir in + let opt = + if Coq_config.has_natdynlink then " "^base^".cmxs" else "" + in + printf " %s%s%s" base suff opt + in + let decl str = + let s = basename_noext str in + if not (List.mem s !deja_vu_ml) then begin + addQueue deja_vu_ml s; + match search_mllib_known s with + | Some mldir -> declare ".cma" mldir s + | None -> + match search_ml_known s with + | Some mldir -> declare ".cmo" mldir s + | None -> warning_declare f str + end + in List.iter decl sl | Load str -> let str = Filename.basename str in if not (List.mem [str] !deja_vu_v) then begin @@ -318,16 +367,16 @@ let warning_Declare f dcl = 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 @@ -355,35 +404,41 @@ let file_mem (f,_,d) = let rec loop = function | (f1,_,d1) :: l -> (f1 = f && d1 = d) || (loop l) | _ -> false - in + in loop let mL_dependencies () = List.iter - (fun ((name,ext,dirname) as pairname) -> - let fullname = file_name ([name],dirname) in + (fun (name,ext,dirname) -> + 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; + let intf = + if List.mem (name,dirname) !mliAccu then " "^fullname^".cmi" else "" + in + printf "%s.cmo: %s%s%s%s\n" fullname fullname ext intf dep; + printf "%s.cmx: %s%s%s%s\n" fullname fullname ext intf 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; + (fun (name,dirname) -> + let fullname = file_name name dirname in + let (dep,_) = traite_fichier_ML fullname ".mli" in + printf "%s.cmi: %s.mli%s\n" fullname fullname dep; + flush stdout) + (List.rev !mliAccu); + List.iter + (fun (name,dirname) -> + let fullname = file_name name dirname in + let (dep,dep_opt) = traite_fichier_mllib fullname ".mllib" in + printf "%s.cma:%s\n" fullname dep; + printf "%s.cmxa %s.cmxs:%s\n" fullname fullname dep_opt; flush stdout) - (List.rev !mliAccu) + (List.rev !mllibAccu) let coq_dependencies () = List.iter (fun (name,_) -> - let glob = if !option_noglob then "" else " "^name^".glob" in + let glob = if !option_noglob then "" else " "^name^".glob" in printf "%s%s%s: %s.v" name !suffixe glob name; traite_fichier_Coq true (name ^ ".v"); printf "\n"; @@ -393,24 +448,24 @@ let coq_dependencies () = 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 rec warning_mult suf iter = 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 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 + with Not_found -> () end; + Hashtbl.add tab f d + in + iter check let usage () = eprintf @@ -418,24 +473,27 @@ let usage () = 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 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 = [name;[basename]] in - List.iter - (fun n -> safe_hash_add clash_v vKnown (n,file)) paths +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 add_known phys_dir log_dir f = + match get_extension f [".v";".ml";".mli";".ml4";".mllib"] with + | (basename,".v") -> + let name = log_dir@[basename] in + let file = phys_dir//basename in + let paths = [name;[basename]] in + List.iter + (fun n -> safe_hash_add clash_v vKnown (n,file)) paths + | (basename,(".ml"|".ml4")) -> add_ml_known basename (Some phys_dir) + | (basename,".mli") -> add_mli_known basename (Some phys_dir) + | (basename,".mllib") -> add_mllib_known basename (Some phys_dir) + | _ -> () (* Visits all the directories under [dir], including [dir], or just [dir] if [recur=false] *) @@ -470,7 +528,7 @@ let rec treat_file old_dirname old_name = | (None,d) -> Some d | (Some d1,d2) -> Some (d1//d2) in - let complete_name = file_name ([name],dirname) 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 @@ -483,20 +541,16 @@ let rec treat_file old_dirname old_name = 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) + | S_REG -> + (match get_extension name [".v";".ml";".mli";".ml4";".mllib"] with + | (base,".v") -> + let name = file_name base dirname + and absname = absolute_file_name base dirname in + addQueue vAccu (name, absname) + | (base,(".ml"|".ml4" as ext)) -> addQueue mlAccu (base,ext,dirname) + | (base,".mli") -> addQueue mliAccu (base,dirname) + | (base,".mllib") -> addQueue mllibAccu (base,dirname) + | _ -> ()) | _ -> () let rec parse = function @@ -526,14 +580,15 @@ let coqdep () = add_rec_dir add_known "contrib" ["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//"contrib") ["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 (); diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll index 67dea5a3c..6d6a804da 100755 --- a/tools/coqdep_lexer.mll +++ b/tools/coqdep_lexer.mll @@ -225,5 +225,11 @@ and caml_opened_file = parse | eof {raise Fin_fichier } | _ { caml_action lexbuf } +and mllib_list = parse + | coq_ident { let s = String.uncapitalize (Lexing.lexeme lexbuf) + in s :: mllib_list lexbuf } + | space+ { mllib_list lexbuf } + | eof { [] } + -- cgit v1.2.3