From 3bf8320cb8614db81c366c9fb0bdea367e81441a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Tue, 22 May 2018 10:49:47 +0200
Subject: [build] Add -cclib -lcoqrun options to build of kernel.cmxa.

It seems that it is standard practice in the OCaml world to set the
`-cclib` flags at library creation time, at least in native libraries.

Indeed, this seems to make linking easier as seen for example in #7563.
---
 META.coq       | 3 ---
 Makefile.build | 6 +++++-
 Makefile.ide   | 1 -
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/META.coq b/META.coq
index 3414ccbd4..570d9ce79 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 5f5eaf3a4..624ed8b47 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -393,7 +393,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) $@
@@ -577,6 +576,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) $@
-- 
cgit v1.2.3