aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-05-24 13:07:06 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-05-24 13:07:06 +0200
commit9a236b4f854bf59be80148db94344347dab27a42 (patch)
tree73904825dd4c1920550c880ca799bbd5e9d460cd
parent6622bc2a735dc8c3b33bd5c149860bbdb339e1a0 (diff)
parent3bf8320cb8614db81c366c9fb0bdea367e81441a (diff)
Merge PR #7575: [build] Add -cclib -lcoqrun options to build of kernel.cmxa.
-rw-r--r--META.coq3
-rw-r--r--Makefile.build6
-rw-r--r--Makefile.ide1
3 files changed, 5 insertions, 5 deletions
diff --git a/META.coq b/META.coq
index 12d7666cb..8d4c3d5f0 100644
--- a/META.coq
+++ b/META.coq
@@ -57,9 +57,6 @@ package "vm" (
# We currently prefer static linking of the VM.
archive(byte) = "libcoqrun.a"
linkopts(byte) = "-custom"
-
- linkopts(native) = "-cclib -lcoqrun"
-
)
package "kernel" (
diff --git a/Makefile.build b/Makefile.build
index 1326027ca..7454e1b0c 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -397,7 +397,6 @@ $(COQTOPEXE): $(TOPBIN:.opt=.$(BEST))
bin/%.opt$(EXE): topbin/%_bin.ml $(LINKCMX) $(LIBCOQRUN)
$(SHOW)'COQMKTOP -o $@'
$(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) \
- -I kernel/byterun/ -cclib -lcoqrun \
$(SYSMOD) -package camlp5.gramlib \
$(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) $< -o $@
$(STRIP) $@
@@ -637,6 +636,11 @@ kernel/kernel.cma: kernel/kernel.mllib
$(SHOW)'OCAMLC -a -o $@'
$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(VMBYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^)
+# Specific rule for kernel.cmxa as to adjoin -cclib -lcoqrun
+kernel/kernel.cmxa: kernel/kernel.mllib
+ $(SHOW)'OCAMLOPT -a -o $@'
+ $(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -I kernel/byterun/ -cclib -lcoqrun -a -o $@ $(filter-out %.mllib, $^)
+
%.cma: %.mllib
$(SHOW)'OCAMLC -a -o $@'
$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^)
diff --git a/Makefile.ide b/Makefile.ide
index 37f698e0c..48b554912 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -147,7 +147,6 @@ $(IDETOPEXE): $(IDETOP:.opt=.$(BEST))
$(IDETOP): ide/idetop.ml $(LINKCMX) $(LIBCOQRUN) $(IDETOPCMX)
$(SHOW)'COQMKTOP -o $@'
$(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) -I ide \
- -I kernel/byterun/ -cclib -lcoqrun \
$(SYSMOD) -package camlp5.gramlib \
$(LINKCMX) $(IDETOPCMX) $(OPTFLAGS) $(LINKMETADATA) $< -o $@
$(STRIP) $@