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
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
|
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
|
