Merge PR#464: [META] More fixes

3 files changed, 42 insertions, 37 deletions

diff --git a/META.coq b/META.coq
index d83dab23d1..83134d4a08 100644
--- a/META.coq
+++ b/META.coq
@@ -1,5 +1,15 @@
+# TODO: Move to META.in once coq_makefile2 is merged.
+# We need to reuse:
+# - The variable substitution mechanism.
+# - Sourcing of "coq_install_path" and "coq_version" variables.
+#
+# With this rules, we would have:
+#  version = ${coq_version}
+# and
+#  linkopts(byte)   = "-dllpath ${coq_install_path}/kernel/byterun/ -dllib -lcoqrun"
+
 description = "The Coq Proof Assistant Plugin API"
-version = "8.6"
+version = "8.7"
 
 directory = ""
 requires = "camlp5"
@@ -7,7 +17,7 @@ requires = "camlp5"
 package "config" (
 
   description = "Coq Configuration Variables"
-  version     = "8.6"
+  version     = "8.7"
 
   directory   = "config"
 
@@ -16,7 +26,7 @@ package "config" (
 package "lib" (
 
   description = "Base Coq Library"
-  version     = "8.6"
+  version     = "8.7"
 
   directory   = "lib"
 
@@ -33,22 +43,16 @@ package "lib" (
 package "vm" (
 
   description = "Coq VM"
+  version     = "8.7"
 
-  version     = "8.6"
-
-# EJGA FIXME: Unfortunately dllpath is dependent on the type of Coq
-# install. In a local one we'll want kernel/byterun, in a non-local
-# one we want to set it to coqlib. We should thus generate this file
-# at configure time, but let's hear for some more feedback from
-# experts.
+  directory        = "kernel/byterun"
 
-# Enable for local native & byte builds
-#  directory        = "kernel/byterun"
+# We should generate this file at configure time for local byte builds
+# to work properly.
 
-# Enable for local byte builds and set up properly
-#  linkopts(byte)   = "-dllpath /path/to/coq/kernel/byterun/ -dllib -lcoqrun"
+# Enable this setting for local byte builds, disabling the one below.
+#  linkopts(byte)   = "-dllpath path_to_coq/kernel/byterun/ -dllib -lcoqrun"
 
-# Disable for local byte builds
   linkopts(byte)   = "-dllib -lcoqrun"
   linkopts(native) = "-cclib -lcoqrun"
 
@@ -57,7 +61,7 @@ package "vm" (
 package "kernel" (
 
   description = "Coq's Kernel"
-  version     = "8.6"
+  version     = "8.7"
 
   directory   = "kernel"
 
@@ -71,7 +75,7 @@ package "kernel" (
 package "library" (
 
   description = "Coq Libraries (vo) support"
-  version     = "8.6"
+  version     = "8.7"
 
   requires    = "coq.kernel"
 
@@ -85,7 +89,7 @@ package "library" (
 package "intf" (
 
   description = "Coq Public Data Types"
-  version     = "8.6"
+  version     = "8.7"
 
   requires    = "coq.library"
 
@@ -96,7 +100,7 @@ package "intf" (
 package "engine" (
 
   description = "Coq Tactic Engine"
-  version     = "8.6"
+  version     = "8.7"
 
   requires    = "coq.library"
   directory   = "engine"
@@ -109,7 +113,7 @@ package "engine" (
 package "pretyping" (
 
   description = "Coq Pretyper"
-  version     = "8.6"
+  version     = "8.7"
 
   requires    = "coq.engine"
   directory   = "pretyping"
@@ -122,7 +126,7 @@ package "pretyping" (
 package "interp" (
 
   description = "Coq Term Interpretation"
-  version     = "8.6"
+  version     = "8.7"
 
   requires    = "coq.pretyping"
   directory   = "interp"
@@ -135,7 +139,7 @@ package "interp" (
 package "grammar" (
 
   description = "Coq Base Grammar"
-  version     = "8.6"
+  version     = "8.7"
 
   requires    = "coq.interp"
   directory   = "grammar"
@@ -147,7 +151,7 @@ package "grammar" (
 package "proofs" (
 
   description = "Coq Proof Engine"
-  version     = "8.6"
+  version     = "8.7"
 
   requires    = "coq.interp"
   directory   = "proofs"
@@ -160,7 +164,7 @@ package "proofs" (
 package "parsing" (
 
   description = "Coq Parsing Engine"
-  version     = "8.6"
+  version     = "8.7"
 
   requires    = "coq.proofs"
   directory   = "parsing"
@@ -173,7 +177,7 @@ package "parsing" (
 package "printing" (
 
   description = "Coq Printing Engine"
-  version     = "8.6"
+  version     = "8.7"
 
   requires    = "coq.parsing"
   directory   = "printing"
@@ -186,7 +190,7 @@ package "printing" (
 package "tactics" (
 
   description = "Coq Basic Tactics"
-  version     = "8.6"
+  version     = "8.7"
 
   requires    = "coq.printing"
   directory   = "tactics"
@@ -199,7 +203,7 @@ package "tactics" (
 package "vernac" (
 
   description = "Coq Vernacular Interpreter"
-  version     = "8.6"
+  version     = "8.7"
 
   requires    = "coq.tactics"
   directory   = "vernac"
@@ -212,7 +216,7 @@ package "vernac" (
 package "stm" (
 
   description = "Coq State Transactional Machine"
-  version     = "8.6"
+  version     = "8.7"
 
   requires    = "coq.vernac"
   directory   = "stm"
@@ -225,7 +229,7 @@ package "stm" (
 package "toplevel" (
 
   description = "Coq Toplevel"
-  version     = "8.6"
+  version     = "8.7"
 
   requires    = "coq.stm"
   directory   = "toplevel"
@@ -238,7 +242,7 @@ package "toplevel" (
 package "highparsing" (
 
   description = "Coq Extra Parsing"
-  version     = "8.6"
+  version     = "8.7"
 
   requires    = "coq.toplevel"
   directory   = "parsing"
@@ -251,12 +255,12 @@ package "highparsing" (
 package "ltac" (
 
   description = "Coq LTAC Plugin"
-  version     = "8.6"
+  version     = "8.7"
 
   requires    = "coq.highparsing"
-  directory   = "ltac"
+  directory   = "plugins/ltac"
 
-  archive(byte)    = "ltac.cma"
-  archive(native)  = "ltac.cmxa"
+  archive(byte)    = "ltac_plugin.cmo"
+  archive(native)  = "ltac_plugin.cmx"
 
 )
diff --git a/Makefile.install b/Makefile.install
index 4800ea0b96..bde0355519 100644
--- a/Makefile.install
+++ b/Makefile.install
@@ -104,11 +104,12 @@ install-library:
 	$(MKDIR) $(FULLCOQLIB)
 	$(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS)
 	$(MKDIR) $(FULLCOQLIB)/user-contrib
+	$(MKDIR) $(FULLCOQLIB)/kernel/byterun
 ifndef CUSTOM
-	$(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB)
+	$(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB)/kernel/byterun
 endif
 ifeq ($(BEST),opt)
-	$(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB)
+	$(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB)/kernel/byterun
 	$(INSTALLSH) $(FULLCOQLIB) $(PLUGINSOPT)
 endif
 # csdpcert is not meant to be directly called by the user; we install
diff --git a/configure.ml b/configure.ml
index e711367510..82ce931d67 100644
--- a/configure.ml
+++ b/configure.ml
@@ -926,7 +926,7 @@ let config_runtime () =
   | _ ->
     let ld="CAML_LD_LIBRARY_PATH" in
     build_loadpath := sprintf "export %s:='%s/kernel/byterun':$(%s)" ld coqtop ld;
-    ["-dllib";"-lcoqrun";"-dllpath";libdir]
+    ["-dllib";"-lcoqrun";"-dllpath";libdir/"kernel/byterun"]
 
 let vmbyteflags = config_runtime ()