Merge PR #9477: Makefiles: Fixes for byte compilation

Reviewed-by: gares

6 files changed, 37 insertions, 23 deletions

diff --git a/Makefile.build b/Makefile.build
index 26e2819990..ca988aaac2 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -239,6 +239,10 @@ OPT:=
 BESTOBJ:=.cmo
 BESTLIB:=.cma
 BESTDYN:=.cma
+
+# needed while booting if non -local
+CAML_LD_LIBRARY_PATH := $(PWD)/kernel/byterun:$(CAML_LD_LIBRARY_PATH)
+export CAML_LD_LIBRARY_PATH
 endif
 
 define bestobj
@@ -350,12 +354,12 @@ kernel/uint63.ml: kernel/write_uint63.ml kernel/uint63_x86.ml kernel/uint63_amd6
 
 .PHONY: coqbinaries coqbyte
 
-coqbinaries: $(TOPBINOPT) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE)
-coqbyte: $(TOPBYTE) $(CHICKENBYTE)
+coqbinaries: $(TOPBIN) $(COQC) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE)
+coqbyte: $(TOPBYTE) $(COQCBYTE) $(CHICKENBYTE)
 
 # Special rule for coqtop, we imitate `ocamlopt` can delete the target
 # to avoid #7666
-$(COQTOPEXE): $(TOPBINOPT:.opt=.$(BEST))
+$(COQTOPEXE): $(TOPBIN)
 	rm -f $@ && cp $< $@
 
 $(COQC): $(COQCOPT:.opt=.$(BEST))
@@ -380,12 +384,12 @@ COQTOP_BYTE=topbin/coqtop_byte_bin.ml
 
 # Special rule for coqtop.byte
 # VMBYTEFLAGS will either contain -custom of the right -dllpath for the VM
-$(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(COQTOP_BYTE)
+$(COQTOPBYTE): $(COQTOP_BYTE) $(LINKCMO) $(LIBCOQRUN)
 	$(SHOW)'COQMKTOP -o $@'
 	$(HIDE)$(OCAMLC) -linkall -linkpkg -I lib -I vernac -I toplevel \
 	                 -I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \
 			 $(SYSMOD) -package compiler-libs.toplevel \
-			 $(LINKCMO) $(BYTEFLAGS) $(COQTOP_BYTE) -o $@
+			 $(LINKCMO) $(BYTEFLAGS) $< -o $@
 
 ###########################################################################
 # other tools
@@ -501,7 +505,7 @@ $(COQWORKMGRBYTE): $(COQWORKMGRCMO)
 
 FAKEIDECMO:=config/config.cma clib/clib.cma lib/lib.cma ide/protocol/ideprotocol.cma ide/document.cmo ide/fake_ide.cmo
 
-$(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOP)
+$(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOPEXE)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, -I ide -I ide/protocol -package str -package dynlink)
 
diff --git a/Makefile.common b/Makefile.common
index 8292158ef8..bd0e19cd00 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -75,10 +75,12 @@ endif
 # for Declare ML Module files.
 
 ifeq ($(BEST),opt)
+TOPBIN:=$(TOPBINOPT)
 COQTOPBEST:=$(COQTOPEXE)
 DYNOBJ:=.cmxs
 DYNLIB:=.cmxs
 else
+TOPBIN:=$(TOPBYTE)
 COQTOPBEST:=$(COQTOPBYTE)
 DYNOBJ:=.cmo
 DYNLIB:=.cma
diff --git a/Makefile.install b/Makefile.install
index b6e2ec2aeb..5b5e548f9c 100644
--- a/Makefile.install
+++ b/Makefile.install
@@ -68,7 +68,7 @@ endif
 
 install-binaries: install-tools
 	$(MKDIR) $(FULLBINDIR)
-	$(INSTALLBIN) $(COQC) $(CHICKEN) $(COQTOPEXE) $(TOPBINOPT) $(FULLBINDIR)
+	$(INSTALLBIN) $(COQC) $(CHICKEN) $(COQTOPEXE) $(TOPBIN) $(FULLBINDIR)
 
 install-byte: install-coqide-byte
 	$(MKDIR) $(FULLBINDIR)
@@ -100,18 +100,15 @@ INSTALLCMX = $(sort $(filter-out checker/% ide/% tools/% dev/% \
 	configure.cmx toplevel/coqtop_byte_bin.cmx plugins/extraction/big.cmx, \
 	$(filter %.cmx, $(GRAMMLFILES:.ml=.cmx)) $(MLFILES:.ml=.cmx)))
 
-foo:
-	@echo $(INSTALLCMX)
-
 install-devfiles:
 	$(MKDIR) $(FULLBINDIR)
 	$(MKDIR) $(FULLCOQLIB)
 	$(INSTALLSH)  $(FULLCOQLIB) $(INSTALLCMI)           # Regular CMI files
