Create (stdlib) syntax for Coq stanza

Fixes ocaml#6163

Co-authored-by: Christine Rose <[email protected]>
Signed-off-by: Lasse Blaauwbroek <[email protected]>

CHANGES.md

@@ -63,6 +63,10 @@
 
 - The test suite for Coq now requires Coq >= 8.16 due to changes in the
   plugin loading mechanism upstream (which now uses findlib).
+
+- Starting with Coq build language 0.6, theories can be built without importing
+  Coq's standard library by including `(stdlib no)`.
+  (#6165 #6164, fixes #6163, @ejgallego @Alizter @LasseBlaauwbroek)
 
 3.4.1 (26-07-2022)
 ------------------

doc/coq.rst

@@ -30,7 +30,7 @@ version<coq-lang>` in the :ref:`dune-project` file. For example, adding
 
 .. code:: scheme
 
-    (using coq 0.4)
+    (using coq 0.6)
 
 to a :ref:`dune-project` file enables using the ``coq.theory`` stanza and other
 ``coq.*`` stanzas. See the :ref:`Dune Coq language<coq-lang>` section for more
@@ -53,6 +53,7 @@ stanza:
      (modules <ordered_set_lang>)
      (plugins <ocaml_plugins>)
      (flags <coq_flags>)
+     (stdlib <stdlib_included>)
      (mode <coq_native_mode>)
      (theories <coq_theories>))
 
@@ -98,6 +99,11 @@ The semantics of the fields are:
   is taken from the value set in the ``(coq (flags <flags>))`` field in ``env``
   profile. See :ref:`dune-env` for more information.
 
+- ``<stdlib_included>`` can either be ``yes`` or ``no``, currently defaulting to
+  ``yes``. When set to ``no``, Coq's standard library won't be visible from this
+  theory, which means the ``Coq`` prefix won't be bound, and ``Coq.Init.Prelude``
+  won't be imported by default.
+
 - The path to the installed locations of the ``<ocaml_plugins>`` is passed to
   ``coqdep`` and ``coqc`` using Coq's ``-I`` flag. This allows a Coq theory to
   depend on OCaml plugins.
@@ -235,6 +241,8 @@ The supported Coq language versions (not the version of Coq) are:
 - ``0.3``: Support for ``(mode native)`` requires Coq >= 8.10 (and Dune >= 2.9
   for Coq >= 8.14).
 - ``0.4``: Support for interproject composition of theories.
+- ``0.5``: ``(libraries ...)`` field deprecated in favor of ``(plugins ...)`` field.
+- ``0.6``: Support for ``(stdlib no)``.
 
 .. _coq-lang-1.0:
 
@@ -267,7 +275,7 @@ process by using the ``coq.extraction`` stanza:
 - ``(extracted_modules <names>)`` is an exhaustive list of OCaml modules
   extracted.
 
-- ``<optional-fields>`` are ``flags``, ``theories``, and ``plugins``. All of
+- ``<optional-fields>`` are ``flags``, ``stdlib``, ``theories``, and ``plugins``. All of
   these fields have the same meaning as in the ``coq.theory`` stanza.
 
 The extracted sources can then be used in ``executable`` or ``library`` stanzas

src/dune_rules/coq_stanza.ml

@@ -25,6 +25,7 @@ let coq_syntax =
     ; ((0, 3), `Since (2, 8))
     ; ((0, 4), `Since (3, 3))
     ; ((0, 5), `Since (3, 4))
