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, 17 insertions, 36 deletions

diff --git a/Makefile.build b/Makefile.build
index 7dff7f2fc..0ab057a9d 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -17,9 +17,16 @@
 
 world: coq coqide documentation revision
 
-coq: coqlib coqbinaries tools printers
+coq: coqlib coqbinaries tools
 
-.PHONY: world coq
+# Note: 'world' do not build the bytecode binaries anymore.
+# For that, you can use the 'byte' rule. Native and byte compilations
+# shouldn't be done in a same make -j... run, otherwise both ocamlc and
+# ocamlopt might race for access to the same .cmi files.
+
+byte: coqbyte coqide-byte pluginsbyte printers
+
+.PHONY: world coq byte
 
 ###########################################################################
 # Includes
@@ -313,11 +320,11 @@ grammar/%.cmi: grammar/%.mli
 # Main targets (coqmktop, coqtop.opt, coqtop.byte)
 ###########################################################################
 
-.PHONY: coqbinaries
+.PHONY: coqbinaries coqbyte
 
-coqbinaries: $(COQMKTOP) $(COQTOPEXE) $(COQTOPBYTE) \
- $(CHICKEN) $(CHICKENBYTE) $(CSDPCERT) $(FAKEIDE)
+coqbinaries: $(COQMKTOP) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE)
 
+coqbyte: $(COQTOPBYTE) $(CHICKENBYTE)
 
 ifeq ($(BEST),opt)
 $(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs)
@@ -503,18 +510,13 @@ test-suite: world $(ALLSTDLIB).v
 
 # For plugin packs
 
-# Note: both ocamlc -pack and ocamlopt -pack will create the same .cmi, and there's
-# apparently no way to avoid that (no -intf-suffix hack as below).
-# We at least ensure that these two commands won't run at the same time, by a fake
-# dependency from the packed .cmx to the packed .cmo.
-
 %.cmo: %.mlpack
 	$(SHOW)'OCAMLC -pack -o $@'
 	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -pack -o $@ $(filter-out %.mlpack, $^)
 
-%.cmx: %.mlpack %.cmo
+%.cmx: %.mlpack
 	$(SHOW)'OCAMLOPT -pack -o $@'
-	$(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -pack -o $@ $(filter-out %.mlpack %.cmo, $^)
+	$(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -pack -o $@ $(filter-out %.mlpack, $^)
 
 COND_BYTEFLAGS= \
  $(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) $(BYTEFLAGS)
@@ -530,27 +532,6 @@ COND_OPTFLAGS= \
 	$(SHOW)'OCAMLC    $<'
 	$(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $<
 
-## NB: for the moment ocamlopt erases and recreates .cmi if there's no .mli around.
-## This can lead to nasty things with make -j. To avoid that:
-##  1) We make .cmx always depend on .cmi
-##  2) This .cmi will be created from the .mli, or trigger the compilation of the
-##    .cmo if there's no .mli (see rule below about MLWITHOUTMLI)
-##  3) We tell ocamlopt to use the .cmi as the interface source file. With this
-##     hack, everything goes as if there is a .mli, and the .cmi is preserved
-##     and the .cmx is checked with respect to this .cmi
-
-HACKMLI = $(if $(wildcard $<i),,-intf-suffix .cmi)
-
-define diff
- $(strip $(foreach f, $(1), $(if $(filter $(f),$(2)),,$f)))
-endef
-
-MLWITHOUTMLI := $(call diff, $(MLFILES), $(MLIFILES:.mli=.ml))
-
-$(MLWITHOUTMLI:.ml=.cmx): %.cmx: %.cmi  # for .ml with .mli this is already the case
-
-$(MLWITHOUTMLI:.ml=.cmi): %.cmi: %.cmo
-
 # NB: the *_FORPACK variables are generated in *.mlpack.d by ocamllibdep
 # The only exceptions are the sources of the csdpcert binary.
 # To avoid warnings, we set them manually here:
@@ -561,11 +542,11 @@ plugins/micromega/csdpcert_FORPACK:=
 
 plugins/%.cmx: plugins/%.ml
 	$(SHOW)'OCAMLOPT  $<'
-	$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -c $<
+	$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $($(@:.cmx=_FORPACK)) -c $<
 
 %.cmx: %.ml
 	$(SHOW)'OCAMLOPT  $<'
-	$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) -c $<
+	$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) -c $<
 
 %.cmxs: %.cmx
 	$(SHOW)'OCAMLOPT -shared -o $@'
@@ -650,7 +631,7 @@ endif
 
 %.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENVFILES)
 	$(SHOW)'COQDEP    $<'
-	$(HIDE)$(COQDEPBOOT) -boot $(DEPNATDYN) "$<" $(TOTARGET)
+	$(HIDE)$(COQDEPBOOT) -boot $(DYNDEP) "$<" $(TOTARGET)
 
 ###########################################################################