Merge pull request #2055 from ejgallego/coq+rename

[coq] Rename `(coqlib ...)` to `(coq.theory ...)`

CHANGES.md

@@ -1,6 +1,10 @@
 unreleased
 ----------
 
+- [coq] Rename `(coqlib ...)` to `(coq.theory ...)`, support for
+  `coqlib` will be dropped in the 1.0 version of the Coq language
+  (#2055, @ejgallego)
+
 - [coq] Add `coq.pp` stanza to help with pre-processing of grammar
   files (#2054, @ejgallego, review by @rgrinberg)
 

doc/coq.rst

@@ -14,9 +14,9 @@ in the ``dune-project`` file. For example:
 
     (using coq 0.1)
 
-This will enable support for the ``coqlib`` stanza in the current project. If the
+This will enable support for the ``coq.theory`` stanza in the current project. If the
 language version is absent, dune will automatically add this line with the
-latest Coq version to the project file once a ``(coqlib ...)`` stanza is used anywhere.
+latest Coq version to the project file once a ``(coq.theory ...)`` stanza is used anywhere.
 
 
 Basic Usage
@@ -26,7 +26,7 @@ The basic form for defining Coq libraries is very similar to the OCaml form:
 
 .. code:: scheme
 
-    (coqlib
+    (coq.theory
      (name <module_prefix>)
      (public_name <package.lib_name>)
      (synopsis <text>)

src/dune_file.ml

@@ -1886,11 +1886,18 @@ module Coq = struct
 
   let unit_to_sexp () = Sexp.List []
 
-  let coqlib_p = "coqlib", decode >>| fun x -> [T x]
+  let coqlib_warn x =
+    Errors.warn x.loc
+      "(coqlib ...) is deprecated and will be removed in the Coq \
+       language version 1.0, please use (coq.theory ...) instead";
+    x
+
+  let coqlib_p = "coqlib", decode >>| fun x -> [T (coqlib_warn x)]
+  let coqtheory_p = "coq.theory", decode >>| fun x -> [T x]
   let coqpp_p = "coq.pp", Coqpp.(decode >>| fun x -> [T x])
 
   let unit_stanzas =
-    let+ r = return [coqlib_p; coqpp_p] in
+    let+ r = return [coqlib_p; coqtheory_p; coqpp_p] in
     ((), r)
 
   let key =

test/blackbox-tests/test-cases/coq/base/dune

@@ -1,4 +1,4 @@
-(coqlib
+(coq.theory
  (name basic)
  (public_name base.basic)
  (modules :standard)

test/blackbox-tests/test-cases/coq/ml_lib/theories/dune

@@ -1,4 +1,4 @@
-(coqlib
+(coq.theory
  (name Plugin)
  (public_name ml_lib.Plugin)
  (synopsis "Test Plugin")

test/blackbox-tests/test-cases/coq/rec_module/dune

@@ -1,4 +1,4 @@
-(coqlib
+(coq.theory
  (name rec_module)
  (public_name rec.module)
  (modules :standard)