From f29aa6720eba884533972530b4283bf19d8410aa Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 5 Feb 2019 15:34:49 +0100
Subject: Makefiles: Fixes for byte compilation

- 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

cf https://github.com/coq/coq/issues/9464
---
 Makefile.build | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

(limited to 'Makefile.build')

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)
 
-- 
cgit v1.2.3