From afd9f3621d5c8c12c8d52bd233c77a92bd3afe16 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 16 Dec 2017 08:30:47 +0100
Subject: [make] More build fixes for static plugins and ocamlfind.

- In ocamlfind-based byte builds, link the VM statically as in native
  builds. This is the best way to get reliable, path-independent
  self-contained executables.

- In `make install`, install the `.cmx` files for plugins too. To
  statically link Coq plugins in native mode, both the `.cmx` and `.o`
  files must be present.
---
 META.coq         | 14 +++++++++-----
 Makefile.install |  7 ++++---
 2 files changed, 13 insertions(+), 8 deletions(-)

diff --git a/META.coq b/META.coq
index 504a85ba6c..d31b60cd02 100644
--- a/META.coq
+++ b/META.coq
@@ -47,13 +47,17 @@ package "vm" (
 
   directory        = "kernel/byterun"
 
-# We should generate this file at configure time for local byte builds
-# to work properly.
-
-# Enable this setting for local byte builds, disabling the one below.
+# We could generate this file at configure time for the share byte
+# build path to work properly.
+#
+# Enable this setting for local byte builds if you want dynamic linking:
+#
 #  linkopts(byte)   = "-dllpath path_to_coq/kernel/byterun/ -dllib -lcoqrun"
 
-  linkopts(byte)   = "-dllib -lcoqrun"
+# We currently prefer static linking of the VM.
+  archive(byte)    = "libcoqrun.a"
+  linkopts(byte)   = "-custom"
+
   linkopts(native) = "-cclib -lcoqrun"
 
 )
diff --git a/Makefile.install b/Makefile.install
index 84aa11a5ee..9a7229d524 100644
--- a/Makefile.install
+++ b/Makefile.install
@@ -107,9 +107,10 @@ install-devfiles:
 	$(MKDIR) $(FULLBINDIR)
 	$(MKDIR) $(FULLCOQLIB)
 	$(INSTALLSH)  $(FULLCOQLIB) $(GRAMMARCMA)
-	$(INSTALLSH)  $(FULLCOQLIB) $(INSTALLCMI)
-	$(INSTALLSH)  $(FULLCOQLIB) $(INSTALLCMX)
-	$(INSTALLSH)  $(FULLCOQLIB) $(PLUGINSCMO:.cmo=.o)
+	$(INSTALLSH)  $(FULLCOQLIB) $(INSTALLCMI)           # Regular CMI files
+	$(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)
-- 
cgit v1.2.3