Makefile: no bytecode compilation in make world, see make byte instead

 On a machine for which ocamlopt is available, the make world will now
 perform bytecode compilation only in grammar/ (up to the syntax
 extension grammar.cma), and then exclusively use ocamlopt.
 In particular, make world do not build bin/coqtop.byte.
 A separate rule 'make byte' does it, as well as bytecode plugins and
 things like dev/printers.cma.

 'make install' deals only with the part built by 'make', while a new
 rule 'make install-byte' installs the part built by 'make byte'.

 IMPORTANT: PLEASE AVOID doing things like 'make -j world byte' or any
 parallel mix of native and byte rules. These are known to crash sometimes,
 see below. Instead, do rather 'make -j && make -j byte'.

 Indeed, apart from marginal compilation speed-up for users not interested
 in byte versions, the main reason for this commit is to discourage any
 simultaneous use of OCaml native and byte compilers. Indeed, ocamlopt and
 ocamlc will both happily destroy and recreate .cmi for .ml files with no .mli,
 and in case of parallel build this may happen at the very moment another
 ocaml(c|opt) is accessing this .cmi. Until now, this issue has been
 handled via nasty hacks (see the former MLWITHOUTMLI and HACKMLI vars in
 Makefile.build). But these hacks weren't obvious to extend to ocamlopt
 -pack vs. ocamlopt -pack.

 coqdep_boot takes a "-dyndep" option to control precisely how a Declare ML
 Module influences the .v.d dependency file. Possible values are:
 -dyndep opt : regular situation now, depends only on .cmxs
 -dyndep byte : no ocamlopt, or compilation forced to bytecode, depends on .cm(o|a)
 -dyndep both : earlier behavior, dependency over both .cm(o|a) and .cmxs
 -dyndep none : interesting for coqtop with statically linked plugins
 -dyndep var : place Makefile variables $(DYNLIB) and $(DYNOBJ) in .v.d
   instead of extensions .cm*, so that the choice is made in the rest of the
   makefile (see a future commit about coq_makefile)

 NB: two extra mli added to avoid building unecessary .cmo during 'make world',
 without having to use the ocamldep -native option.

 NB: we should state somewhere that coqmktop -top won't work unless
  'make byte' was done first

1 files changed, 18 insertions, 6 deletions

diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 044399544..cba9c3eb0 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -320,19 +320,25 @@ let treat_coq_file chan =
         List.fold_left (fun accu v -> mark_v_done from accu v) acc 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
-          (escape base, suff ^ opt)
+          let base = escape (file_name s dir) in
+          match !option_dynlink with
+          | No -> []
+          | Byte -> [base,suff]
+          | Opt -> [base,".cmxs"]
+          | Both -> [base,suff; base,".cmxs"]
+          | Variable ->
+             if suff=".cmo" then [base,"$(DYNOBJ)"]
+             else [base,"$(DYNLIB)"]
         in
         let decl acc str =
           let s = basename_noext str in
           if not (StrSet.mem s !deja_vu_ml) then
             let () = deja_vu_ml := StrSet.add s !deja_vu_ml in
             match search_mllib_known s with
-            | Some mldir -> (declare ".cma" mldir s) :: acc
+            | Some mldir -> (declare ".cma" mldir s) @ acc
             | None ->
               match search_ml_known s with
-              | Some mldir -> (declare ".cmo" mldir s) :: acc
+              | Some mldir -> (declare ".cmo" mldir s) @ acc
               | None -> acc
           else acc
         in
@@ -449,6 +455,7 @@ let usage () =
   eprintf "  -coqlib dir : set the coq standard library directory\n";
   eprintf "  -suffix s : \n";
   eprintf "  -slash : deprecated, no effect\n";
+  eprintf "  -dyndep (opt|byte|both|no|var) : set how dependencies over ML modules are printed";
   exit 1
 
 let split_period = Str.split (Str.regexp (Str.quote "."))
@@ -476,17 +483,22 @@ let rec parse = function
   | "-slash" :: ll ->
     Printf.eprintf "warning: option -slash has no effect and is deprecated.\n";
     parse ll
+  | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll
+  | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll
+  | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll
+  | "-dyndep" :: "both" :: ll -> option_dynlink := Both; parse ll
+  | "-dyndep" :: "var" :: ll -> option_dynlink := Variable; parse ll
   | ("-h"|"--help"|"-help") :: _ -> usage ()
   | f :: ll -> treat_file None f; parse ll
   | [] -> ()
 
 let coqdep () =
   if Array.length Sys.argv < 2 then usage ();
+  if not Coq_config.has_natdynlink then option_dynlink := No;
   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_import add_known "theories" ["Coq"];