+    ; ((0, 6), `Since (3, 5))
     ]
 
 module Buildable = struct
@@ -63,7 +64,8 @@ module Buildable = struct
            (Dune_lang.Syntax.since coq_syntax (0, 3) >>> Coq_mode.decode))
     and+ use_stdlib =
       field ~default:true "stdlib"
-        Dune_lang.Decoder.(enum [ ("yes", true); ("no", false) ])
+        (Dune_lang.Syntax.since coq_syntax (0, 6)
+        >>> enum [ ("yes", true); ("no", false) ])
     and+ libraries =
       field "libraries" ~default:[]
         (Dune_sexp.Syntax.deprecated_in coq_syntax (0, 5)

test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/A/a.v

@@ -0,0 +1,6 @@
+Print LoadPath.
+Fail Print Prelude.
+From Coq Require Import Prelude.
+Print Prelude.
+Require Import mytheory.
+Check Hello.

test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/A/dune

@@ -0,0 +1,4 @@
+(coq.theory
+ (name A)
+ (stdlib no)
+ (theories Coq))

test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/A/dune-project

@@ -0,0 +1,2 @@
+(lang dune 3.5)
+(using coq 0.6)

test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/B/b.v

@@ -0,0 +1,4 @@
+Print LoadPath.
+Print Prelude.
+Require Import mytheory.
+Check Hello.

test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/B/dune

@@ -0,0 +1,4 @@
+(coq.theory
+ (name B)
+ (stdlib yes)
+ (theories Coq))

test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/B/dune-project

@@ -0,0 +1,2 @@
+(lang dune 3.5)
+(using coq 0.6)

test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/Coq/Init/Prelude.v

@@ -0,0 +1,2 @@
+Unset Elimination Schemes.
+Inductive BootType := boot | type.

test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/Coq/dune

@@ -0,0 +1,6 @@
+(coq.theory
+ (name Coq)
+ (package Coq)
+ (boot))
+
+(include_subdirs qualified)

test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/Coq/dune-project

@@ -0,0 +1,2 @@
+(lang dune 3.3)
+(using coq 0.4)

test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/Coq/mytheory.v

@@ -0,0 +1,2 @@
+
+Inductive Hello := World | Bye.

test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/dune-workspace

@@ -0,0 +1 @@
+(lang dune 3.3)

test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/run.t

@@ -0,0 +1,36 @@
+Testing composition of theories across a Dune workspace with a boot library and
+importing ``stdlib`` enabled or disabled.
+
+Composing library A depending on Coq but having `(stdlib no)`:
+
+  $ dune build A
+  Logical Path / Physical path:
+  A
+    $TESTCASE_ROOT/_build/default/A
+  Coq
+    $TESTCASE_ROOT/_build/default/Coq
+  Coq.Init
+    $TESTCASE_ROOT/_build/default/Coq/Init
+  Module
+  Prelude
+  := Struct Inductive BootType : Set :=  boot : BootType | type : BootType. End
+
+  Hello
+       : Set
+
+Composing library B depending on Coq but having `(stdlib yes)`:
+
+  $ dune build B
+  Logical Path / Physical path:
+  B
+    $TESTCASE_ROOT/_build/default/B
+  Coq
+    $TESTCASE_ROOT/_build/default/Coq
+  Coq.Init
+    $TESTCASE_ROOT/_build/default/Coq/Init
+  Module
+  Prelude
+  := Struct Inductive BootType : Set :=  boot : BootType | type : BootType. End
+
+  Hello
+       : Set

test/blackbox-tests/test-cases/coq/coqtop-root.t/run.t

@@ -14,5 +14,5 @@ This test is currently broken due to the workspace resolution being faulty #5899
   1 | (coq.theory
   2 |  (name foo))
   Error: 'coq.theory' is available only when coq is enabled in the dune-project
-  file. You must enable it using (using coq 0.5) in your dune-project file.
+  file. You must enable it using (using coq 0.6) in your dune-project file.
   [1]

test/blackbox-tests/test-cases/coq/github3624.t

@@ -16,5 +16,5 @@ that the error message is good when the coq extension is not enabled.
   1 | (coq.theory
   2 |  (name foo))
   Error: 'coq.theory' is available only when coq is enabled in the dune-project
-  file. You must enable it using (using coq 0.5) in your dune-project file.
+  file. You must enable it using (using coq 0.6) in your dune-project file.
   [1]

test/blackbox-tests/test-cases/coq/no-stdlib.t/bar.v

@@ -0,0 +1 @@
+Definition mynat := nat.

test/blackbox-tests/test-cases/coq/no-stdlib.t/dune

@@ -0,0 +1,5 @@
+(coq.theory
+ (name basic)
+ (package no-stdlib)
+ (stdlib no)
+ (synopsis "Test Coq library"))

test/blackbox-tests/test-cases/coq/no-stdlib.t/dune-project

@@ -0,0 +1,3 @@
+(lang dune 3.5)
+
+(using coq 0.6)

test/blackbox-tests/test-cases/coq/no-stdlib.t/foo.v

@@ -0,0 +1 @@
+From Coq Require Import Prelude.

test/blackbox-tests/test-cases/coq/no-stdlib.t/run.t

@@ -0,0 +1,20 @@
+Test that when `(stdlib no)` is provided, the standard library is not bound to `Coq`
+and the prelude is not imported
+
+  $ dune build --display=short foo.vo
+        coqdep foo.v.d
+  *** Warning: in file foo.v, library Prelude is required from root Coq and has not been found in the loadpath!
+          coqc foo.{glob,vo} (exit 1)
+  File "./foo.v", line 1, characters 0-32:
+  Error: Cannot find a physical path bound to logical path
+  Prelude with prefix Coq.
+
+  [1]
+
+  $ dune build --display=short bar.vo
+        coqdep bar.v.d
+          coqc bar.{glob,vo} (exit 1)
+  File "./bar.v", line 1, characters 20-23:
+  Error: The reference nat was not found in the current environment.
+
+  [1]