aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--META.coq14
-rw-r--r--Makefile.install7
2 files changed, 13 insertions, 8 deletions
diff --git a/META.coq b/META.coq
index 504a85ba6..d31b60cd0 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 84aa11a5e..9a7229d52 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)