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

diff --git a/dune-project b/dune-project
index 03e7147019..251fbd92aa 100644
--- a/dune-project
+++ b/dune-project
@@ -22,14 +22,13 @@
 ; Note that we use coq.opam.template to have dune add the correct opam
 ; prefix for configure
 (package
- (name coq)
+ (name coq-core)
  (depends
   (ocaml (>= 4.05.0))
-  (dune  (>= 2.5.0))
   (ocamlfind (>= 1.8.1))
   (zarith (>= 1.10))
   (ounit2 :with-test))
- (synopsis "The Coq Proof Assistant")
+ (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
@@ -39,13 +38,38 @@ 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."))
+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."))
+
+(package
+ (name coq-stdlib)
+ (depends
+  (coq-core (= :version)))
+ (synopsis "The Coq Proof Assistant -- Standard Library")
+ (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 Standard Library, that is to say, the
+set of modules usually bound to the Coq.* namespace."))
 
 (package
  (name coqide-server)
  (depends
-  (dune (>= 2.5.0))
-  (coq (= :version)))
+  (coq-core (= :version)))
  (synopsis "The Coq Proof Assistant, XML protocol server")
  (description "Coq is a formal proof management system. It provides
 a formal language to write mathematical definitions, executable
@@ -60,7 +84,6 @@ structured way."))
 (package
  (name coqide)
  (depends
-  (dune (>= 2.5.0))
   (coqide-server (= :version)))
  (synopsis "The Coq Proof Assistant --- GTK3 IDE")
  (description "Coq is a formal proof management system. It provides
@@ -86,3 +109,19 @@ semi-interactive development of machine-checked proofs.
 
 This package provides the Coq Reference Manual."))
 
+(package
+ (name coq)
+ (depends
+  (coq-core (= :version))
+  (coq-stdlib (= :version)))
+ (synopsis "The Coq Proof Assistant")
+ (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."))