diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-01-05 17:01:13 +0100 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-05-23 10:48:28 +0200 |
commit | e94334670c7aa9c96e40d678fcc7a7a70cfd0099 (patch) | |
tree | 8a85328eb5fe6fe6a45fb48b2e9ceb490d1980f0 /tools | |
parent | cd6dd06789139ee0ff5c2b79a280476999fe2bf1 (diff) |
coqdep: set FOR_PACK variable for files that need to be packed
This enables one to have just one rule to compile .ml -> .cmx.
By using $(FOR_PACK) in such rule one passes to ocamlopt
-for-pack ModName only when necessary.
Before this coq_makefile had to generate 2 different rules, depending if
the module was mentioned in an .mlpack.
Diffstat (limited to 'tools')
-rw-r--r-- | tools/coqdep_common.ml | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 93b25e2ed..281644d23 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -293,15 +293,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 @@ -443,7 +443,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 +453,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 = String.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) |