Merge PR #12567: [build] Split stdlib to it's own package.

Reviewed-by: Zimmi48
Ack-by: JasonGross
Ack-by: gares
Ack-by: LasseBlaauwbroek
Ack-by: silene
Ack-by: vbgl

8 files changed, 31 insertions, 13 deletions

diff --git a/doc/changelog/11-infrastructure-and-dependencies/12567-dune+split_stdlib.rst b/doc/changelog/11-infrastructure-and-dependencies/12567-dune+split_stdlib.rst
new file mode 100644
index 0000000000..6fe6f62faa
--- /dev/null
+++ b/doc/changelog/11-infrastructure-and-dependencies/12567-dune+split_stdlib.rst
@@ -0,0 +1,14 @@
+- **Changed:**
+  Coq's configure script now requires absolute paths for the `-prefix`
+  option.
+  (`#12567 <https://github.com/coq/coq/pull/12567>`_,
+  by Emilio Jesus Gallego Arias).
+
+- **Changed:**
+  The regular Coq package has been split in two: coq-core, with
+  OCaml-based libraries and tools; and coq-stdlib, which contains the
+  Gallina-based standard library. The package Coq now depends on both
+  for compatiblity.
+  (`#12567 <https://github.com/coq/coq/pull/12567>`_,
+  by Emilio Jesus Gallego Arias, review by Vincent Laporte, Guillaume
+  Melquiond, Enrico Tassi, and Théo Zimmerman).
diff --git a/doc/dune b/doc/dune
index c82e5a3df4..97bd437097 100644
--- a/doc/dune
+++ b/doc/dune
@@ -13,7 +13,8 @@
   ;   + %{bin:coqdoc} etc...
   ;   + config/coq_config.py
   ;   + tools/coqdoc/coqdoc.css
-  (package coq)
+  (package coq-core)
+  (package coq-stdlib)
   (source_tree sphinx)
   (source_tree tools/coqrst)
   unreleased.rst
@@ -26,7 +27,8 @@
  ; Cannot use this deps alias because of ocaml/dune#3415
  ; (deps (alias refman-deps))
  (deps
-  (package coq)
+  (package coq-core)
+  (package coq-stdlib)
   (source_tree sphinx)
   (source_tree tools/coqrst)
   unreleased.rst
@@ -41,7 +43,8 @@
  ; Cannot use this deps alias because of ocaml/dune#3415
  ; (deps (alias refman-deps))
  (deps
-  (package coq)
+  (package coq-core)
+  (package coq-stdlib)
   (source_tree sphinx)
   (source_tree tools/coqrst)
   unreleased.rst
diff --git a/doc/plugin_tutorial/tuto0/src/dune b/doc/plugin_tutorial/tuto0/src/dune
index ab9b4dd531..c7ed997221 100644
--- a/doc/plugin_tutorial/tuto0/src/dune
+++ b/doc/plugin_tutorial/tuto0/src/dune
@@ -1,6 +1,6 @@
 (library
  (name tuto0_plugin)
- (public_name coq.plugins.tutorial.p0)
- (libraries coq.plugins.ltac))
+ (public_name coq-core.plugins.tutorial.p0)
+ (libraries coq-core.plugins.ltac))
 
 (coq.pp (modules g_tuto0))
diff --git a/doc/plugin_tutorial/tuto1/src/dune b/doc/plugin_tutorial/tuto1/src/dune
index 054d5ecd26..bf87222e16 100644
--- a/doc/plugin_tutorial/tuto1/src/dune
+++ b/doc/plugin_tutorial/tuto1/src/dune
@@ -1,6 +1,6 @@
 (library
  (name tuto1_plugin)
- (public_name coq.plugins.tutorial.p1)
- (libraries coq.plugins.ltac))
+ (public_name coq-core.plugins.tutorial.p1)
+ (libraries coq-core.plugins.ltac))
 
 (coq.pp (modules g_tuto1))
diff --git a/doc/plugin_tutorial/tuto2/src/dune b/doc/plugin_tutorial/tuto2/src/dune
index 8c4b04b1ae..0797debccf 100644
--- a/doc/plugin_tutorial/tuto2/src/dune
+++ b/doc/plugin_tutorial/tuto2/src/dune
@@ -1,6 +1,6 @@
 (library
  (name tuto2_plugin)
- (public_name coq.plugins.tutorial.p2)
- (libraries coq.plugins.ltac))
+ (public_name coq-core.plugins.tutorial.p2)
+ (libraries coq-core.plugins.ltac))
 
 (coq.pp (modules g_tuto2))
diff --git a/doc/plugin_tutorial/tuto3/src/dune b/doc/plugin_tutorial/tuto3/src/dune
index 678dd71328..dcecf0852e 100644
--- a/doc/plugin_tutorial/tuto3/src/dune
+++ b/doc/plugin_tutorial/tuto3/src/dune
@@ -1,7 +1,7 @@
 (library
  (name tuto3_plugin)
- (public_name coq.plugins.tutorial.p3)
+ (public_name coq-core.plugins.tutorial.p3)
  (flags :standard -warn-error -3)
- (libraries coq.plugins.ltac))
+ (libraries coq-core.plugins.ltac))
 
 (coq.pp (modules g_tuto3))
diff --git a/doc/stdlib/dune b/doc/stdlib/dune
index 0b6ca5f178..6b51202f6e 100644
--- a/doc/stdlib/dune
+++ b/doc/stdlib/dune
@@ -22,7 +22,8 @@
    (:header %{project_root}/doc/common/styles/html/coqremote/header.html)
    (:footer %{project_root}/doc/common/styles/html/coqremote/footer.html)
    ; For .glob files, should be gone when Coq Dune is smarter.
-   (package coq))
+   (package coq-core)
+   (package coq-stdlib))
  (action
   (progn
    (run mkdir -p html)
diff --git a/doc/tools/docgram/dune b/doc/tools/docgram/dune
index 1c07d00d4f..4ba60ddd9f 100644
--- a/doc/tools/docgram/dune
+++ b/doc/tools/docgram/dune
@@ -1,6 +1,6 @@
 (executable
  (name doc_grammar)
- (libraries coq.clib coqpp))
+ (libraries coq-core.clib coqpp))
 
 (env (_ (binaries doc_grammar.exe)))