From 2d574e4371fa1b5e1e403455ef7e3a370b031b3b Mon Sep 17 00:00:00 2001 From: Lasse Blaauwbroek Date: Tue, 27 Sep 2022 10:23:50 +0200 Subject: [PATCH] Create (stdlib) syntax for Coq stanza Fixes #6163 Co-authored-by: Christine Rose Signed-off-by: Lasse Blaauwbroek --- CHANGES.md | 4 +++ doc/coq.rst | 12 +++++-- src/dune_rules/coq_stanza.ml | 4 ++- .../coq/compose-boot-nostdlib.t/A/a.v | 6 ++++ .../coq/compose-boot-nostdlib.t/A/dune | 4 +++ .../compose-boot-nostdlib.t/A/dune-project | 2 ++ .../coq/compose-boot-nostdlib.t/B/b.v | 4 +++ .../coq/compose-boot-nostdlib.t/B/dune | 4 +++ .../compose-boot-nostdlib.t/B/dune-project | 2 ++ .../coq/compose-boot-nostdlib.t/Coq/Coq.opam | 0 .../Coq/Init/Prelude.v | 2 ++ .../coq/compose-boot-nostdlib.t/Coq/dune | 6 ++++ .../compose-boot-nostdlib.t/Coq/dune-project | 2 ++ .../compose-boot-nostdlib.t/Coq/mytheory.v | 2 ++ .../compose-boot-nostdlib.t/dune-workspace | 1 + .../coq/compose-boot-nostdlib.t/run.t | 36 +++++++++++++++++++ .../test-cases/coq/coqtop-root.t/run.t | 2 +- .../test-cases/coq/github3624.t | 2 +- .../test-cases/coq/no-stdlib.t/bar.v | 1 + .../test-cases/coq/no-stdlib.t/dune | 5 +++ .../test-cases/coq/no-stdlib.t/dune-project | 3 ++ .../test-cases/coq/no-stdlib.t/foo.v | 1 + .../test-cases/coq/no-stdlib.t/no-stdlib.opam | 0 .../test-cases/coq/no-stdlib.t/run.t | 20 +++++++++++ 24 files changed, 120 insertions(+), 5 deletions(-) create mode 100644 test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/A/a.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/A/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/A/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/B/b.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/B/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/B/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/Coq/Coq.opam create mode 100644 test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/Coq/Init/Prelude.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/Coq/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/Coq/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/Coq/mytheory.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/dune-workspace create mode 100644 test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/run.t create mode 100644 test/blackbox-tests/test-cases/coq/no-stdlib.t/bar.v create mode 100644 test/blackbox-tests/test-cases/coq/no-stdlib.t/dune create mode 100644 test/blackbox-tests/test-cases/coq/no-stdlib.t/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/no-stdlib.t/foo.v create mode 100644 test/blackbox-tests/test-cases/coq/no-stdlib.t/no-stdlib.opam create mode 100644 test/blackbox-tests/test-cases/coq/no-stdlib.t/run.t diff --git a/CHANGES.md b/CHANGES.md index d4cf4926083c..5fd00fba71dd 100644 --- a/CHANGES.md +++ b/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) ------------------ diff --git a/doc/coq.rst b/doc/coq.rst index 4035b6cec72b..5ab78adc4e61 100644 --- a/doc/coq.rst +++ b/doc/coq.rst @@ -30,7 +30,7 @@ version` 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` section for more @@ -53,6 +53,7 @@ stanza: (modules ) (plugins ) (flags ) + (stdlib ) (mode ) (theories )) @@ -98,6 +99,11 @@ The semantics of the fields are: is taken from the value set in the ``(coq (flags ))`` field in ``env`` profile. See :ref:`dune-env` for more information. +- ```` 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 ```` 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 )`` is an exhaustive list of OCaml modules extracted. -- ```` are ``flags``, ``theories``, and ``plugins``. All of +- ```` 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 diff --git a/src/dune_rules/coq_stanza.ml b/src/dune_rules/coq_stanza.ml index bfd006fed559..23b07f353271 100644 --- a/src/dune_rules/coq_stanza.ml +++ b/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) diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/A/a.v b/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/A/a.v new file mode 100644 index 000000000000..110ee9e41b42 --- /dev/null +++ b/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. diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/A/dune b/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/A/dune new file mode 100644 index 000000000000..2ea19719d59f --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/A/dune @@ -0,0 +1,4 @@ +(coq.theory + (name A) + (stdlib no) + (theories Coq)) diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/A/dune-project b/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/A/dune-project new file mode 100644 index 000000000000..4dad2a1c9b97 --- /dev/null +++ b/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) diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/B/b.v b/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/B/b.v new file mode 100644 index 000000000000..3d8121dab096 --- /dev/null +++ b/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. diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/B/dune b/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/B/dune new file mode 100644 index 000000000000..094a2674eda6 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/B/dune @@ -0,0 +1,4 @@ +(coq.theory + (name B) + (stdlib yes) + (theories Coq)) diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/B/dune-project b/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/B/dune-project new file mode 100644 index 000000000000..4dad2a1c9b97 --- /dev/null +++ b/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) diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/Coq/Coq.opam b/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/Coq/Coq.opam new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/Coq/Init/Prelude.v b/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/Coq/Init/Prelude.v new file mode 100644 index 000000000000..9de480a5ab81 --- /dev/null +++ b/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. diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/Coq/dune b/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/Coq/dune new file mode 100644 index 000000000000..323f2d22b4b7 --- /dev/null +++ b/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) diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/Coq/dune-project b/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/Coq/dune-project new file mode 100644 index 000000000000..05af5ca5dce3 --- /dev/null +++ b/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) diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/Coq/mytheory.v b/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/Coq/mytheory.v new file mode 100644 index 000000000000..831752c569d8 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/Coq/mytheory.v @@ -0,0 +1,2 @@ + +Inductive Hello := World | Bye. diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/dune-workspace b/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/dune-workspace new file mode 100644 index 000000000000..7b17fb2d3089 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/dune-workspace @@ -0,0 +1 @@ +(lang dune 3.3) diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/run.t b/test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/run.t new file mode 100644 index 000000000000..7fb935fb72e4 --- /dev/null +++ b/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 diff --git a/test/blackbox-tests/test-cases/coq/coqtop-root.t/run.t b/test/blackbox-tests/test-cases/coq/coqtop-root.t/run.t index 60f0ce511dea..3c485e53732c 100644 --- a/test/blackbox-tests/test-cases/coq/coqtop-root.t/run.t +++ b/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] diff --git a/test/blackbox-tests/test-cases/coq/github3624.t b/test/blackbox-tests/test-cases/coq/github3624.t index 8a95533a1dc8..42fd0c8af465 100644 --- a/test/blackbox-tests/test-cases/coq/github3624.t +++ b/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] diff --git a/test/blackbox-tests/test-cases/coq/no-stdlib.t/bar.v b/test/blackbox-tests/test-cases/coq/no-stdlib.t/bar.v new file mode 100644 index 000000000000..53e0ce1b1526 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/no-stdlib.t/bar.v @@ -0,0 +1 @@ +Definition mynat := nat. diff --git a/test/blackbox-tests/test-cases/coq/no-stdlib.t/dune b/test/blackbox-tests/test-cases/coq/no-stdlib.t/dune new file mode 100644 index 000000000000..5e049f634ad4 --- /dev/null +++ b/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")) diff --git a/test/blackbox-tests/test-cases/coq/no-stdlib.t/dune-project b/test/blackbox-tests/test-cases/coq/no-stdlib.t/dune-project new file mode 100644 index 000000000000..4effa102dde5 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/no-stdlib.t/dune-project @@ -0,0 +1,3 @@ +(lang dune 3.5) + +(using coq 0.6) diff --git a/test/blackbox-tests/test-cases/coq/no-stdlib.t/foo.v b/test/blackbox-tests/test-cases/coq/no-stdlib.t/foo.v new file mode 100644 index 000000000000..4e944c79f70e --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/no-stdlib.t/foo.v @@ -0,0 +1 @@ +From Coq Require Import Prelude. diff --git a/test/blackbox-tests/test-cases/coq/no-stdlib.t/no-stdlib.opam b/test/blackbox-tests/test-cases/coq/no-stdlib.t/no-stdlib.opam new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/test/blackbox-tests/test-cases/coq/no-stdlib.t/run.t b/test/blackbox-tests/test-cases/coq/no-stdlib.t/run.t new file mode 100644 index 000000000000..15144d49c6fe --- /dev/null +++ b/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]