[build] Split stdlib to it's own opam package.

We introduce a new package structure for Coq:

- `coq-core`: Coq's OCaml tools code and plugins
- `coq-stdlib`: Coq's stdlib [.vo files]
- `coq`: meta-package that pulls `coq-{core,stdlib}`

This has several advantages, in particular it allows to install Coq
without the stdlib which is useful in several scenarios, it also open
the door towards a versioning of the stdlib at the package level.

The main user-visible change is that Coq's ML development files now
live in `$lib/coq-core`, for compatibility in the regular build we
install a symlink and support both setups for a while.

Note that plugin developers and even `coq_makefile` should actually
rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust.

There is a transient state where we actually look for both
`$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support
the non-ocamlfind plus custom variables.

This will be much improved once #13617 is merged (which requires this
PR first), then, we will introduce a `coq.boot` library so finally
`coqdep`, `coqchk`, etc... can share the same path setup code.

IMHO the plan should work fine.

1 files changed, 591 insertions, 0 deletions

diff --git a/META.coq-core.in b/META.coq-core.in
new file mode 100644
index 0000000000..c58513979d
--- /dev/null
+++ b/META.coq-core.in
@@ -0,0 +1,591 @@
+# TODO: Generate automatically with Dune
+
+description = "The Coq Proof Assistant Plugin API"
+version = "8.14"
+
+directory = ""
+requires = ""
+
+package "config" (
+
+  description = "Coq Configuration Variables"
+  version     = "8.14"
+
+  directory   = "config"
+
+  archive(byte)    = "config.cma"
+  archive(native)  = "config.cmxa"
+)
+
+package "clib" (
+  description = "Base General Coq Library"
+  version     = "8.14"
+
+  directory   = "clib"
+  requires    = "str, unix, threads"
+
+  archive(byte)    = "clib.cma"
+  archive(native)  = "clib.cmxa"
+)
+
+package "lib" (
+
+  description = "Base Coq-Specific Library"
+  version     = "8.14"
+
+  directory   = "lib"
+
+  requires    = "coq-core.clib, coq-core.config, dynlink"
+
+  archive(byte)   = "lib.cma"
+  archive(native) = "lib.cmxa"
+
+)
+
+package "vm" (
+
+  description = "Coq VM"
+  version     = "8.14"
+
+  directory        = "kernel/byterun"
+
+# 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"
+
+# We currently prefer static linking of the VM.
+  archive(byte)    = "libcoqrun.a"
+  linkopts(byte)   = "-custom"
+)
+
+package "kernel" (
+
+  description = "Coq's Kernel"
+  version     = "8.14"
+
+  directory   = "kernel"
+
+  requires    = "coq-core.lib, coq-core.vm"
+
+  archive(byte)    = "kernel.cma"
+  archive(native)  = "kernel.cmxa"
+
+)
+
+package "library" (
+
+  description = "Coq Libraries (vo) support"
+  version     = "8.14"
+
+  requires    = "coq-core.kernel"
+
+  directory   = "library"
+
+  archive(byte)    = "library.cma"
+  archive(native)  = "library.cmxa"
+
+)
+
+package "engine" (
+
+  description = "Coq Tactic Engine"
+  version     = "8.14"
+
+  requires    = "coq-core.library"
+  directory   = "engine"
+
+  archive(byte)    = "engine.cma"
+  archive(native)  = "engine.cmxa"
+
+)
+
+package "pretyping" (
+
+  description = "Coq Pretyper"
+  version     = "8.14"
+
+  requires    = "coq-core.engine"
+  directory   = "pretyping"
+
+  archive(byte)    = "pretyping.cma"
+  archive(native)  = "pretyping.cmxa"
+
+)
+
+package "interp" (
+
+  description = "Coq Term Interpretation"
+  version     = "8.14"
+
+  requires    = "zarith, coq-core.pretyping"
+  directory   = "interp"
+
+  archive(byte)    = "interp.cma"
+  archive(native)  = "interp.cmxa"
+
+)
+
+package "proofs" (
+
+  description = "Coq Proof Engine"
+  version     = "8.14"
+
+  requires    = "coq-core.interp"
+  directory   = "proofs"
+
+  archive(byte)    = "proofs.cma"
+  archive(native)  = "proofs.cmxa"
+
+)
+
+package "gramlib" (
+
+  description = "Coq Grammar Engine"
+  version     = "8.14"
+
+  requires    = "coq-core.lib"
+  directory   = "gramlib/.pack"
+
+  archive(byte)    = "gramlib.cma"
+  archive(native)  = "gramlib.cmxa"
+)
+
+package "parsing" (
+
+  description = "Coq Parsing Engine"
+  version     = "8.14"
+
+  requires    = "coq-core.gramlib, coq-core.proofs"
+  directory   = "parsing"
+
+  archive(byte)    = "parsing.cma"
+  archive(native)  = "parsing.cmxa"
+
+)
+
+package "printing" (
+
+  description = "Coq Printing Engine"
+  version     = "8.14"
+
+  requires    = "coq-core.parsing"
+  directory   = "printing"
+
+  archive(byte)    = "printing.cma"
+  archive(native)  = "printing.cmxa"
+
+)
+
+package "tactics" (
+
+  description = "Coq Basic Tactics"
+  version     = "8.14"
+
+  requires    = "coq-core.printing"
+  directory   = "tactics"
+
+  archive(byte)    = "tactics.cma"
+  archive(native)  = "tactics.cmxa"
+
+)
+
+package "vernac" (
+
+  description = "Coq Vernacular Interpreter"
+  version     = "8.14"
+
+  requires    = "coq-core.tactics"
+  directory   = "vernac"
+
+  archive(byte)    = "vernac.cma"
+  archive(native)  = "vernac.cmxa"
+
+)
+
+package "stm" (
+
+  description = "Coq State Transaction Machine"
+  version     = "8.14"
+
+  requires    = "coq-core.sysinit"
+  directory   = "stm"
+
+  archive(byte)    = "stm.cma"
+  archive(native)  = "stm.cmxa"
+
+)
+
+package "sysinit" (
+
+  description = "Coq initialization"
+  version     = "8.14"
+
+  requires    = "coq-core.vernac"
+  directory   = "sysinit"
+
+  archive(byte)    = "sysinit.cma"
+  archive(native)  = "sysinit.cmxa"
+
+)
+
+package "toplevel" (
+
+  description = "Coq Toplevel"
+  version     = "8.14"
+
+  requires    = "coq-core.stm"
+  directory   = "toplevel"
+
+  archive(byte)    = "toplevel.cma"
+  archive(native)  = "toplevel.cmxa"
+
+)
+
+package "idetop" (
+
+  description = "Coq IDE Libraries"
+  version     = "8.14"
+
+  requires    = "coq-core.toplevel"
+  directory   = "ide"
+
+  archive(byte)    = "coqidetop.cma"
+  archive(native)  = "coqidetop.cmxa"
+
+)
+
+package "ide" (
+
+  description = "Coq IDE Libraries"
+  version     = "8.14"
+
+  requires    = "coq-core.lib, coq-core.ideprotocol, lablgtk3, lablgtk3-sourceview3"
+  directory   = "ide"
+
+  archive(byte)    = "ide.cma"
+  archive(native)  = "ide.cmxa"
+
+)
+
+package "ideprotocol" (
+
+  description = "Coq IDE protocol"
+  version     = "8.14"
+
+  requires    = "coq-core.toplevel"
+  directory   = "ide/protocol"
+
+  archive(byte)    = "ideprotocol.cma"
+  archive(native)  = "ideprotocol.cmxa"
+
+)
+
+package "plugins" (
+
+  description = "Coq built-in plugins"
+  version     = "8.14"
+
+  directory   = "plugins"
+
+  package "ltac" (
+
+    description = "Coq LTAC Plugin"
+    version     = "8.14"
+
+    requires    = "coq-core.stm"
+    directory   = "ltac"
+
+    archive(byte)    = "ltac_plugin.cmo"
+    archive(native)  = "ltac_plugin.cmx"
+
+    plugin(byte)    = "ltac_plugin.cmo"
+    plugin(native)  = "ltac_plugin.cmxs"
+  )
+
+  package "tauto" (
+
+    description = "Coq tauto plugin"
+    version     = "8.14"
+
+    requires    = "coq-core.plugins.ltac"
+    directory   = "ltac"
+
+    archive(byte)    = "tauto_plugin.cmo"
+    archive(native)  = "tauto_plugin.cmx"
+
+    plugin(byte)    = "tauto_plugin.cmo"
+    plugin(native)  = "tauto_plugin.cmxs"
+  )
+
+  package "omega" (
+
+    description = "Coq omega plugin"
+    version     = "8.14"
+
+    requires    = "coq-core.plugins.ltac"
+    directory   = "omega"
+
+    archive(byte)    = "omega_plugin.cmo"
+    archive(native)  = "omega_plugin.cmx"
+
+    plugin(byte)    = "omega_plugin.cmo"
+    plugin(native)  = "omega_plugin.cmxs"
+  )
+
+  package "micromega" (
+
+    description = "Coq micromega plugin"
+    version     = "8.14"
+
+    requires    = "coq-core.plugins.ltac"
+    directory   = "micromega"
+
+    archive(byte)    = "micromega_plugin.cmo"
+    archive(native)  = "micromega_plugin.cmx"
+
+    plugin(byte)    = "micromega_plugin.cmo"
+    plugin(native)  = "micromega_plugin.cmxs"
+  )
+
+  package "zify" (
+
+    description = "Coq Zify plugin"
+    version     = "8.14"
+
+    requires    = "coq-core.plugins.ltac"
+    directory   = "micromega"
+
+    archive(byte)    = "zify_plugin.cmo"
+    archive(native)  = "zify_plugin.cmx"
+
+    plugin(byte)    = "zify_plugin.cmo"
+    plugin(native)  = "zify_plugin.cmxs"
+  )
+
+  package "ring" (
+
+    description = "Coq ring plugin"
+    version     = "8.14"
+
+    requires    = ""
+    directory   = "ring"
+
+    archive(byte)    = "ring_plugin.cmo"
+    archive(native)  = "ring_plugin.cmx"
+
+    plugin(byte)    = "ring_plugin.cmo"
+    plugin(native)  = "ring_plugin.cmxs"
+  )
+
+  package "extraction" (
+
+    description = "Coq extraction plugin"
+    version     = "8.14"
+
+    requires    = "coq-core.plugins.ltac"
+    directory   = "extraction"
+
+    archive(byte)    = "extraction_plugin.cmo"
+    archive(native)  = "extraction_plugin.cmx"
+
+    plugin(byte)    = "extraction_plugin.cmo"
+    plugin(native)  = "extraction_plugin.cmxs"
+  )
+
+  package "cc" (
+
+    description = "Coq cc plugin"
+    version     = "8.14"
+
+    requires    = "coq-core.plugins.ltac"
+    directory   = "cc"
+
+    archive(byte)    = "cc_plugin.cmo"
+    archive(native)  = "cc_plugin.cmx"
+
+    plugin(byte)    = "cc_plugin.cmo"
+    plugin(native)  = "cc_plugin.cmxs"
+  )
+
+  package "firstorder" (
+
+    description = "Coq ground plugin"
+    version     = "8.14"
+
+    requires    = "coq-core.plugins.ltac"
+    directory   = "firstorder"
+
+    archive(byte)    = "ground_plugin.cmo"
+    archive(native)  = "ground_plugin.cmx"
+
+    plugin(byte)    = "ground_plugin.cmo"
+    plugin(native)  = "ground_plugin.cmxs"
+  )
+
+  package "rtauto" (
+
+    description = "Coq rtauto plugin"
+    version     = "8.14"
+
+    requires    = "coq-core.plugins.ltac"
+    directory   = "rtauto"
+
+    archive(byte)    = "rtauto_plugin.cmo"
+    archive(native)  = "rtauto_plugin.cmx"
+
+    plugin(byte)    = "rtauto_plugin.cmo"
+    plugin(native)  = "rtauto_plugin.cmxs"
+  )
+
+  package "btauto" (
+
+    description = "Coq btauto plugin"
+    version     = "8.14"
+
+    requires    = "coq-core.plugins.ltac"
+    directory   = "btauto"
+
+    archive(byte)    = "btauto_plugin.cmo"
+    archive(native)  = "btauto_plugin.cmx"
+
+    plugin(byte)    = "btauto_plugin.cmo"
+    plugin(native)  = "btauto_plugin.cmxs"
+  )
+
+  package "funind" (
+
+    description = "Coq recdef plugin"
+    version     = "8.14"
+
+    requires    = "coq-core.plugins.extraction"
+    directory   = "funind"
+
+    archive(byte)    = "recdef_plugin.cmo"
+    archive(native)  = "recdef_plugin.cmx"
+
+    plugin(byte)    = "recdef_plugin.cmo"
+    plugin(native)  = "recdef_plugin.cmxs"
+  )
+
+  package "nsatz" (
+
+    description = "Coq nsatz plugin"
+    version     = "8.14"
+
+    requires    = "zarith, coq-core.plugins.ltac"
+    directory   = "nsatz"
+
+    archive(byte)    = "nsatz_plugin.cmo"
+    archive(native)  = "nsatz_plugin.cmx"
+
+    plugin(byte)    = "nsatz_plugin.cmo"
+    plugin(native)  = "nsatz_plugin.cmxs"
+  )
+
+  package "rsyntax" (
+
+    description = "Coq rsyntax plugin"
+    version     = "8.14"
+
+    requires    = ""
+    directory   = "syntax"
+
+    archive(byte)    = "r_syntax_plugin.cmo"
+    archive(native)  = "r_syntax_plugin.cmx"
+
+    plugin(byte)    = "r_syntax_plugin.cmo"
+    plugin(native)  = "r_syntax_plugin.cmxs"
+  )
+
+  package "string_notation" (
+
+    description = "Coq string_notation plugin"
+    version     = "8.14"
+
+    requires    = "coq-core.vernac"
+    directory   = "syntax"
+
+    archive(byte)    = "string_notation_plugin.cmo"
+    archive(native)  = "string_notation_plugin.cmx"
+
+    plugin(byte)    = "string_notation_plugin.cmo"
+    plugin(native)  = "string_notation_plugin.cmxs"
+  )
+
+  package "numeral_notation" (
+    description = "Coq numeral notation plugin"
+    version 	= "8.14"
+
+    requires    = "coq-core.vernac"
+    directory 	= "numeral_notation"
+
+    archive(byte)    = "numeral_notation_plugin.cmo"
+    archive(native)  = "numeral_notation_plugin.cmx"
+
+    plugin(byte)    = "numeral_notation_plugin.cmo"
+    plugin(native)  = "numeral_notation_plugin.cmxs"
+  )
+
+  package "derive" (
+
+    description = "Coq derive plugin"
+    version     = "8.14"
+
+    requires    = ""
+    directory   = "derive"
+
+    archive(byte)    = "derive_plugin.cmo"
+    archive(native)  = "derive_plugin.cmx"
+
+    plugin(byte)    = "derive_plugin.cmo"
+    plugin(native)  = "derive_plugin.cmxs"
+  )
+
+  package "ssrmatching" (
+
+    description = "Coq ssrmatching plugin"
+    version     = "8.14"
+
+    requires    = "coq-core.plugins.ltac"
+    directory   = "ssrmatching"
+
+    archive(byte)    = "ssrmatching_plugin.cmo"
+    archive(native)  = "ssrmatching_plugin.cmx"
+
+    plugin(byte)    = "ssrmatching_plugin.cmo"
+    plugin(native)  = "ssrmatching_plugin.cmxs"
+  )
+
+  package "ssreflect" (
+
+    description = "Coq ssreflect plugin"
+    version     = "8.14"
+
+    requires    = "coq-core.plugins.ssrmatching"
+    directory   = "ssr"
+
+    archive(byte)    = "ssreflect_plugin.cmo"
+    archive(native)  = "ssreflect_plugin.cmx"
+
+    plugin(byte)    = "ssreflect_plugin.cmo"
+    plugin(native)  = "ssreflect_plugin.cmxs"
+  )
+
+  package "ltac2" (
+
+    description = "Coq Ltac2 Plugin"
+    version     = "8.14"
+
+    requires    = "coq-core.plugins.ltac"
+    directory   = "../user-contrib/Ltac2"
+
+    archive(byte)    = "ltac2_plugin.cmo"
+    archive(native)  = "ltac2_plugin.cmx"
+
+    plugin(byte)    = "ltac2_plugin.cmo"
+    plugin(native)  = "ltac2_plugin.cmxs"
+  )
+)