diff options
Diffstat (limited to 'tools/coqdep_common.ml')
| -rw-r--r-- | tools/coqdep_common.ml | 70 |
1 files changed, 45 insertions, 25 deletions
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 0064aebd..db69a3b7 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Printf @@ -15,7 +17,7 @@ open Minisys behavior is the one of [coqdep -boot]. Its only dependencies are [Coqdep_lexer], [Unix] and [Minisys], and it should stay so. If it need someday some additional information, pass it via - options (see for instance [option_natdynlk] below). + options (see for instance [option_dynlink] below). *) module StrSet = Set.Make(String) @@ -26,9 +28,11 @@ module StrListMap = Map.Make(StrList) let stderr = Pervasives.stderr let stdout = Pervasives.stdout +type dynlink = Opt | Byte | Both | No | Variable + let option_c = ref false let option_noglob = ref false -let option_natdynlk = ref true +let option_dynlink = ref Both let option_boot = ref false let option_mldep = ref None @@ -36,6 +40,10 @@ let norec_dirs = ref StrSet.empty let suffixe = ref ".vo" +[@@@ocaml.warning "-3"] (* String.capitalize_ascii since 4.03.0 GPR#124 *) +let capitalize = String.capitalize +[@@@ocaml.warning "+3"] + type dir = string option (** [get_extension f l] checks whether [f] has one of the extensions @@ -94,8 +102,18 @@ let safe_hash_add cmp clq q (k, (v, b)) = For the ML files, the string is the basename without extension. *) +let same_path_opt s s' = + let nf s = (* ./foo/a.ml and foo/a.ml are the same file *) + if Filename.is_implicit s + then "." // s + else s + in + let s = match s with None -> "." | Some s -> nf s in + let s' = match s' with None -> "." | Some s' -> nf s' in + s = s' + let warning_ml_clash x s suff s' suff' = - if suff = suff' then + if suff = suff' && not (same_path_opt s s') then eprintf "*** Warning: %s%s already found in %s (discarding %s%s)\n" x suff (match s with None -> "." | Some d -> d) @@ -219,7 +237,6 @@ let register_dir_logpath,find_dir_logpath = let file_name s = function | None -> s - | Some "." -> s | Some d -> d // s let depend_ML str = @@ -293,15 +310,15 @@ let traite_fichier_modules md ext = (fun a_faire str -> match search_mlpack_known str with | Some mldir -> let file = file_name str mldir in - a_faire^" "^file + a_faire @ [file] | None -> match search_ml_known str with | Some mldir -> let file = file_name str mldir in - a_faire^" "^file - | None -> a_faire) "" list + a_faire @ [file] + | None -> a_faire) [] list with - | Sys_error _ -> "" + | Sys_error _ -> [] | Syntax_error (i,j) -> error_cannot_parse (md^ext) (i,j) (* Makefile's escaping rules are awful: $ is escaped by doubling and @@ -380,10 +397,16 @@ let rec traite_fichier_Coq suffixe verbose f = end) strl | Declare sl -> let declare suff dir s = - let base = file_name s dir in - let opt = if !option_natdynlk then " "^base^".cmxs" else "" in - printf " %s%s%s" (escape base) suff opt - in + let base = escape (file_name s dir) in + match !option_dynlink with + | No -> () + | Byte -> printf " %s%s" base suff + | Opt -> printf " %s.cmxs" base + | Both -> printf " %s%s %s.cmxs" base suff base + | Variable -> + printf " %s%s" base + (if suff=".cmo" then "$(DYNOBJ)" else "$(DYNLIB)") + in let decl str = let s = basename_noext str in if not (StrSet.mem s !deja_vu_ml) then begin @@ -443,7 +466,7 @@ let mL_dependencies () = let fullname = file_name name dirname in let dep = traite_fichier_modules fullname ".mllib" in let efullname = escape fullname in - printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname dep; + printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname (String.concat " " dep); printf "%s.cma:$(addsuffix .cmo,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname; printf "%s.cmxa:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname; flush stdout) @@ -453,9 +476,13 @@ let mL_dependencies () = let fullname = file_name name dirname in let dep = traite_fichier_modules fullname ".mlpack" in let efullname = escape fullname in - printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname dep; + printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname (String.concat " " dep); printf "%s.cmo:$(addsuffix .cmo,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname; printf "%s.cmx:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname; + let efullname_capital = capitalize (Filename.basename efullname) in + List.iter (fun dep -> + printf "%s.cmx : FOR_PACK=-for-pack %s\n" dep efullname_capital) + dep; flush stdout) (List.rev !mlpackAccu) @@ -544,13 +571,6 @@ let add_rec_dir_no_import add_file phys_dir log_dir = let add_rec_dir_import add_file phys_dir log_dir = add_directory true (add_file true) phys_dir log_dir -(** -R semantic but only on immediate capitalized subdirs *) - -let add_rec_uppercase_subdirs add_file phys_dir log_dir = - process_subdirectories (fun phys_dir f -> - add_directory true (add_file true) phys_dir (log_dir@[String.capitalize f])) - phys_dir - (** -I semantic: do not go in subdirs. *) let add_caml_dir phys_dir = add_directory false add_caml_known phys_dir [] |