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 next commit about coq_makedile)

 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, 49 insertions, 0 deletions

diff --git a/tools/coqdoc/cdglobals.mli b/tools/coqdoc/cdglobals.mli
new file mode 100644
index 000000000..2c9b3fb8e
--- /dev/null
+++ b/tools/coqdoc/cdglobals.mli
@@ -0,0 +1,49 @@
+type target_language = LaTeX | HTML | TeXmacs | Raw
+val target_language : target_language ref
+type output_t = StdOut | MultFiles | File of string
+val output_dir : string ref
+val out_to : output_t ref
+val out_channel : out_channel ref
+val ( / ) : string -> string -> string
+val coqdoc_out : string -> string
+val open_out_file : string -> unit
+val close_out_file : unit -> unit
+type glob_source_t = NoGlob | DotGlob | GlobFile of string
+val glob_source : glob_source_t ref
+val normalize_path : string -> string
+val normalize_filename : string -> string * string
+val guess_coqlib : unit -> string
+val header_trailer : bool ref
+val header_file : string ref
+val header_file_spec : bool ref
+val footer_file : string ref
+val footer_file_spec : bool ref
+val quiet : bool ref
+val light : bool ref
+val gallina : bool ref
+val short : bool ref
+val index : bool ref
+val multi_index : bool ref
+val index_name : string ref
+val toc : bool ref
+val page_title : string ref
+val title : string ref
+val externals : bool ref
+val coqlib : string ref
+val coqlib_path : string ref
+val raw_comments : bool ref
+val parse_comments : bool ref
+val plain_comments : bool ref
+val toc_depth : int option ref
+val lib_name : string ref
+val lib_subtitles : bool ref
+val interpolate : bool ref
+val inline_notmono : bool ref
+val charset : string ref
+val inputenc : string ref
+val latin1 : bool ref
+val utf8 : bool ref
+val set_latin1 : unit -> unit
+val set_utf8 : unit -> unit
+type coq_module = string
+type file = Vernac_file of string * coq_module | Latex_file of string