From 7812c5f39dd166559847c1ece573b02653e62100 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 9 Mar 2017 01:08:42 +0100 Subject: [META] Update version number. --- META.coq | 59 ++++++++++++++++++++++++++++++++++------------------------- 1 file changed, 34 insertions(+), 25 deletions(-) diff --git a/META.coq b/META.coq index d83dab23d1..dea9fb458f 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" @@ -34,13 +44,12 @@ package "vm" ( description = "Coq VM" - version = "8.6" + version = "8.7" -# 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. +# 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. # Enable for local native & byte builds # directory = "kernel/byterun" @@ -57,7 +66,7 @@ package "vm" ( package "kernel" ( description = "Coq's Kernel" - version = "8.6" + version = "8.7" directory = "kernel" @@ -71,7 +80,7 @@ package "kernel" ( package "library" ( description = "Coq Libraries (vo) support" - version = "8.6" + version = "8.7" requires = "coq.kernel" @@ -85,7 +94,7 @@ package "library" ( package "intf" ( description = "Coq Public Data Types" - version = "8.6" + version = "8.7" requires = "coq.library" @@ -96,7 +105,7 @@ package "intf" ( package "engine" ( description = "Coq Tactic Engine" - version = "8.6" + version = "8.7" requires = "coq.library" directory = "engine" @@ -109,7 +118,7 @@ package "engine" ( package "pretyping" ( description = "Coq Pretyper" - version = "8.6" + version = "8.7" requires = "coq.engine" directory = "pretyping" @@ -122,7 +131,7 @@ package "pretyping" ( package "interp" ( description = "Coq Term Interpretation" - version = "8.6" + version = "8.7" requires = "coq.pretyping" directory = "interp" @@ -135,7 +144,7 @@ package "interp" ( package "grammar" ( description = "Coq Base Grammar" - version = "8.6" + version = "8.7" requires = "coq.interp" directory = "grammar" @@ -147,7 +156,7 @@ package "grammar" ( package "proofs" ( description = "Coq Proof Engine" - version = "8.6" + version = "8.7" requires = "coq.interp" directory = "proofs" @@ -160,7 +169,7 @@ package "proofs" ( package "parsing" ( description = "Coq Parsing Engine" - version = "8.6" + version = "8.7" requires = "coq.proofs" directory = "parsing" @@ -173,7 +182,7 @@ package "parsing" ( package "printing" ( description = "Coq Printing Engine" - version = "8.6" + version = "8.7" requires = "coq.parsing" directory = "printing" @@ -186,7 +195,7 @@ package "printing" ( package "tactics" ( description = "Coq Basic Tactics" - version = "8.6" + version = "8.7" requires = "coq.printing" directory = "tactics" @@ -199,7 +208,7 @@ package "tactics" ( package "vernac" ( description = "Coq Vernacular Interpreter" - version = "8.6" + version = "8.7" requires = "coq.tactics" directory = "vernac" @@ -212,7 +221,7 @@ package "vernac" ( package "stm" ( description = "Coq State Transactional Machine" - version = "8.6" + version = "8.7" requires = "coq.vernac" directory = "stm" @@ -225,7 +234,7 @@ package "stm" ( package "toplevel" ( description = "Coq Toplevel" - version = "8.6" + version = "8.7" requires = "coq.stm" directory = "toplevel" @@ -238,7 +247,7 @@ package "toplevel" ( package "highparsing" ( description = "Coq Extra Parsing" - version = "8.6" + version = "8.7" requires = "coq.toplevel" directory = "parsing" @@ -251,7 +260,7 @@ package "highparsing" ( package "ltac" ( description = "Coq LTAC Plugin" - version = "8.6" + version = "8.7" requires = "coq.highparsing" directory = "ltac" -- cgit v1.2.3 From ccb706774a8f9bf4f58f6899a58e6cc5117901a6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 9 Mar 2017 01:09:00 +0100 Subject: [META] Ltac now a plugin. --- META.coq | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/META.coq b/META.coq index dea9fb458f..5084237e8e 100644 --- a/META.coq +++ b/META.coq @@ -263,9 +263,9 @@ package "ltac" ( 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" ) -- cgit v1.2.3 From d201ccad094feda44a4d232de936df57c33f22f2 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 9 Mar 2017 01:09:50 +0100 Subject: [META] [build] Install dlls to kernel/byterun This makes the dll path consistent both in `-local` and non-local Coq install. --- META.coq | 15 +++++---------- Makefile.install | 5 +++-- configure.ml | 2 +- 3 files changed, 9 insertions(+), 13 deletions(-) diff --git a/META.coq b/META.coq index 5084237e8e..83134d4a08 100644 --- a/META.coq +++ b/META.coq @@ -43,21 +43,16 @@ package "lib" ( package "vm" ( description = "Coq VM" - version = "8.7" -# 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" 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 () -- cgit v1.2.3