1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
|
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!'
|
