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/4308dd8cd6deff4db946faf11822c80d16ee77ea
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

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)
--- 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!'