From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Subject: Makefiles: Fixes for byte compilation
Bug: https://github.com/coq/coq/issues/9464
Origin: other, https://github.com/SkySkimmer/coq/commit/f29aa6720eba884533972530b4283bf19d8410aa
Reviewed-by: Benjamin Barenblat <bbaren@debian.org>

- default targets don't depend on ocamlopt when it's unavailable
- coqc.byte is built by byte target and coqc by coqbinaries target
- unit tests use best ocaml
- poly-capture-global-univs tests ml compilation with ocamlc
- don't try to install .cmx and native-compute .o files

Benjamin Barenblat modified this patch to apply cleanly on top of 8.9.0.
--- a/Makefile.build
+++ b/Makefile.build
@@ -237,6 +237,10 @@
 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
@@ -408,12 +412,12 @@
 
 .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 $< $@
 
 bin/%.opt$(EXE): topbin/%_bin.ml $(LINKCMX) $(LIBCOQRUN)
@@ -435,12 +439,12 @@
 
 # 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 camlp5.gramlib,compiler-libs.toplevel \
-			 $(LINKCMO) $(BYTEFLAGS) $(COQTOP_BYTE) -o $@
+			 $(LINKCMO) $(BYTEFLAGS) $< -o $@
 
 # For coqc
 COQCCMO:=clib/clib.cma lib/lib.cma toplevel/usage.cmo tools/coqc.cmo
@@ -567,7 +571,7 @@
 
 FAKEIDECMO:=clib/clib.cma lib/lib.cma ide/protocol/ideprotocol.cma ide/document.cmo tools/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)
 
--- a/Makefile.common
+++ b/Makefile.common
@@ -74,10 +74,12 @@
 # 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
--- a/Makefile.install
+++ b/Makefile.install
@@ -68,7 +68,7 @@
 
 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)
@@ -104,11 +104,11 @@
 	$(MKDIR) $(FULLCOQLIB)
 	$(INSTALLSH)  $(FULLCOQLIB) $(GRAMMARCMA)
 	$(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
 
--- a/test-suite/misc/poly-capture-global-univs.sh
+++ b/test-suite/misc/poly-capture-global-univs.sh
@@ -11,7 +11,7 @@
 
 make clean
 
-make src/evil_plugin.cmxs
+make src/evil_plugin.cma
 
 if make; then
     >&2 echo 'Should have failed!'
--- a/Makefile.vofiles
+++ b/Makefile.vofiles
@@ -31,7 +31,10 @@
 
 GLOBFILES:=$(ALLVO:.vo=.glob)
 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