+	$(INSTALLSH)  $(FULLCOQLIB) $(TOOLS_HELPERS)
+ifeq ($(BEST),opt)
 	$(INSTALLSH)  $(FULLCOQLIB) $(INSTALLCMX)           # To avoid warning 58 "-opaque"
 	$(INSTALLSH)  $(FULLCOQLIB) $(PLUGINSCMO:.cmo=.cmx) # For static linking of plugins
 	$(INSTALLSH)  $(FULLCOQLIB) $(PLUGINSCMO:.cmo=.o)   # For static linking of plugins
-	$(INSTALLSH)  $(FULLCOQLIB) $(TOOLS_HELPERS)
-ifeq ($(BEST),opt)
 	$(INSTALLSH)  $(FULLCOQLIB) $(LINKCMX) $(CORECMA:.cma=.a) $(STATICPLUGINS:.cma=.a)
 endif
 
diff --git a/Makefile.vofiles b/Makefile.vofiles
index d5217ef4b7..a71d68e565 100644
--- a/Makefile.vofiles
+++ b/Makefile.vofiles
@@ -42,7 +42,10 @@ GLOBFILES:=$(ALLVO:.$(VO)=.glob)
 endif
 
 ifdef NATIVECOMPUTE
-NATIVEFILES := $(call vo_to_cm,$(ALLVO)) $(call vo_to_obj,$(ALLVO))
+NATIVEFILES := $(call vo_to_cm,$(ALLVO))
+ifeq ($(BEST),opt)
+NATIVEFILES += $(call vo_to_obj,$(ALLVO))
+endif
 else
 NATIVEFILES :=
 endif
@@ -50,5 +53,5 @@ LIBFILES:=$(ALLVO:.$(VO)=.vo) $(NATIVEFILES) $(VFILES) $(GLOBFILES)
 
 # For emacs:
 # Local Variables:
-# mode: makefile
+# mode: makefile-gmake
 # End:
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 68acb6f04d..03bfc5ffac 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -260,6 +260,7 @@ ifeq ($(LOCAL),true)
 endif
 
 OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS)
+OCAMLC := $(OCAMLFIND) ocamlc $(CAMLFLAGS)
 
 # ML files from unit-test framework, not containing tests
 UNIT_SRCFILES:=$(shell find ./unit-tests/src -name *.ml)
@@ -267,24 +268,31 @@ UNIT_ALLMLFILES:=$(shell find ./unit-tests -name *.ml)
 UNIT_MLFILES:=$(filter-out $(UNIT_SRCFILES),$(UNIT_ALLMLFILES))
 UNIT_LOGFILES:=$(patsubst %.ml,%.ml.log,$(UNIT_MLFILES))
 
-UNIT_CMXS=utest.cmx
+ifneq ($(BEST),opt)
+UNIT_LINK:=utest.cmo
+OCAMLBEST:=$(OCAMLC)
+else
+UNIT_LINK:=utest.cmx
+OCAMLBEST:=$(OCAMLOPT)
+endif
 
 unit-tests/src/utest.cmx: unit-tests/src/utest.ml unit-tests/src/utest.cmi
 	$(SHOW) 'OCAMLOPT  $<'
 	$(HIDE)$(OCAMLOPT) -c -I unit-tests/src -package oUnit $<
+unit-tests/src/utest.cmo: unit-tests/src/utest.ml unit-tests/src/utest.cmi
+	$(SHOW) 'OCAMLC  $<'
+	$(HIDE)$(OCAMLC) -c -I unit-tests/src -package oUnit $<
 unit-tests/src/utest.cmi: unit-tests/src/utest.mli
-	$(SHOW) 'OCAMLOPT  $<'
-	$(HIDE)$(OCAMLOPT) -package oUnit $<
-
-$(UNIT_LOGFILES): unit-tests/src/utest.cmx
+	$(SHOW) 'OCAMLC  $<'
+	$(HIDE)$(OCAMLC) -package oUnit -c $<
 
 unit-tests: $(UNIT_LOGFILES)
 
 # Build executable, run it to generate log file
-unit-tests/%.ml.log: unit-tests/%.ml
+unit-tests/%.ml.log: unit-tests/%.ml unit-tests/src/$(UNIT_LINK)
 	$(SHOW) 'TEST      $<'
-	$(HIDE)$(OCAMLOPT) -linkall -linkpkg -package coq.toplevel,oUnit \
-	     -I unit-tests/src $(UNIT_CMXS) $< -o $<.test;
+	$(HIDE)$(OCAMLBEST) -linkall -linkpkg -package coq.toplevel,oUnit \
+	     -I unit-tests/src $(UNIT_LINK) $< -o $<.test;
 	$(HIDE)./$<.test
 
 #######################################################################
diff --git a/test-suite/misc/poly-capture-global-univs.sh b/test-suite/misc/poly-capture-global-univs.sh
index e066ac039b..39d20fd524 100755
--- a/test-suite/misc/poly-capture-global-univs.sh
+++ b/test-suite/misc/poly-capture-global-univs.sh
@@ -11,7 +11,7 @@ coq_makefile -f _CoqProject -o Makefile
 
 make clean
 
-make src/evil_plugin.cmxs
+make src/evil_plugin.cma
 
 if make; then
     >&2 echo 'Should have failed!'