[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, 54 insertions, 0 deletions

diff --git a/coq-core.opam b/coq-core.opam
new file mode 100644
index 0000000000..8b8c43f66e
--- /dev/null
+++ b/coq-core.opam
@@ -0,0 +1,54 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+version: "dev"
+synopsis: "The Coq Proof Assistant -- Core Binaries and Tools"
+description: """
+Coq is a formal proof management system. It provides
+a formal language to write mathematical definitions, executable
+algorithms and theorems together with an environment for
+semi-interactive development of machine-checked proofs.
+
+Typical applications include the certification of properties of
+programming languages (e.g. the CompCert compiler certification
+project, or the Bedrock verified low-level programming library), the
+formalization of mathematics (e.g. the full formalization of the
+Feit-Thompson theorem or homotopy type theory) and teaching.
+
+This package includes the Coq core binaries, plugins, and tools, but
+not the vernacular standard library.
+
+Note that in this setup, Coq needs to be started with the -boot and
+-noinit options, as will otherwise fail to find the regular Coq
+prelude, now living in the coq-stdlib package."""
+maintainer: ["The Coq development team <coqdev@inria.fr>"]
+authors: ["The Coq development team, INRIA, CNRS, and contributors"]
+license: "LGPL-2.1-only"
+homepage: "https://coq.inria.fr/"
+doc: "https://coq.github.io/doc/"
+bug-reports: "https://github.com/coq/coq/issues"
+depends: [
+  "dune" {>= "2.5"}
+  "ocaml" {>= "4.05.0"}
+  "ocamlfind" {>= "1.8.1"}
+  "zarith" {>= "1.10"}
+  "ounit2" {with-test}
+]
+build: [
+  # Requires dune 2.8 due to https://github.com/ocaml/dune/issues/3219
+  # ["dune" "subst"] {pinned}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/coq/coq.git"
+build-env: [
+  [ COQ_CONFIGURE_PREFIX = "%{prefix}" ]
+]