diff options
| author | Enrico Tassi | 2019-02-07 17:33:44 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-02-07 17:33:44 +0100 |
| commit | e209341f6b9858279d2fe53d1eb795ff25925eed (patch) | |
| tree | 0fe0035e1688dd878a17e3f464de0d4fe0d82c0d /Makefile.build | |
| parent | 99c1d7b0ae1beed66fe8dd6a06db84dc0c8322d8 (diff) | |
| parent | f29aa6720eba884533972530b4283bf19d8410aa (diff) | |
Merge PR #9477: Makefiles: Fixes for byte compilation
Reviewed-by: gares
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 16 |
1 files changed, 10 insertions, 6 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) |