coq_makefile : do not build bytecode versions of plugins by default

 make install does not install these *.cm(o|a) files either.
 You could always do manually :
 - make bytefiles : to build the bytecode *.cm(o|a) files
 - make install-byte : to install these files
 - make byte : to compile the whole development with the bytecode version
   of Coq (this builds the *.cm(o|a) files, but also the .vo via coqc -byte).

 Technically, the behavior of make is controlled by the OPT variable,
 which could be -byte or -opt. For instance, 'make byte' corresponds to a
 'make OPT:=-byte'

 Note that coqdep is used with the new option "-dyndep var" : when seeing
 a Declare ML Module "foo", "coqdep -dyndep var" does not decide whether to
 depend on foo.cma or foo.cmxs, but rather use some Makefile variables such
 as foo$(DYNLIB), whose content is later set according to $(OPT)

1 files changed, 33 insertions, 4 deletions

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index fb064c495..8aff25738 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -116,6 +116,17 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
 
 OPT?=
 
+# The DYNOBJ and DYNLIB variables are used by "coqdep -dyndep var" in .v.d
+ifeq '$(OPT)' '-byte'
+USEBYTE:=true
+DYNOBJ:=.cmo
+DYNLIB:=.cma
+else
+USEBYTE:=
+DYNOBJ:=.cmxs
+DYNLIB:=.cmxs
+endif
+
 COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS)
 COQCHKFLAGS?=-silent -o $(COQLIBS) 
 COQDOCFLAGS?=-interpolate -utf8 $(COQLIBS_NOML)
@@ -214,7 +225,6 @@ CMOFILESTOINSTALL = $(filter-out $(addsuffix .cmo,$(PACKEDFILES)),$(CMOFILES))
 OBJFILES = $(call vo_to_obj,$(VOFILES))
 ALLNATIVEFILES = \
 	$(OBJFILES:.o=.cmi) \
-	$(OBJFILES:.o=.cmo) \
 	$(OBJFILES:.o=.cmx) \
 	$(OBJFILES:.o=.cmxs)
 # trick: wildcard filters out non-existing files
@@ -224,8 +234,9 @@ FILESTOINSTALL = \
 	$(VFILES) \
 	$(GLOBFILES) \
 	$(NATIVEFILESTOINSTALL) \
+	$(CMIFILESTOINSTALL)
+BYTEFILESTOINSTALL = \
 	$(CMOFILESTOINSTALL) \
-	$(CMIFILESTOINSTALL) \
 	$(CMAFILES)
 ifeq '$(HASNATDYNLINK)' 'true'
 DO_NATDYNLINK = yes
@@ -257,9 +268,15 @@ post-all::
 	@# Extension point
 .PHONY: post-all
 
-real-all: $(VOFILES) $(CMOFILES) $(CMAFILES) $(if $(DO_NATDYNLINK),$(CMXSFILES))
+real-all: $(VOFILES) $(if $(USEBYTE),bytefiles,optfiles)
 .PHONY: real-all
 
+bytefiles: $(CMOFILES) $(CMAFILES)
+.PHONY: bytefiles
+
+optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES))
+.PHONY: optfiles
+
 # FIXME, see Ralph's bugreport
 quick: $(VOFILES:.vo=.vio)
 .PHONY: quick
@@ -351,6 +368,18 @@ install-extra::
 	@# Extension point
 .PHONY: install install-extra
 
+install-byte:
+	$(HIDE)for f in $(BYTEFILESTOINSTALL); do\
+	 df="`$(COQMF_MAKEFILE) -destination-of "$$f" $(COQLIBS)`";\
+	 if [ -z "$$df" ]; then\
+	   echo SKIP "$$f" since it has no logical path;\
+	 else\
+	   install -d "$(DESTDIR)$(COQLIBINSTALL)/$$df"; \
+	   install -m 0644 "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df"; \
+	   echo INSTALL "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df";\
+	 fi;\
+	done
+
 install-doc:: html mlihtml
 	@# Extension point
 	$(HIDE)install -d "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html"
@@ -563,7 +592,7 @@ $(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack
 
 $(addsuffix .d,$(VFILES)): %.v.d: %.v
 	$(SHOW)'COQDEP $<'
-	$(HIDE)$(COQDEP) $(COQLIBS) -c "$<" $(redir_if_ok)
+	$(HIDE)$(COQDEP) $(COQLIBS) -dyndep var -c "$<" $(redir_if_ok)
 
 # Misc ########################################################################