From 4d4a3fc4c2fba08d828aff94d08b30d78e6b37ea Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 26 May 2022 16:47:15 +0100 Subject: [PATCH] feature(coq): support for interproject composition of theories Co-authored-by: Rudi Grinberg Signed-off-by: Ali Caglayan --- bin/coqtop.ml | 1 + bin/import.ml | 1 + doc/coq.rst | 148 +++++- src/dune_rules/coq_lib.ml | 462 +++++++++++++----- src/dune_rules/coq_lib.mli | 49 +- src/dune_rules/coq_lib_name.ml | 2 + src/dune_rules/coq_lib_name.mli | 2 + src/dune_rules/coq_rules.ml | 133 +++-- src/dune_rules/coq_rules.mli | 2 +- src/dune_rules/coq_stanza.ml | 8 +- src/dune_rules/coq_stanza.mli | 1 + src/dune_rules/scope.ml | 102 ++-- .../compose-boot.t/{cboot.opam => A/A.opam} | 0 .../test-cases/coq/compose-boot.t/A/a.v | 1 + .../test-cases/coq/compose-boot.t/A/dune | 4 + .../coq/compose-boot.t/{ => A}/dune-project | 0 .../ccycle.opam => compose-boot.t/B/B.opam} | 0 .../test-cases/coq/compose-boot.t/B/b.v | 1 + .../test-cases/coq/compose-boot.t/B/dune | 6 + .../coq/compose-boot.t/B/dune-project | 3 + .../coq/compose-boot.t/boot/Init/Prelude.v | 1 - .../test-cases/coq/compose-boot.t/dune | 3 - .../coq/compose-boot.t/dune-workspace | 1 + .../test-cases/coq/compose-boot.t/run.t | 9 +- .../test-cases/coq/compose-boot.t/user/dune | 5 - .../test-cases/coq/compose-boot.t/user/user.v | 1 - .../coq/compose-cycle.t/{a => A}/a.v | 0 .../test-cases/coq/compose-cycle.t/A/dune | 3 + .../coq/compose-cycle.t/{b => B}/b.v | 0 .../test-cases/coq/compose-cycle.t/B/dune | 3 + .../test-cases/coq/compose-cycle.t/a/dune | 4 - .../test-cases/coq/compose-cycle.t/b/dune | 4 - .../test-cases/coq/compose-cycle.t/dune | 3 - .../coq/compose-cycle.t/dune-project | 5 +- .../test-cases/coq/compose-cycle.t/run.t | 37 +- .../test-cases/coq/compose-installed.t/A/a.v | 2 + .../test-cases/coq/compose-installed.t/A/dune | 3 + .../coq/compose-installed.t/A/dune-project | 2 + .../test-cases/coq/compose-installed.t/run.t | 20 + .../compose-installed.t/user-contrib/B/b.v | 3 + .../A/A.opam} | 0 .../coq/compose-private-ambiguous.t/A/a.v | 3 + .../coq/compose-private-ambiguous.t/A/dune | 3 + .../A_vendored/A.opam} | 0 .../A_vendored/a.v | 3 + .../A_vendored/dune | 4 + .../A_vendored/dune-project | 2 + .../coq/compose-private-ambiguous.t/B/b.v | 7 + .../coq/compose-private-ambiguous.t/B/dune | 3 + .../coq/compose-private-ambiguous.t/C.opam | 0 .../coq/compose-private-ambiguous.t/C/c.v | 7 + .../coq/compose-private-ambiguous.t/C/dune | 6 + .../compose-private-ambiguous.t/dune-project | 2 + .../coq/compose-private-ambiguous.t/run.t | 16 + .../test-cases/coq/compose-private.t/A/A.opam | 0 .../test-cases/coq/compose-private.t/A/a.v | 2 + .../test-cases/coq/compose-private.t/A/dune | 3 + .../test-cases/coq/compose-private.t/B/b.v | 4 + .../test-cases/coq/compose-private.t/B/dune | 3 + .../test-cases/coq/compose-private.t/C.opam | 0 .../test-cases/coq/compose-private.t/C/c.v | 0 .../test-cases/coq/compose-private.t/C/dune | 4 + .../coq/compose-private.t/dune-project | 2 + .../test-cases/coq/compose-private.t/run.t | 13 + .../coq/compose-projects-boot.t/A/a.v | 10 + .../coq/compose-projects-boot.t/A/dune | 3 + .../compose-projects-boot.t/A/dune-project | 2 + .../B/Coq/Init/Prelude.v | 2 + .../coq/compose-projects-boot.t/B/Foo.opam | 0 .../coq/compose-projects-boot.t/B/Stuff/b.v | 1 + .../coq/compose-projects-boot.t/B/Stuff/dune | 3 + .../compose-projects-boot.t/B/dune-project | 2 + .../coq/compose-projects-boot.t/Coq/Coq.opam | 0 .../Coq/Init/Prelude.v | 2 + .../boot => compose-projects-boot.t/Coq}/dune | 3 +- .../compose-projects-boot.t/Coq/dune-project | 2 + .../compose-projects-boot.t/Coq/mytheory.v | 2 + .../compose-projects-boot.t/dune-workspace | 1 + .../coq/compose-projects-boot.t/run.t | 53 ++ .../coq/compose-projects-cycle.t/A/A.opam | 0 .../coq/compose-projects-cycle.t/A/a.v | 3 + .../coq/compose-projects-cycle.t/A/dune | 5 + .../compose-projects-cycle.t/A/dune-project | 2 + .../coq/compose-projects-cycle.t/B/B.opam | 0 .../coq/compose-projects-cycle.t/B/b.v | 4 + .../coq/compose-projects-cycle.t/B/dune | 4 + .../compose-projects-cycle.t/B/dune-project | 2 + .../coq/compose-projects-cycle.t/C/C.opam | 0 .../coq/compose-projects-cycle.t/C/c.v | 1 + .../coq/compose-projects-cycle.t/C/dune | 4 + .../compose-projects-cycle.t/C/dune-project | 2 + .../compose-projects-cycle.t/dune-workspace | 1 + .../coq/compose-projects-cycle.t/run.t | 38 ++ .../coq/compose-projects-missing.t/A/A.opam | 0 .../coq/compose-projects-missing.t/A/a.v | 2 + .../coq/compose-projects-missing.t/A/dune | 3 + .../compose-projects-missing.t/A/dune-project | 2 + .../coq/compose-projects-missing.t/B/B.opam | 0 .../coq/compose-projects-missing.t/B/b.v | 4 + .../coq/compose-projects-missing.t/B/dune | 4 + .../compose-projects-missing.t/B/dune-project | 2 + .../coq/compose-projects-missing.t/C/C.opam | 0 .../coq/compose-projects-missing.t/C/c.v | 2 + .../coq/compose-projects-missing.t/C/dune | 4 + .../compose-projects-missing.t/C/dune-project | 2 + .../compose-projects-missing.t/dune-workspace | 1 + .../coq/compose-projects-missing.t/run.t | 15 + .../coq/compose-projects.t/A/A.opam | 0 .../test-cases/coq/compose-projects.t/A/a.v | 2 + .../test-cases/coq/compose-projects.t/A/dune | 4 + .../coq/compose-projects.t/A/dune-project | 2 + .../test-cases/coq/compose-projects.t/B/b.v | 4 + .../test-cases/coq/compose-projects.t/B/dune | 3 + .../coq/compose-projects.t/B/dune-project | 2 + .../coq/compose-projects.t/dune-workspace | 1 + .../test-cases/coq/compose-projects.t/run.t | 10 + .../test-cases/coq/compose-self.t/A/a.v | 0 .../test-cases/coq/compose-self.t/A/dune | 3 + .../coq/compose-self.t/dune-project | 2 + .../test-cases/coq/compose-self.t/run.t | 9 + .../coq/compose-simple.t/{a => A}/a.v | 0 .../test-cases/coq/compose-simple.t/A/dune | 3 + .../coq/compose-simple.t/{b => B}/b.v | 2 +- .../test-cases/coq/compose-simple.t/B/dune | 4 + .../coq/compose-simple.t/Simple.opam | 0 .../test-cases/coq/compose-simple.t/a/dune | 3 - .../test-cases/coq/compose-simple.t/b/dune | 4 - .../test-cases/coq/compose-simple.t/dune | 3 - .../coq/compose-simple.t/dune-project | 5 +- .../test-cases/coq/compose-simple.t/run.t | 31 +- .../coq/compose-sub-theory.t/{a => A}/a.v | 0 .../coq/compose-sub-theory.t/A/dune | 3 + .../test-cases/coq/compose-sub-theory.t/B/b.v | 3 + .../coq/compose-sub-theory.t/B/dune | 4 + .../coq/compose-sub-theory.t/Subtheory.opam | 0 .../coq/compose-sub-theory.t/a/dune | 3 - .../test-cases/coq/compose-sub-theory.t/b/b.v | 3 - .../coq/compose-sub-theory.t/b/dune | 4 - .../test-cases/coq/compose-sub-theory.t/dune | 3 - .../coq/compose-sub-theory.t/dune-project | 4 +- .../test-cases/coq/compose-sub-theory.t/run.t | 30 +- .../coq/compose-two-scopes.t/dune-project | 5 +- .../test-cases/coq/compose-two-scopes.t/run.t | 23 +- .../test-cases/coq/github3624.t | 2 +- .../coq/public-dep-on-private.t/run.t | 5 +- 145 files changed, 1137 insertions(+), 367 deletions(-) rename test/blackbox-tests/test-cases/coq/compose-boot.t/{cboot.opam => A/A.opam} (100%) create mode 100644 test/blackbox-tests/test-cases/coq/compose-boot.t/A/a.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-boot.t/A/dune rename test/blackbox-tests/test-cases/coq/compose-boot.t/{ => A}/dune-project (100%) rename test/blackbox-tests/test-cases/coq/{compose-cycle.t/ccycle.opam => compose-boot.t/B/B.opam} (100%) create mode 100644 test/blackbox-tests/test-cases/coq/compose-boot.t/B/b.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-boot.t/B/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-boot.t/B/dune-project delete mode 100644 test/blackbox-tests/test-cases/coq/compose-boot.t/boot/Init/Prelude.v delete mode 100644 test/blackbox-tests/test-cases/coq/compose-boot.t/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-boot.t/dune-workspace delete mode 100644 test/blackbox-tests/test-cases/coq/compose-boot.t/user/dune delete mode 100644 test/blackbox-tests/test-cases/coq/compose-boot.t/user/user.v rename test/blackbox-tests/test-cases/coq/compose-cycle.t/{a => A}/a.v (100%) create mode 100644 test/blackbox-tests/test-cases/coq/compose-cycle.t/A/dune rename test/blackbox-tests/test-cases/coq/compose-cycle.t/{b => B}/b.v (100%) create mode 100644 test/blackbox-tests/test-cases/coq/compose-cycle.t/B/dune delete mode 100644 test/blackbox-tests/test-cases/coq/compose-cycle.t/a/dune delete mode 100644 test/blackbox-tests/test-cases/coq/compose-cycle.t/b/dune delete mode 100644 test/blackbox-tests/test-cases/coq/compose-cycle.t/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-installed.t/A/a.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-installed.t/A/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-installed.t/A/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/compose-installed.t/run.t create mode 100644 test/blackbox-tests/test-cases/coq/compose-installed.t/user-contrib/B/b.v rename test/blackbox-tests/test-cases/coq/{compose-simple.t/csimple.opam => compose-private-ambiguous.t/A/A.opam} (100%) create mode 100644 test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A/a.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A/dune rename test/blackbox-tests/test-cases/coq/{compose-sub-theory.t/subtheory.opam => compose-private-ambiguous.t/A_vendored/A.opam} (100%) create mode 100644 test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A_vendored/a.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A_vendored/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A_vendored/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/B/b.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/B/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/C.opam create mode 100644 test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/C/c.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/C/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/run.t create mode 100644 test/blackbox-tests/test-cases/coq/compose-private.t/A/A.opam create mode 100644 test/blackbox-tests/test-cases/coq/compose-private.t/A/a.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-private.t/A/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-private.t/B/b.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-private.t/B/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-private.t/C.opam create mode 100644 test/blackbox-tests/test-cases/coq/compose-private.t/C/c.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-private.t/C/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-private.t/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/compose-private.t/run.t create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-boot.t/A/a.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-boot.t/A/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-boot.t/A/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-boot.t/B/Coq/Init/Prelude.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-boot.t/B/Foo.opam create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-boot.t/B/Stuff/b.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-boot.t/B/Stuff/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-boot.t/B/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-boot.t/Coq/Coq.opam create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-boot.t/Coq/Init/Prelude.v rename test/blackbox-tests/test-cases/coq/{compose-boot.t/boot => compose-projects-boot.t/Coq}/dune (77%) create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-boot.t/Coq/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-boot.t/Coq/mytheory.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-boot.t/dune-workspace create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-boot.t/run.t create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/A/A.opam create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/A/a.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/A/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/A/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/B/B.opam create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/B/b.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/B/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/B/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/C/C.opam create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/C/c.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/C/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/C/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/dune-workspace create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/run.t create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-missing.t/A/A.opam create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-missing.t/A/a.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-missing.t/A/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-missing.t/A/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-missing.t/B/B.opam create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-missing.t/B/b.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-missing.t/B/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-missing.t/B/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-missing.t/C/C.opam create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-missing.t/C/c.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-missing.t/C/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-missing.t/C/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-missing.t/dune-workspace create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects-missing.t/run.t create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects.t/A/A.opam create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects.t/A/a.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects.t/A/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects.t/A/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects.t/B/b.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects.t/B/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects.t/B/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects.t/dune-workspace create mode 100644 test/blackbox-tests/test-cases/coq/compose-projects.t/run.t create mode 100644 test/blackbox-tests/test-cases/coq/compose-self.t/A/a.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-self.t/A/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-self.t/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/compose-self.t/run.t rename test/blackbox-tests/test-cases/coq/compose-simple.t/{a => A}/a.v (100%) create mode 100644 test/blackbox-tests/test-cases/coq/compose-simple.t/A/dune rename test/blackbox-tests/test-cases/coq/compose-simple.t/{b => B}/b.v (50%) create mode 100644 test/blackbox-tests/test-cases/coq/compose-simple.t/B/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-simple.t/Simple.opam delete mode 100644 test/blackbox-tests/test-cases/coq/compose-simple.t/a/dune delete mode 100644 test/blackbox-tests/test-cases/coq/compose-simple.t/b/dune delete mode 100644 test/blackbox-tests/test-cases/coq/compose-simple.t/dune rename test/blackbox-tests/test-cases/coq/compose-sub-theory.t/{a => A}/a.v (100%) create mode 100644 test/blackbox-tests/test-cases/coq/compose-sub-theory.t/A/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-sub-theory.t/B/b.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-sub-theory.t/B/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-sub-theory.t/Subtheory.opam delete mode 100644 test/blackbox-tests/test-cases/coq/compose-sub-theory.t/a/dune delete mode 100644 test/blackbox-tests/test-cases/coq/compose-sub-theory.t/b/b.v delete mode 100644 test/blackbox-tests/test-cases/coq/compose-sub-theory.t/b/dune delete mode 100644 test/blackbox-tests/test-cases/coq/compose-sub-theory.t/dune diff --git a/bin/coqtop.ml b/bin/coqtop.ml index b836bfe2c0c7..76219bc1c707 100644 --- a/bin/coqtop.ml +++ b/bin/coqtop.ml @@ -96,6 +96,7 @@ let term = in let* (_ : unit * Dep.Fact.t Dep.Map.t) = let deps = + let boot_type = Resolve.Memo.return boot_type in Dune_rules.Coq_rules.deps_of ~dir ~boot_type coq_module in Action_builder.run deps Eager diff --git a/bin/import.ml b/bin/import.ml index 2bbf30502f29..238bedd51f4f 100644 --- a/bin/import.ml +++ b/bin/import.ml @@ -28,6 +28,7 @@ module Workspace = Dune_rules.Workspace module Cached_digest = Dune_engine.Cached_digest module Targets = Dune_engine.Targets module Profile = Dune_rules.Profile +module Resolve = Dune_rules.Resolve module Log = Dune_util.Log module Dune_rpc = Dune_rpc_private module Graph = Dune_graph.Graph diff --git a/doc/coq.rst b/doc/coq.rst index d69333ec78ba..32abfa2cd3dd 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.3) + (using coq 0.4) 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 @@ -67,12 +67,12 @@ The semantics of the fields are: - ```` is a dot-separated list of valid Coq module names and determines the module scope under which the theory is compiled (this corresponds to Coq's ``-R`` option). - + For example, if ```` is ``foo.Bar``, the theory modules are named ``foo.Bar.module1``, ``foo.Bar.module2``, etc. Note that modules in the same theory don't see the ``foo.Bar`` prefix in the same way that OCaml ``wrapped`` libraries do. - + For compatibility, :ref:`Coq lang 1.0` installs a theory named ``foo.Bar`` under ``foo/Bar``. Also note that Coq supports composing a module path from different theories, thus you can name a theory ``foo.Bar`` and a @@ -85,12 +85,12 @@ The semantics of the fields are: - If ``package`` is present, Dune generates install rules for the ``.vo`` files of the theory. ``pkg_name`` must be a valid package name. - + Note that :ref:`Coq lang 1.0` will use the Coq legacy install setup, where all packages share a common root namespace and install directory, ``lib/coq/user-contrib/``, as is customary in the Make-based Coq package ecosystem. - + For compatibility, Dune also installs, under the ``user-contrib`` prefix, the ``.cmxs`` files that appear in ````. @@ -105,12 +105,30 @@ The semantics of the fields are: - Your Coq theory can depend on other theories by specifying them in the ```` field. Dune then passes to Coq the corresponding flags for everything to compile correctly (this corresponds to the ``-Q`` flag for Coq). + + You may also depend on theories belonging to another :ref:`dune-project` as + long as they share a common scope under another :ref:`dune-project` file or a + :ref:`dune-workspace` file. + + Doing so can be as simple as placing a Coq project within the scope of + another. This process is termed *composition*. See the :ref:`interproject + composition` example. - As of today, we only support composition with libraries defined in the same - scope (i.e., under the same :ref:`dune-project` domain). This restriction will - be lifted in the future. Note that composition with the Coq standard library - is supported, but in this case the ``Coq`` prefix has been made available in a - qualified way, since :ref:`Coq lang 0.2`. + Interproject composition allows for a fine granularity of dependencies. In + practice, this means that Dune will only build the parts of a dependency that + are needed. This means that building a project depending on another will not + trigger a rebuild of the whole of the latter. + + Interproject composition has been available since :ref:`Coq lang + 0.4`. + + As of today, Dune cannot depend on installed Coq theories. This restriction + will be lifted in the future. Note that composition with the Coq standard + library is supported, but in this case the ``Coq`` prefix has been made + available in a qualified way, since :ref:`Coq lang 0.2`. + + You may still use installed libraries in your Coq project, but there is + currently no way for Dune to know about it. - You can enable the production of Coq's native compiler object files by setting ```` to ``native``. This passes ``-native-compiler on`` to @@ -142,6 +160,33 @@ directory and its subdirectories, adding a prefix to the module name in the usual Coq style for subdirectories. For example, file ``A/b/C.v`` becomes the module ``A.b.C``. +.. _public-private-theory: + +Public and Private Theories +~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +A *public theory* is a :ref:`coq-theory` stanza that is visible outside the +scope of a :ref:`dune-project` file. + +A *private theory* is a :ref:`coq-theory` stanza that is limited to the scope of +the :ref:`dune-project` file it is in. + +A private theory may depend on both private and public theories; however, a +public theory may only depend on other public theories. + +By default, all :ref:`coq-theory` stanzas are considered private by Dune. In +order to make a private theory into a public theory, the ``(package )`` field +must be specified. + +.. code:: scheme + + (coq.theory + (name private_theory)) + + (coq.theory + (name private_theory) + (package coq-public-theory)) + Limitations ~~~~~~~~~~~ @@ -168,15 +213,16 @@ file: .. code:: scheme - (using coq 0.3) + (using coq 0.4) The supported Coq language versions (not the version of Coq) are: - ``0.1``: Basic Coq theory support. - ``0.2``: Support for the ``theories`` field and composition of theories in the - same scope, + same scope. - ``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. .. _coq-lang-1.0: @@ -255,21 +301,21 @@ Here we list some examples of some basic Coq project setups in order. .. _example-simple: -Simple Coq Project -~~~~~~~~~~~~~~~~~~ +Simple Project +~~~~~~~~~~~~~~ -Let us start with a simple project. First we make sure we have a +Let us start with a simple project. First, make sure we have a :ref:`dune-project` file with a :ref:`Coq lang` stanza present: .. code:: scheme (lang dune 3.3) - (using coq 0.3) + (using coq 0.4) Next we need a :ref:`dune` file with a :ref:`coq-theory` stanza: .. code:: scheme - + (coq.theory (name myTheory)) @@ -336,12 +382,12 @@ Here are the :ref:`dune` files: Notice the ``theories`` field in ``B`` allows one :ref:`coq-theory` to depend on another. Another thing to note is the inclusion of the :ref:`include_subdirs` stanza. This allows our theory to have :ref:`multiple -subdirectories`. +subdirectories`. Here are the contents of the ``.v`` files: .. code:: coq - + (* A/AA/aa.v is empty *) (* A/AB/ab.v *) @@ -354,6 +400,70 @@ This causes a dependency chain ``b.v -> ab.v -> aa.v``. Now we might be interested in building theory ``B``, so all we have to do is run ``dune build B``. Dune will automatically build the theory ``A`` since it is a dependency. +.. _example-interproject-theory: + +Composing Projects +~~~~~~~~~~~~~~~~~~ + +To demonstrate the composition of Coq projects, we can take our previous two +examples and put them in project which has a theory that depends on theories in +both projects. + +.. code:: + + . + ├── CombinedWork + │ ├── comb.v + │ └── dune + ├── DeeperTheory + │ ├── A + │ │ ├── AA + │ │ │ └── aa.v + │ │ ├── AB + │ │ │ └── ab.v + │ │ └── dune + │ ├── B + │ │ ├── b.v + │ │ └── dune + │ ├── Deep.opam + │ └── dune-project + ├── dune-project + └── SimpleTheory + ├── A.v + ├── dune + ├── dune-project + └── Simple.opam + +The file ``comb.v`` looks like: + +.. code:: coq + + (* Files from DeeperTheory *) + From A.AA Require Import aa. + (* In Coq, partial prefixes for theory names are enough *) + From A Require Import ab. + From B Require Import b. + + (* Files from SimpleTheory *) + From myTheory Require Import A. + +We are referencing Coq modules from all three of our previously defined +theories. + +Our :ref:`dune` file in ``CombinedWork`` looks like: + +.. code:: scheme + + (coq.theory + (name Combined) + (theories myTheory A B)) + +As you can see, there are dependencies on all the theories we mentioned. + +All three of the theories we defined before were *private theories*. In order to +depend on them, we needed to make them *public theories*. See the section on +:ref:`public-private-theory`. + .. _running-coq-top: Running a Coq Toplevel diff --git a/src/dune_rules/coq_lib.ml b/src/dune_rules/coq_lib.ml index 5a7155ecae6c..c3eb5a75ddbe 100644 --- a/src/dune_rules/coq_lib.ml +++ b/src/dune_rules/coq_lib.ml @@ -5,30 +5,59 @@ open Import (* (c) INRIA 2020 *) (* Written by: Emilio Jesús Gallego Arias *) -(* At some point we may want to reify this into resolved status, for example: +module Id = struct + module T = struct + type t = + { path : Path.Build.t + ; name : Coq_lib_name.t + } - ; libraries : Lib.t list Or_exn.t + let compare t { path; name } = + let open Ordering.O in + let= () = Path.Build.compare t.path path in + Coq_lib_name.compare t.name name + + let to_dyn { path; name } = + Dyn.( + record + [ ("path", Path.Build.to_dyn path) + ; ("name", Coq_lib_name.to_dyn name) + ]) + end + + include T + + let pp { path; name } = + Pp.concat ~sep:Pp.space + [ Pp.textf "theory %s in" (Coq_lib_name.to_string name) + ; Path.pp (Path.build path) + ] + + let create ~path ~name = { path; name } + + module C = Comparable.Make (T) + module Top_closure = Top_closure.Make (C.Set) (Resolve) + + let top_closure ~key ~deps xs = Top_closure.top_closure ~key ~deps xs +end - etc.. *) type t = - { name : Loc.t * Coq_lib_name.t - ; wrapper : string + { loc : Loc.t + ; boot : t option Resolve.t + ; id : Id.t ; implicit : bool (* Only useful for the stdlib *) ; src_root : Path.Build.t ; obj_root : Path.Build.t - ; theories : (Loc.t * Coq_lib_name.t) list - ; libraries : (Loc.t * Lib_name.t) list + ; theories : (Loc.t * t) list Resolve.t + ; libraries : (Loc.t * Lib.t) list Resolve.t + ; theories_closure : t list Resolve.t Lazy.t ; package : Package.t option } -let name l = snd l.name +let name l = l.id.name let implicit l = l.implicit -let location l = fst l.name - -let wrapper l = l.wrapper - let src_root l = l.src_root let obj_root l = l.obj_root @@ -38,128 +67,333 @@ let libraries l = l.libraries let package l = l.package module Error = struct - let make ?loc ?hints paragraphs = - Error (User_error.E (User_error.make ?loc ?hints paragraphs)) + let annots = + User_message.Annots.singleton User_message.Annots.needs_stack_trace () - let duplicate_theory_name theory = - let loc, name = theory.Coq_stanza.Theory.name in + let duplicate_theory_name (loc, name) = let name = Coq_lib_name.to_string name in - make ~loc [ Pp.textf "Duplicate theory name: %s" name ] + User_error.raise ~loc [ Pp.textf "Duplicate theory name: %s" name ] + + let incompatible_boot id id' = + let pp_lib (id : Id.t) = Pp.seq (Pp.text "- ") (Id.pp id) in + User_message.make ~annots + [ Pp.textf "The following theories use incompatible boot libraries" + ; pp_lib id' + ; pp_lib id + ] + |> Resolve.fail let theory_not_found ~loc name = let name = Coq_lib_name.to_string name in - make ~loc [ Pp.textf "Theory %s not found" name ] - - let private_deps_not_allowed ~loc private_dep = - let name = Coq_lib_name.to_string (name private_dep) in - make ~loc - [ Pp.textf - "Theory %S is private, it cannot be a dependency of a public theory. \ - You need to associate %S to a package." - name name - ] + Resolve.Memo.fail + @@ User_message.make ~annots ~loc [ Pp.textf "Theory %s not found" name ] - let duplicate_boot_lib ~loc boot_theory = - let name = - Coq_lib_name.to_string (snd boot_theory.Coq_stanza.Theory.name) - in - make ~loc [ Pp.textf "Cannot have more than one boot library: %s)" name ] + let hidden_without_composition ~loc name = + let name = Coq_lib_name.to_string name in + Resolve.Memo.fail + @@ User_message.make ~annots ~loc + [ Pp.textf + "Theory %s not found in the current scope. Upgrade coq lang to \ + 0.4 to enable scope composition." + name + ] + + let private_deps_not_allowed ~loc name = + let name = Coq_lib_name.to_string name in + Resolve.Memo.fail + @@ User_message.make ~loc + [ Pp.textf + "Theory %S is private, it cannot be a dependency of a public \ + theory. You need to associate %S to a package." + name name + ] - let cycle_found ~loc cycle = - make ~loc - [ Pp.textf "Cycle found" - ; Pp.enumerate cycle ~f:(fun t -> - Pp.text (Coq_lib_name.to_string (snd t.name))) + let duplicate_boot_lib theories = + let open Coq_stanza.Theory in + let name (t : Coq_stanza.Theory.t) = + let name = Coq_lib_name.to_string (snd t.name) in + Pp.textf "%s at %s" name (Loc.to_file_colon_line t.buildable.loc) + in + User_error.raise + [ Pp.textf "Cannot have more than one boot theory in scope:" + ; Pp.enumerate theories ~f:name ] end +let top_closure = + let key t = t.id in + let deps t = t.theories |> Resolve.map ~f:(List.map ~f:snd) in + fun theories -> + let open Resolve.O in + Id.top_closure theories ~key ~deps >>= function + | Ok s -> Resolve.return s + | Error _ -> assert false + module DB = struct type lib = t - type nonrec t = - { boot : (Loc.t * t) option - ; libs : t Coq_lib_name.Map.t + type entry = + | Theory of Path.Build.t + | Redirect of t + + and t = + { parent : t option + ; resolve : + Coq_lib_name.t + -> [ `Redirect of t + | `Theory of Lib.DB.t * Path.Build.t * Coq_stanza.Theory.t + | `Not_found + ] + ; boot : (Loc.t * lib Resolve.t Memo.Lazy.t) option } - let boot_library { boot; _ } = boot - - let create_from_stanza ((dir, s) : Path.Build.t * Coq_stanza.Theory.t) = - let name = snd s.name in - ( name - , { name = s.name - ; wrapper = Coq_lib_name.wrapper name - ; implicit = s.boot - ; obj_root = dir - ; src_root = dir - ; theories = s.buildable.theories - ; libraries = s.buildable.libraries - ; package = s.package - } ) + module rec R : sig + val resolve : + t + -> coq_lang_version:Dune_sexp.Syntax.Version.t + -> Loc.t * Coq_lib_name.t + -> lib Resolve.Memo.t + end = struct + open R + + let rec boot coq_db = + match coq_db.boot with + | Some (_, boot) -> + Memo.Lazy.force boot |> Resolve.Memo.map ~f:Option.some + | None -> ( + match coq_db.parent with + | None -> Resolve.Memo.return None + | Some parent -> boot parent) + + let create_from_stanza = + let create_from_stanza_impl (coq_db, db, dir, (s : Coq_stanza.Theory.t)) = + let id = Id.create ~path:dir ~name:(snd s.name) in + let coq_lang_version = s.buildable.coq_lang_version in + let open Memo.O in + let* boot = if s.boot then Resolve.Memo.return None else boot coq_db in + let allow_private_deps = Option.is_none s.package in + let+ libraries = + Resolve.Memo.List.map s.buildable.libraries ~f:(fun (loc, lib) -> + let open Resolve.Memo.O in + let* lib = Lib.DB.resolve db (loc, lib) in + let+ () = + Resolve.Memo.lift + @@ + if allow_private_deps then Resolve.return () + else + match + let info = Lib.info lib in + let status = Lib_info.status info in + Lib_info.Status.is_private status + with + | false -> Resolve.return () + | true -> + Resolve.fail + @@ User_message.make ~loc + [ Pp.textf + "private theory %s may not depend on a public \ + library" + (Coq_lib_name.to_string (snd s.name)) + ] + in + (loc, lib)) + and+ theories = + let check_boot (lib : lib) = + let open Resolve.O in + let* boot = boot in + match boot with + | None -> Resolve.return () + | Some boot -> ( + let* boot' = lib.boot in + match boot' with + | None -> Resolve.return () + | Some boot' -> ( + match Id.compare boot.id boot'.id with + | Eq -> Resolve.return () + | _ -> Error.incompatible_boot lib.id id)) + in + Resolve.Memo.List.map s.buildable.theories ~f:(fun (loc, theory) -> + let open Resolve.Memo.O in + let* theory = resolve ~coq_lang_version coq_db (loc, theory) in + let* () = Resolve.Memo.lift @@ check_boot theory in + let+ () = + if allow_private_deps then Resolve.Memo.return () + else + match theory.package with + | Some _ -> Resolve.Memo.return () + | None -> Error.private_deps_not_allowed ~loc theory.id.name + in + + (loc, theory)) + in + let theories = + let open Resolve.O in + let* boot = boot in + match boot with + | None -> theories + | Some boot -> + let+ theories = theories in + (* TODO: if lib is boot, don't add boot dep *) + (* maybe use the loc for boot? *) + (Loc.none, boot) :: theories + in + let map_error x = + let human_readable_description () = Id.pp id in + Resolve.push_stack_frame ~human_readable_description x + in + let theories = map_error theories in + let libraries = map_error libraries in + + { loc = fst s.name + ; boot + ; id + ; implicit = s.boot + ; obj_root = dir + ; src_root = dir + ; theories + ; libraries + ; theories_closure = + lazy + (Resolve.bind theories ~f:(fun theories -> + List.map theories ~f:snd |> top_closure)) + ; package = s.package + } + in + let module Input = struct + type nonrec t = t * Lib.DB.t * Path.Build.t * Coq_stanza.Theory.t + + let equal (coq_db, ml_db, path, stanza) (coq_db', ml_db', path', stanza') + = + coq_db == coq_db' && ml_db == ml_db' + && Path.Build.equal path path' + && stanza == stanza' + + let hash = Poly.hash + + let to_dyn = Dyn.opaque + end in + let memo = + Memo.create "create-from-stanza" + ~human_readable_description:(fun (_, _, path, theory) -> + Id.pp (Id.create ~path ~name:(snd theory.name))) + ~input:(module Input) + create_from_stanza_impl + in + fun coq_db db dir stanza -> Memo.exec memo (coq_db, db, dir, stanza) + + let rec find coq_db (loc, name) = + match coq_db.resolve name with + | `Theory (db, dir, stanza) -> Some (db, dir, stanza) + | `Redirect coq_db -> find coq_db (loc, name) + | `Not_found -> ( + match coq_db.parent with + | None -> None + | Some parent -> find parent (loc, name)) + + let find coq_db ~coq_lang_version (loc, name) = + match find coq_db (loc, name) with + | None -> `Not_found + | Some (mldb, dir, stanza) when coq_lang_version >= (0, 4) -> + `Found (mldb, dir, stanza) + | Some (mldb, dir, stanza) -> ( + match coq_db.resolve name with + | `Not_found -> `Hidden + | `Theory _ | `Redirect _ -> `Found (mldb, dir, stanza)) + + let resolve coq_db ~coq_lang_version (loc, name) = + match find coq_db ~coq_lang_version (loc, name) with + | `Not_found -> Error.theory_not_found ~loc name + | `Hidden -> Error.hidden_without_composition ~loc name + | `Found (db, dir, stanza) -> + let open Memo.O in + let+ theory = create_from_stanza coq_db db dir stanza in + let open Resolve.O in + let* (_ : (Loc.t * Lib.t) list) = theory.libraries in + let+ (_ : (Loc.t * lib) list) = theory.theories in + theory + end + + open R + + let rec boot_library_finder t = + match t.boot with + | None -> ( + match t.parent with + | None -> None + | Some parent -> boot_library_finder parent) + | Some (loc, lib) -> Some (loc, lib) + + let boot_library t = + (* Check if a database and its parents have the boot flag *) + match boot_library_finder t with + | None -> Resolve.Memo.return None + | Some (loc, lib) -> + let open Memo.O in + let+ lib = Memo.Lazy.force lib in + Resolve.map lib ~f:(fun lib -> Some (loc, lib)) (* Should we register errors and printers, or raise is OK? *) - let create_from_coqlib_stanzas sl = - let libs = - match Coq_lib_name.Map.of_list_map ~f:create_from_stanza sl with - | Ok m -> m - | Error (_name, _w1, (_, w2)) -> - Result.ok_exn (Error.duplicate_theory_name w2) - in + let create_from_coqlib_stanzas ~(parent : t option) ~find_db + (entries : (Coq_stanza.Theory.t * entry) list) = + let t = Fdecl.create Dyn.opaque in let boot = - match List.find_all ~f:(fun (_, s) -> s.Coq_stanza.Theory.boot) sl with - | [] -> None - | [ l ] -> Some ((snd l).buildable.loc, snd (create_from_stanza l)) - | _ :: (_, s2) :: _ -> - Result.ok_exn (Error.duplicate_boot_lib ~loc:s2.buildable.loc s2) + let boot = + match + List.find_all entries + ~f:(fun ((theory : Coq_stanza.Theory.t), _entry) -> theory.boot) + with + | [] -> None + | [ ((theory : Coq_stanza.Theory.t), _entry) ] -> + let loc, name = theory.name in + Some (loc, name, theory.buildable.coq_lang_version) + | boots -> + let stanzas = List.map boots ~f:fst in + Error.duplicate_boot_lib stanzas + in + match boot with + | None -> None + | Some (loc, name, coq_lang_version) -> + let lib = + Memo.lazy_ (fun () -> + let t = Fdecl.get t in + resolve t ~coq_lang_version (loc, name)) + in + Some (loc, lib) in - { boot; libs } - - let resolve ?(allow_private_deps = true) db (loc, name) = - match Coq_lib_name.Map.find db.libs name with - | Some s -> - if (not allow_private_deps) && Option.is_none s.package then - Error.private_deps_not_allowed ~loc s - else Ok s - | None -> Error.theory_not_found ~loc name - - let find_many t ~loc = Result.List.map ~f:(fun name -> resolve t (loc, name)) - - module Coq_lib_closure = Top_closure.Make (String.Set) (Or_exn) - - let add_boot db theories = - match db.boot with - | None -> theories - (* XXX: Note that this means that we will prefix Coq with -Q, not sure we - want to do that (yet), but seems like good practice. *) - | Some (loc, stdlib) -> (loc, snd stdlib.name) :: theories - - let top_closure db theories ~allow_private_deps ~loc = - let open Result.O in - let* theories = - add_boot db theories - |> Result.List.map ~f:(resolve ~allow_private_deps db) + let resolve = + let map = + match + Coq_lib_name.Map.of_list_map entries + ~f:(fun ((theory : Coq_stanza.Theory.t), entry) -> + (snd theory.name, (theory, entry))) + with + | Ok m -> m + | Error (_name, _, (theory, _entry)) -> + Error.duplicate_theory_name theory.name + in + fun name -> + match Coq_lib_name.Map.find map name with + | None -> `Not_found + | Some (theory, entry) -> ( + match entry with + | Theory dir -> `Theory (find_db dir, dir, theory) + | Redirect db -> `Redirect db) in - let key (t : lib) = Coq_lib_name.to_string (snd t.name) in - let deps (t : lib) = - Result.List.map ~f:(resolve ~allow_private_deps db) t.theories + Fdecl.set t { boot; resolve; parent }; + Fdecl.get t + + let find_many t ~loc theories ~coq_lang_version = + Resolve.Memo.List.map theories ~f:(fun name -> + resolve ~coq_lang_version t (loc, name)) + + let requires_for_user_written db theories ~coq_lang_version = + let open Memo.O in + let+ theories = + Resolve.Memo.List.map theories ~f:(resolve ~coq_lang_version db) in - match Coq_lib_closure.top_closure theories ~key ~deps with - | Ok (Ok s) -> Ok s - | Ok (Error cycle) -> Error.cycle_found ~loc cycle - | Error exn -> Error exn - - let requires db (t : lib) : lib list Or_exn.t = - let allow_private_deps = Option.is_none t.package in - let loc = location t in - top_closure db t.theories ~loc ~allow_private_deps - - let requires_for_user_written db = function - | [] -> Ok [] - | start :: xs as theories -> - let loc = - let stop = Option.value (List.last xs) ~default:start in - Loc.span (fst start) (fst stop) - in - top_closure db theories ~loc ~allow_private_deps:true + Resolve.O.(theories >>= top_closure) - let resolve db l = resolve db l + let resolve db l ~coq_lang_version = resolve db ~coq_lang_version l end + +let theories_closure t = Lazy.force t.theories_closure diff --git a/src/dune_rules/coq_lib.mli b/src/dune_rules/coq_lib.mli index 5ac26f80baf8..062a241733df 100644 --- a/src/dune_rules/coq_lib.mli +++ b/src/dune_rules/coq_lib.mli @@ -10,11 +10,8 @@ val name : t -> Coq_lib_name.t val implicit : t -> bool -(* this is not really a wrapper for the prefix path *) -val wrapper : t -> string - (** ml libraries *) -val libraries : t -> (Loc.t * Lib_name.t) list +val libraries : t -> (Loc.t * Lib.t) list Resolve.t val src_root : t -> Path.Build.t @@ -22,24 +19,42 @@ val obj_root : t -> Path.Build.t val package : t -> Package.t option +(** Return the list of dependencies needed for compiling this library *) +val theories_closure : t -> t list Resolve.t + module DB : sig - type lib + type lib := t type t - val create_from_coqlib_stanzas : - (Path.Build.t * Coq_stanza.Theory.t) list -> t - - val find_many : t -> loc:Loc.t -> Coq_lib_name.t list -> lib list Or_exn.t + type entry = + | Theory of Path.Build.t + | Redirect of t - val boot_library : t -> (Loc.t * lib) option - - val resolve : t -> Loc.t * Coq_lib_name.t -> lib Or_exn.t - - (** Return the list of dependencies needed for compiling this library *) - val requires : t -> lib -> lib list Or_exn.t + val create_from_coqlib_stanzas : + parent:t option + -> find_db:(Path.Build.t -> Lib.DB.t) + -> (Coq_stanza.Theory.t * entry) list + -> t + + val find_many : + t + -> loc:Loc.t + -> Coq_lib_name.t list + -> coq_lang_version:Dune_sexp.Syntax.Version.t + -> lib list Resolve.Memo.t + + val boot_library : t -> (Loc.t * lib) option Resolve.Memo.t + + val resolve : + t + -> Loc.t * Coq_lib_name.t + -> coq_lang_version:Dune_sexp.Syntax.Version.t + -> lib Resolve.Memo.t val requires_for_user_written : - t -> (Loc.t * Coq_lib_name.t) list -> lib list Or_exn.t + t + -> (Loc.t * Coq_lib_name.t) list + -> coq_lang_version:Dune_sexp.Syntax.Version.t + -> lib list Resolve.Memo.t end -with type lib := t diff --git a/src/dune_rules/coq_lib_name.ml b/src/dune_rules/coq_lib_name.ml index c0342ccc1eb3..abbbc6ccab0e 100644 --- a/src/dune_rules/coq_lib_name.ml +++ b/src/dune_rules/coq_lib_name.ml @@ -8,6 +8,8 @@ open! Import (* Coq Directory Path *) type t = string list +let compare = List.compare ~compare:String.compare + let to_string x = String.concat ~sep:"." x let to_dir x = String.concat ~sep:"/" x diff --git a/src/dune_rules/coq_lib_name.mli b/src/dune_rules/coq_lib_name.mli index 235dc7b48210..7f0df9dae970 100644 --- a/src/dune_rules/coq_lib_name.mli +++ b/src/dune_rules/coq_lib_name.mli @@ -10,6 +10,8 @@ open Import (** A Coq library name is a dot-separated list of Coq module identifiers. *) type t +val compare : t -> t -> Ordering.t + (** Returns the wrapper name, a dot-separated list of Coq module identifies *) val wrapper : t -> string diff --git a/src/dune_rules/coq_rules.ml b/src/dune_rules/coq_rules.ml index 1e2de995d44a..290ccf0373c2 100644 --- a/src/dune_rules/coq_rules.ml +++ b/src/dune_rules/coq_rules.ml @@ -68,7 +68,7 @@ module Bootstrap = struct | Some (_loc, lib) -> ( (* This is here as an optimization, TODO; replace with per_file flags *) let init = - String.equal (Coq_lib.wrapper lib) wrapper_name + String.equal (Coq_lib_name.wrapper (Coq_lib.name lib)) wrapper_name && Option.equal String.equal (List.hd_opt (Coq_module.prefix coq_module)) (Some "Init") @@ -111,11 +111,12 @@ module Context = struct ; dir : Path.Build.t ; expander : Expander.t ; buildable : Buildable.t - ; theories_deps : Coq_lib.t list Resolve.t + ; theories_deps : Coq_lib.t list Resolve.Memo.t ; mlpack_rule : unit Action_builder.t - ; ml_flags : 'a Command.Args.t + ; ml_flags : 'a Command.Args.t Resolve.Memo.t ; scope : Scope.t - ; boot_type : Bootstrap.t + ; boot_type : Bootstrap.t Resolve.Memo.t + ; build_dir : Path.Build.t ; profile_flags : string list Action_builder.t ; mode : Coq_mode.t ; native_includes : Path.Set.t Resolve.t @@ -132,27 +133,35 @@ module Context = struct let theories_flags = let setup_theory_flag lib = - let wrapper = Coq_lib.wrapper lib in let dir = Coq_lib.src_root lib in let binding_flag = if Coq_lib.implicit lib then "-R" else "-Q" in - [ Command.Args.A binding_flag; Path (Path.build dir); A wrapper ] + [ Command.Args.A binding_flag + ; Path (Path.build dir) + ; A (Coq_lib.name lib |> Coq_lib_name.wrapper) + ] in fun t -> - Resolve.args - (let open Resolve.O in + Resolve.Memo.args + (let open Resolve.Memo.O in let+ libs = t.theories_deps in Command.Args.S (List.concat_map libs ~f:setup_theory_flag)) let coqc_file_flags cctx = let file_flags = - [ cctx.ml_flags + [ Command.Args.Dyn (Resolve.Memo.read cctx.ml_flags) ; theories_flags cctx ; Command.Args.A "-R" ; Path (Path.build cctx.dir) ; A cctx.wrapper_name ] in - [ Command.Args.S (Bootstrap.flags cctx.boot_type); S file_flags ] + [ Command.Args.Dyn + (Resolve.Memo.map + ~f:(fun b -> Command.Args.S (Bootstrap.flags b)) + cctx.boot_type + |> Resolve.Memo.read) + ; S file_flags + ] let coqc_native_flags cctx : _ Command.Args.t = match cctx.mode with @@ -198,17 +207,26 @@ module Context = struct ; A cctx.wrapper_name ] in - [ Command.Args.S (Bootstrap.flags cctx.boot_type); S file_flags ] + [ Command.Args.Dyn + (Resolve.Memo.map + ~f:(fun b -> Command.Args.S (Bootstrap.flags b)) + cctx.boot_type + |> Resolve.Memo.read) + ; S file_flags + ] (* compute include flags and mlpack rules *) - let setup_ml_deps ~lib_db libs theories = + let setup_ml_deps libs theories = (* Pair of include flags and paths to mlpack *) let libs = let open Resolve.Memo.O in - let* theories = Resolve.Memo.lift theories in - let libs = libs @ List.concat_map ~f:Coq_lib.libraries theories in - let* libs = libs_of_coq_deps ~lib_db libs in - Lib.closure ~linking:false libs + let* theories = theories in + let* theories = + Resolve.Memo.lift + @@ Resolve.List.concat_map ~f:Coq_lib.libraries theories + in + let libs = libs @ theories in + Lib.closure ~linking:false (List.map ~f:snd libs) in ( Resolve.Memo.args (Resolve.Memo.map libs ~f:Util.include_flags) , let open Action_builder.O in @@ -224,12 +242,10 @@ module Context = struct let+ coq_sources = Dir_contents.coq dir_contents in Coq_sources.directories coq_sources ~name - let setup_native_theory_includes ~sctx ~mode - ~(theories_deps : Coq_lib.t list Resolve.t) ~theory_dirs = + let setup_native_theory_includes ~sctx ~mode ~theories_deps ~theory_dirs = match mode with | Coq_mode.Native -> - Resolve.Memo.bind (Resolve.Memo.lift theories_deps) - ~f:(fun theories_deps -> + Resolve.Memo.bind theories_deps ~f:(fun theories_deps -> let+ l = Memo.parallel_map theories_deps ~f:(fun lib -> let+ theory_dirs = directories_of_lib ~sctx lib in @@ -248,7 +264,22 @@ module Context = struct let lib_db = Scope.libs scope in (* ML-level flags for depending libraries *) let ml_flags, mlpack_rule = - setup_ml_deps ~lib_db buildable.libraries theories_deps + let res = + let open Resolve.Memo.O in + let+ libs = + Resolve.Memo.List.map buildable.libraries ~f:(fun (loc, name) -> + let+ lib = Lib.DB.resolve lib_db (loc, name) in + (loc, lib)) + in + setup_ml_deps libs theories_deps + in + let ml_flags = Resolve.Memo.map res ~f:fst in + let mlpack_rule = + let open Action_builder.O in + let* _, mlpack_rule = Resolve.Memo.read res in + mlpack_rule + in + (ml_flags, mlpack_rule) in let mode = select_native_mode ~sctx ~buildable in let* native_includes = @@ -273,7 +304,8 @@ module Context = struct ; mlpack_rule ; ml_flags ; scope - ; boot_type = Bootstrap.No_boot + ; boot_type = Resolve.Memo.return Bootstrap.No_boot + ; build_dir = (Super_context.context sctx).build_dir ; profile_flags ; mode ; native_includes @@ -281,8 +313,9 @@ module Context = struct } let for_module t coq_module = - let boot_lib = t.scope |> Scope.coq_libs |> Coq_lib.DB.boot_library in let boot_type = + let open Resolve.Memo.O in + let+ boot_lib = t.scope |> Scope.coq_libs |> Coq_lib.DB.boot_library in Bootstrap.get ~boot_lib ~wrapper_name:t.wrapper_name coq_module in { t with boot_type } @@ -339,9 +372,11 @@ let parse_coqdep ~dir ~(boot_type : Bootstrap.t) ~coq_module let deps_of ~dir ~boot_type coq_module = let stdout_to = Coq_module.dep_file ~obj_dir:dir coq_module in Action_builder.dyn_paths_unit - (Action_builder.map - (Action_builder.lines_of (Path.build stdout_to)) - ~f:(parse_coqdep ~dir ~boot_type ~coq_module)) + (let open Action_builder.O in + let* boot_type = Resolve.Memo.read boot_type in + Action_builder.map + (Action_builder.lines_of (Path.build stdout_to)) + ~f:(parse_coqdep ~dir ~boot_type ~coq_module)) let coqdep_rule (cctx : _ Context.t) ~source_rule ~file_flags coq_module = (* coqdep needs the full source + plugin's mlpack to be present :( *) @@ -420,7 +455,7 @@ let coqdoc_rule (cctx : _ Context.t) ~sctx ~name:(_, name) ~file_flags ~mode let file_flags = let globs = let open Action_builder.O in - let* theories_deps = Resolve.read theories_deps in + let* theories_deps = Resolve.Memo.read theories_deps in Action_builder.of_memo @@ let open Memo.O in @@ -491,7 +526,7 @@ let source_rule ~sctx theories = tree to produce correct dependencies, including those of dependencies *) Action_builder.dyn_paths_unit (let open Action_builder.O in - let* theories = Resolve.read theories in + let* theories = Resolve.Memo.read theories in let+ l = Action_builder.List.map theories ~f:(coq_modules_of_theory ~sctx) in @@ -501,12 +536,16 @@ let setup_rules ~sctx ~dir ~dir_contents (s : Theory.t) = let name = snd s.name in let scope = SC.find_scope_by_dir sctx dir in let coq_lib_db = Scope.coq_libs scope in - let theory = Coq_lib.DB.resolve coq_lib_db s.name |> Result.ok_exn in + let theory = + Coq_lib.DB.resolve coq_lib_db ~coq_lang_version:s.buildable.coq_lang_version + s.name + in let* coq_dir_contents = Dir_contents.coq dir_contents in let* cctx = - let wrapper_name = Coq_lib.wrapper theory in + let wrapper_name = Coq_lib_name.wrapper name in let theories_deps = - Coq_lib.DB.requires coq_lib_db theory |> Resolve.of_result + Resolve.Memo.bind theory ~f:(fun theory -> + Resolve.Memo.lift @@ Coq_lib.theories_closure theory) in let theory_dirs = Coq_sources.directories coq_dir_contents ~name |> Path.Build.Set.of_list @@ -519,7 +558,8 @@ let setup_rules ~sctx ~dir ~dir_contents (s : Theory.t) = let coq_modules = Coq_sources.library coq_dir_contents ~name in let source_rule = let theories = - let open Resolve.O in + let open Resolve.Memo.O in + let* theory = theory in let+ theories = cctx.theories_deps in theory :: theories in @@ -552,12 +592,16 @@ let coqtop_args_theory ~sctx ~dir ~dir_contents (s : Theory.t) coq_module = let name = snd s.name in let scope = SC.find_scope_by_dir sctx dir in let coq_lib_db = Scope.coq_libs scope in - let theory = Coq_lib.DB.resolve coq_lib_db s.name |> Result.ok_exn in + let theory = + Coq_lib.DB.resolve coq_lib_db s.name + ~coq_lang_version:s.buildable.coq_lang_version + in let* coq_dir_contents = Dir_contents.coq dir_contents in - let+ cctx = - let wrapper_name = Coq_lib.wrapper theory in + let* cctx = + let wrapper_name = Coq_lib_name.wrapper name in let theories_deps = - Coq_lib.DB.requires coq_lib_db theory |> Resolve.of_result + Resolve.Memo.bind theory ~f:(fun theory -> + Resolve.Memo.lift @@ Coq_lib.theories_closure theory) in let theory_dirs = Coq_sources.directories coq_dir_contents ~name in let theory_dirs = Path.Build.Set.of_list theory_dirs in @@ -566,7 +610,8 @@ let coqtop_args_theory ~sctx ~dir ~dir_contents (s : Theory.t) coq_module = s.buildable in let cctx = Context.for_module cctx coq_module in - (Context.coqc_file_flags cctx, cctx.boot_type) + let+ boot_type = Resolve.Memo.read_memo cctx.boot_type in + (Context.coqc_file_flags cctx, boot_type) (******************************************************************************) (* Install rules *) @@ -597,6 +642,7 @@ let coq_plugins_install_rules ~scope ~package ~dst_dir (s : Theory.t) = Path.Local.(to_string (relative dst_dir plugin_file_basename)) in let entry = Install.Entry.make Section.Lib_root ~dst plugin_file in + (* TODO this [loc] should come from [s.buildable.libraries] *) Install.Entry.Sourced.create ~loc entry) else [] in @@ -670,8 +716,8 @@ let setup_extraction_rules ~sctx ~dir ~dir_contents (s : Extraction.t) = let theories_deps = let scope = SC.find_scope_by_dir sctx dir in let coq_lib_db = Scope.coq_libs scope in - Resolve.of_result - (Coq_lib.DB.requires_for_user_written coq_lib_db s.buildable.theories) + Coq_lib.DB.requires_for_user_written coq_lib_db s.buildable.theories + ~coq_lang_version:s.buildable.coq_lang_version in let theory_dirs = Path.Build.Set.empty in Context.create sctx ~coqc_dir:dir ~dir ~wrapper_name ~theories_deps @@ -699,16 +745,17 @@ let coqtop_args_extraction ~sctx ~dir ~dir_contents (s : Extraction.t) = let theories_deps = let scope = SC.find_scope_by_dir sctx dir in let coq_lib_db = Scope.coq_libs scope in - Resolve.of_result - (Coq_lib.DB.requires_for_user_written coq_lib_db s.buildable.theories) + Coq_lib.DB.requires_for_user_written coq_lib_db s.buildable.theories + ~coq_lang_version:s.buildable.coq_lang_version in let theory_dirs = Path.Build.Set.empty in Context.create sctx ~coqc_dir:dir ~dir ~wrapper_name ~theories_deps ~theory_dirs s.buildable in - let+ coq_module = + let* coq_module = let+ coq = Dir_contents.coq dir_contents in Coq_sources.extract coq s in let cctx = Context.for_module cctx coq_module in - (Context.coqc_file_flags cctx, cctx.boot_type) + let+ boot_type = Resolve.Memo.read_memo cctx.boot_type in + (Context.coqc_file_flags cctx, boot_type) diff --git a/src/dune_rules/coq_rules.mli b/src/dune_rules/coq_rules.mli index dedd3108e903..157371123a3c 100644 --- a/src/dune_rules/coq_rules.mli +++ b/src/dune_rules/coq_rules.mli @@ -47,7 +47,7 @@ val setup_extraction_rules : build all dependencies of the Coq module [m]. *) val deps_of : dir:Path.Build.t - -> boot_type:Bootstrap.t + -> boot_type:Bootstrap.t Resolve.Memo.t -> Coq_module.t -> unit Dune_engine.Action_builder.t diff --git a/src/dune_rules/coq_stanza.ml b/src/dune_rules/coq_stanza.ml index b2a9f50352d6..a0db88f983a4 100644 --- a/src/dune_rules/coq_stanza.ml +++ b/src/dune_rules/coq_stanza.ml @@ -23,11 +23,13 @@ let coq_syntax = [ ((0, 1), `Since (1, 9)) ; ((0, 2), `Since (2, 5)) ; ((0, 3), `Since (2, 8)) + ; ((0, 4), `Since (3, 3)) ] module Buildable = struct type t = { flags : Ordered_set_lang.Unexpanded.t + ; coq_lang_version : Dune_sexp.Syntax.Version.t ; mode : Loc.t * Coq_mode.t ; libraries : (Loc.t * Lib_name.t) list (** ocaml libraries *) ; theories : (Loc.t * Coq_lib_name.t) list (** coq libraries *) @@ -35,12 +37,12 @@ module Buildable = struct } let decode = + let* coq_lang_version = Dune_lang.Syntax.get_exn coq_syntax in let+ loc = loc and+ flags = Ordered_set_lang.Unexpanded.field "flags" and+ mode = - let* version = Dune_lang.Syntax.get_exn coq_syntax in let default = - if version < (0, 3) then Coq_mode.Legacy else Coq_mode.VoOnly + if coq_lang_version < (0, 3) then Coq_mode.Legacy else Coq_mode.VoOnly in located (field "mode" ~default @@ -52,7 +54,7 @@ module Buildable = struct (Dune_lang.Syntax.since coq_syntax (0, 2) >>> repeat Coq_lib_name.decode) ~default:[] in - { flags; mode; libraries; theories; loc } + { flags; mode; coq_lang_version; libraries; theories; loc } end module Extraction = struct diff --git a/src/dune_rules/coq_stanza.mli b/src/dune_rules/coq_stanza.mli index 886900d47307..e6f2b9186a8d 100644 --- a/src/dune_rules/coq_stanza.mli +++ b/src/dune_rules/coq_stanza.mli @@ -3,6 +3,7 @@ open Import module Buildable : sig type t = { flags : Ordered_set_lang.Unexpanded.t + ; coq_lang_version : Dune_sexp.Syntax.Version.t ; mode : Loc.t * Coq_mode.t ; libraries : (Loc.t * Lib_name.t) list (** ocaml libraries *) ; theories : (Loc.t * Coq_lib_name.t) list (** coq libraries *) diff --git a/src/dune_rules/scope.ml b/src/dune_rules/scope.ml index 33fa007be84c..257a7306250e 100644 --- a/src/dune_rules/scope.ml +++ b/src/dune_rules/scope.ml @@ -20,6 +20,33 @@ module DB = struct type t = { by_dir : scope Path.Source.Map.t } + let find_by_dir_in_map = + (* This function is linear in the depth of [dir] in the worst case, so if it + shows up in the profile we should memoize it. *) + let find_by_dir map (dir : Path.Source.t) = + let rec loop d = + match Path.Source.Map.find map d with + | Some s -> s + | None -> ( + match Path.Source.parent d with + | Some d -> loop d + | None -> + Code_error.raise "find_by_dir: invalid directory" + [ ("d", Path.Source.to_dyn d); ("dir", Path.Source.to_dyn dir) ]) + in + loop dir + in + fun map dir -> + if Path.Build.is_root dir then + Code_error.raise "Scope.DB.find_by_dir_in_map got an invalid path" + [ ("dir", Path.Build.to_dyn dir) ]; + find_by_dir map (Path.Build.drop_build_context_exn dir) + + let find_by_dir t dir = find_by_dir_in_map t.by_dir dir + + let find_by_project t project = + Path.Source.Map.find_exn t.by_dir (Dune_project.root project) + module Found_or_redirect : sig type t = private | Found of Lib_info.external_ @@ -101,24 +128,6 @@ module DB = struct ~all:(fun () -> Lib_name.Map.keys map |> Memo.return) ~lib_config - (* This function is linear in the depth of [dir] in the worst case, so if it - shows up in the profile we should memoize it. *) - let find_by_dir t (dir : Path.Source.t) = - let rec loop d = - match Path.Source.Map.find t.by_dir d with - | Some s -> s - | None -> ( - match Path.Source.parent d with - | Some d -> loop d - | None -> - Code_error.raise "find_by_dir: invalid directory" - [ ("d", Path.Source.to_dyn d); ("dir", Path.Source.to_dyn dir) ]) - in - loop dir - - let find_by_project t project = - Path.Source.Map.find_exn t.by_dir (Dune_project.root project) - type redirect_to = | Project of Dune_project.t | Name of (Loc.t * Lib_name.t) @@ -131,6 +140,13 @@ module DB = struct Lib.DB.Resolve_result.redirect (Some scope.db) (Loc.none, name) | Some (Name name) -> Lib.DB.Resolve_result.redirect None name + let public_theories ~find_db coq_stanzas = + List.filter_map coq_stanzas ~f:(fun (dir, (stanza : Coq_stanza.Theory.t)) -> + if Option.is_some stanza.package then + Some (stanza, Coq_lib.DB.Theory dir) + else None) + |> Coq_lib.DB.create_from_coqlib_stanzas ~find_db ~parent:None + (* Create a database from the public libraries defined in the stanzas *) let public_libs t ~installed_libs ~lib_config stanzas = let public_libs = @@ -174,7 +190,8 @@ module DB = struct module Path_source_map_traversals = Memo.Make_map_traversals (Path.Source.Map) - let scopes_by_dir context ~projects ~public_libs stanzas coq_stanzas = + let scopes_by_dir context ~projects ~public_libs ~public_theories + stanzas coq_stanzas = let open Memo.O in let projects_by_dir = List.map projects ~f:(fun (project : Dune_project.t) -> @@ -192,12 +209,11 @@ module DB = struct (Dune_project.root project, stanza)) |> Path.Source.Map.of_list_multi in - let coq_db_by_project_dir = - List.map coq_stanzas ~f:(fun (dir, t) -> - let project = t.Coq_stanza.Theory.project in - (Dune_project.root project, (dir, t))) + let coq_stanzas_by_project_dir = + List.map coq_stanzas ~f:(fun (dir, (stanza : Coq_stanza.Theory.t)) -> + let project = stanza.project in + (Dune_project.root project, (dir, stanza))) |> Path.Source.Map.of_list_multi - |> Path.Source.Map.map ~f:Coq_lib.DB.create_from_coqlib_stanzas in let lib_config = Context.lib_config context in let+ db_by_project_dir = @@ -213,14 +229,30 @@ module DB = struct in (project, db)) in + let coq_db_by_project_dir = + let find_db dir = snd (find_by_dir_in_map db_by_project_dir dir) in + Path.Source.Map.merge projects_by_dir coq_stanzas_by_project_dir + ~f:(fun _dir project coq_stanzas -> + assert (Option.is_some project); + let stanzas = Option.value coq_stanzas ~default:[] in + let entries = + List.map stanzas ~f:(fun (dir, (stanza : Coq_stanza.Theory.t)) -> + let entry = + match stanza.package with + | None -> Coq_lib.DB.Theory dir + | Some _ -> Redirect public_theories + in + (stanza, entry)) + in + Some entries) + |> Path.Source.Map.map ~f:(fun stanzas -> + Coq_lib.DB.create_from_coqlib_stanzas + ~parent:(Some public_theories) ~find_db stanzas) + in Path.Source.Map.merge db_by_project_dir coq_db_by_project_dir ~f:(fun _dir project_and_db coq_db -> let project, db = Option.value_exn project_and_db in - let coq_db = - match coq_db with - | Some db -> db - | None -> Coq_lib.DB.create_from_coqlib_stanzas [] - in + let coq_db = Option.value_exn coq_db in let root = Path.Build.append_source context.build_dir (Dune_project.root project) in @@ -234,19 +266,17 @@ module DB = struct let+ installed_libs = Lib.DB.installed context in public_libs t ~lib_config ~installed_libs stanzas in + let public_theories = + public_theories coq_stanzas ~find_db:(fun _ -> public_libs) + in let+ by_dir = - scopes_by_dir context ~projects ~public_libs stanzas coq_stanzas + scopes_by_dir context ~projects ~public_libs ~public_theories + stanzas coq_stanzas in let value = { by_dir } in Fdecl.set t value; (value, public_libs) - let find_by_dir t dir = - if Path.Build.is_root dir then - Code_error.raise "Scope.DB.find_by_dir got an invalid path" - [ ("dir", Path.Build.to_dyn dir) ]; - find_by_dir t (Path.Build.drop_build_context_exn dir) - let create_from_stanzas ~projects ~context stanzas = let stanzas, coq_stanzas = Dune_file.fold_stanzas stanzas ~init:([], []) diff --git a/test/blackbox-tests/test-cases/coq/compose-boot.t/cboot.opam b/test/blackbox-tests/test-cases/coq/compose-boot.t/A/A.opam similarity index 100% rename from test/blackbox-tests/test-cases/coq/compose-boot.t/cboot.opam rename to test/blackbox-tests/test-cases/coq/compose-boot.t/A/A.opam diff --git a/test/blackbox-tests/test-cases/coq/compose-boot.t/A/a.v b/test/blackbox-tests/test-cases/coq/compose-boot.t/A/a.v new file mode 100644 index 000000000000..8089bf38ce4c --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-boot.t/A/a.v @@ -0,0 +1 @@ +Inductive AnotherBegining := Of | The | Universe. diff --git a/test/blackbox-tests/test-cases/coq/compose-boot.t/A/dune b/test/blackbox-tests/test-cases/coq/compose-boot.t/A/dune new file mode 100644 index 000000000000..c5888866aadd --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-boot.t/A/dune @@ -0,0 +1,4 @@ +(coq.theory + (name A) + (package A) + (boot)) diff --git a/test/blackbox-tests/test-cases/coq/compose-boot.t/dune-project b/test/blackbox-tests/test-cases/coq/compose-boot.t/A/dune-project similarity index 100% rename from test/blackbox-tests/test-cases/coq/compose-boot.t/dune-project rename to test/blackbox-tests/test-cases/coq/compose-boot.t/A/dune-project diff --git a/test/blackbox-tests/test-cases/coq/compose-cycle.t/ccycle.opam b/test/blackbox-tests/test-cases/coq/compose-boot.t/B/B.opam similarity index 100% rename from test/blackbox-tests/test-cases/coq/compose-cycle.t/ccycle.opam rename to test/blackbox-tests/test-cases/coq/compose-boot.t/B/B.opam diff --git a/test/blackbox-tests/test-cases/coq/compose-boot.t/B/b.v b/test/blackbox-tests/test-cases/coq/compose-boot.t/B/b.v new file mode 100644 index 000000000000..46e4b397d40e --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-boot.t/B/b.v @@ -0,0 +1 @@ +Inductive Begining := Of | The | Universe. diff --git a/test/blackbox-tests/test-cases/coq/compose-boot.t/B/dune b/test/blackbox-tests/test-cases/coq/compose-boot.t/B/dune new file mode 100644 index 000000000000..128896380043 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-boot.t/B/dune @@ -0,0 +1,6 @@ +(coq.theory + (name B) + (package B) + (boot)) + + diff --git a/test/blackbox-tests/test-cases/coq/compose-boot.t/B/dune-project b/test/blackbox-tests/test-cases/coq/compose-boot.t/B/dune-project new file mode 100644 index 000000000000..9ef6b81a34a1 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-boot.t/B/dune-project @@ -0,0 +1,3 @@ +(lang dune 2.5) + +(using coq 0.2) diff --git a/test/blackbox-tests/test-cases/coq/compose-boot.t/boot/Init/Prelude.v b/test/blackbox-tests/test-cases/coq/compose-boot.t/boot/Init/Prelude.v deleted file mode 100644 index eaaf0e55b2cf..000000000000 --- a/test/blackbox-tests/test-cases/coq/compose-boot.t/boot/Init/Prelude.v +++ /dev/null @@ -1 +0,0 @@ -Definition id := forall (X : Type), X. diff --git a/test/blackbox-tests/test-cases/coq/compose-boot.t/dune b/test/blackbox-tests/test-cases/coq/compose-boot.t/dune deleted file mode 100644 index 32d3fd982714..000000000000 --- a/test/blackbox-tests/test-cases/coq/compose-boot.t/dune +++ /dev/null @@ -1,3 +0,0 @@ -(rule - (alias default) - (action (echo "%{read:cboot.install}"))) diff --git a/test/blackbox-tests/test-cases/coq/compose-boot.t/dune-workspace b/test/blackbox-tests/test-cases/coq/compose-boot.t/dune-workspace new file mode 100644 index 000000000000..0c226b5b0c6e --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-boot.t/dune-workspace @@ -0,0 +1 @@ +(lang dune 3.2) diff --git a/test/blackbox-tests/test-cases/coq/compose-boot.t/run.t b/test/blackbox-tests/test-cases/coq/compose-boot.t/run.t index 8f2f58e436b1..a7d7a27e307e 100644 --- a/test/blackbox-tests/test-cases/coq/compose-boot.t/run.t +++ b/test/blackbox-tests/test-cases/coq/compose-boot.t/run.t @@ -1,2 +1,7 @@ -# Test only works on Coq 8.12 due to boot constraints -# $ dune build --display short --debug-dependency-path +Testing composition with two boot libraries + + $ dune build + Error: Cannot have more than one boot theory in scope: + - B at B/dune:1 + - A at A/dune:1 + [1] diff --git a/test/blackbox-tests/test-cases/coq/compose-boot.t/user/dune b/test/blackbox-tests/test-cases/coq/compose-boot.t/user/dune deleted file mode 100644 index 5402df7cc246..000000000000 --- a/test/blackbox-tests/test-cases/coq/compose-boot.t/user/dune +++ /dev/null @@ -1,5 +0,0 @@ -(coq.theory - (name user) - (package cboot)) - - diff --git a/test/blackbox-tests/test-cases/coq/compose-boot.t/user/user.v b/test/blackbox-tests/test-cases/coq/compose-boot.t/user/user.v deleted file mode 100644 index cdda78d422b5..000000000000 --- a/test/blackbox-tests/test-cases/coq/compose-boot.t/user/user.v +++ /dev/null @@ -1 +0,0 @@ -Definition a := id. diff --git a/test/blackbox-tests/test-cases/coq/compose-cycle.t/a/a.v b/test/blackbox-tests/test-cases/coq/compose-cycle.t/A/a.v similarity index 100% rename from test/blackbox-tests/test-cases/coq/compose-cycle.t/a/a.v rename to test/blackbox-tests/test-cases/coq/compose-cycle.t/A/a.v diff --git a/test/blackbox-tests/test-cases/coq/compose-cycle.t/A/dune b/test/blackbox-tests/test-cases/coq/compose-cycle.t/A/dune new file mode 100644 index 000000000000..90fefd9be0ec --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-cycle.t/A/dune @@ -0,0 +1,3 @@ +(coq.theory + (name A) + (theories B)) diff --git a/test/blackbox-tests/test-cases/coq/compose-cycle.t/b/b.v b/test/blackbox-tests/test-cases/coq/compose-cycle.t/B/b.v similarity index 100% rename from test/blackbox-tests/test-cases/coq/compose-cycle.t/b/b.v rename to test/blackbox-tests/test-cases/coq/compose-cycle.t/B/b.v diff --git a/test/blackbox-tests/test-cases/coq/compose-cycle.t/B/dune b/test/blackbox-tests/test-cases/coq/compose-cycle.t/B/dune new file mode 100644 index 000000000000..f087163ebd4d --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-cycle.t/B/dune @@ -0,0 +1,3 @@ +(coq.theory + (name B) + (theories A)) diff --git a/test/blackbox-tests/test-cases/coq/compose-cycle.t/a/dune b/test/blackbox-tests/test-cases/coq/compose-cycle.t/a/dune deleted file mode 100644 index 478550e09852..000000000000 --- a/test/blackbox-tests/test-cases/coq/compose-cycle.t/a/dune +++ /dev/null @@ -1,4 +0,0 @@ -(coq.theory - (name a) - (package ccycle) - (theories b)) diff --git a/test/blackbox-tests/test-cases/coq/compose-cycle.t/b/dune b/test/blackbox-tests/test-cases/coq/compose-cycle.t/b/dune deleted file mode 100644 index 5f42b4087e99..000000000000 --- a/test/blackbox-tests/test-cases/coq/compose-cycle.t/b/dune +++ /dev/null @@ -1,4 +0,0 @@ -(coq.theory - (name b) - (package ccycle) - (theories a)) diff --git a/test/blackbox-tests/test-cases/coq/compose-cycle.t/dune b/test/blackbox-tests/test-cases/coq/compose-cycle.t/dune deleted file mode 100644 index e622b2ade9e6..000000000000 --- a/test/blackbox-tests/test-cases/coq/compose-cycle.t/dune +++ /dev/null @@ -1,3 +0,0 @@ -(rule - (alias default) - (action (echo "%{read:ccycle.install}"))) diff --git a/test/blackbox-tests/test-cases/coq/compose-cycle.t/dune-project b/test/blackbox-tests/test-cases/coq/compose-cycle.t/dune-project index 9ef6b81a34a1..06314b536ad9 100644 --- a/test/blackbox-tests/test-cases/coq/compose-cycle.t/dune-project +++ b/test/blackbox-tests/test-cases/coq/compose-cycle.t/dune-project @@ -1,3 +1,2 @@ -(lang dune 2.5) - -(using coq 0.2) +(lang dune 3.2) +(using coq 0.3) diff --git a/test/blackbox-tests/test-cases/coq/compose-cycle.t/run.t b/test/blackbox-tests/test-cases/coq/compose-cycle.t/run.t index 1934679769f2..6a76d25981bd 100644 --- a/test/blackbox-tests/test-cases/coq/compose-cycle.t/run.t +++ b/test/blackbox-tests/test-cases/coq/compose-cycle.t/run.t @@ -1,28 +1,11 @@ - $ dune build --debug-dependency-path - File "a/dune", line 2, characters 7-8: - 2 | (name a) - ^ - Error: Cycle found - - b - - a - - b - -> required by _build/default/a/a.v.d - -> required by _build/default/a/a.vo - -> required by _build/install/default/lib/coq/user-contrib/a/a.vo - -> required by _build/default/ccycle.install - -> required by %{read:ccycle.install} at dune:3 - -> required by alias default in dune:1 - File "b/dune", line 2, characters 7-8: - 2 | (name b) - ^ - Error: Cycle found - - a - - b - - a - -> required by _build/default/b/b.v.d - -> required by _build/default/b/b.vo - -> required by _build/install/default/lib/coq/user-contrib/b/b.vo - -> required by _build/default/ccycle.install - -> required by %{read:ccycle.install} at dune:3 - -> required by alias default in dune:1 +We check cycles are detected + $ dune build + Error: Dependency cycle between: + theory A in A + -> theory B in B + -> theory A in A + -> required by _build/default/A/a.v.d + -> required by _build/default/A/.a.aux + -> required by alias A/all + -> required by alias default [1] diff --git a/test/blackbox-tests/test-cases/coq/compose-installed.t/A/a.v b/test/blackbox-tests/test-cases/coq/compose-installed.t/A/a.v new file mode 100644 index 000000000000..f1904cefbfc8 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-installed.t/A/a.v @@ -0,0 +1,2 @@ +From B Require Import b. +Print message. diff --git a/test/blackbox-tests/test-cases/coq/compose-installed.t/A/dune b/test/blackbox-tests/test-cases/coq/compose-installed.t/A/dune new file mode 100644 index 000000000000..90fefd9be0ec --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-installed.t/A/dune @@ -0,0 +1,3 @@ +(coq.theory + (name A) + (theories B)) diff --git a/test/blackbox-tests/test-cases/coq/compose-installed.t/A/dune-project b/test/blackbox-tests/test-cases/coq/compose-installed.t/A/dune-project new file mode 100644 index 000000000000..06314b536ad9 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-installed.t/A/dune-project @@ -0,0 +1,2 @@ +(lang dune 3.2) +(using coq 0.3) diff --git a/test/blackbox-tests/test-cases/coq/compose-installed.t/run.t b/test/blackbox-tests/test-cases/coq/compose-installed.t/run.t new file mode 100644 index 000000000000..361fdc9d64d5 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-installed.t/run.t @@ -0,0 +1,20 @@ +We test composing a project with an installed Coq theory. The installed theory +does *not* have to be a dune project. + + $ export COQLIB=. + +TODO: Currently this is not supported so the output is garbage + + $ cd A + $ dune build + File "dune", line 3, characters 11-12: + 3 | (theories B)) + ^ + Theory B not found + -> required by theory A in . + -> required by _build/default/a.v.d + -> required by _build/default/.a.aux + -> required by alias all + -> required by alias default + [1] + diff --git a/test/blackbox-tests/test-cases/coq/compose-installed.t/user-contrib/B/b.v b/test/blackbox-tests/test-cases/coq/compose-installed.t/user-contrib/B/b.v new file mode 100644 index 000000000000..54ff44b1c610 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-installed.t/user-contrib/B/b.v @@ -0,0 +1,3 @@ +From Coq Require Import String. +Local Open Scope string_scope. +Definition message := "Hello from an install location!". diff --git a/test/blackbox-tests/test-cases/coq/compose-simple.t/csimple.opam b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A/A.opam similarity index 100% rename from test/blackbox-tests/test-cases/coq/compose-simple.t/csimple.opam rename to test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A/A.opam diff --git a/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A/a.v b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A/a.v new file mode 100644 index 000000000000..ebbd6bd3ea04 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A/a.v @@ -0,0 +1,3 @@ +From Coq Require Import String. +Local Open Scope string_scope. +Definition message := "I am the the private A ". diff --git a/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A/dune b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A/dune new file mode 100644 index 000000000000..dc6e6bf392b4 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A/dune @@ -0,0 +1,3 @@ +(coq.theory + (name A)) + diff --git a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/subtheory.opam b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A_vendored/A.opam similarity index 100% rename from test/blackbox-tests/test-cases/coq/compose-sub-theory.t/subtheory.opam rename to test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A_vendored/A.opam diff --git a/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A_vendored/a.v b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A_vendored/a.v new file mode 100644 index 000000000000..01c353dd662e --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A_vendored/a.v @@ -0,0 +1,3 @@ +From Coq Require Import String. +Local Open Scope string_scope. +Definition message := "I am the vendored A". diff --git a/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A_vendored/dune b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A_vendored/dune new file mode 100644 index 000000000000..084e1edeb448 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A_vendored/dune @@ -0,0 +1,4 @@ +(coq.theory + (name A) + (package A)) + diff --git a/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A_vendored/dune-project b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A_vendored/dune-project new file mode 100644 index 000000000000..06314b536ad9 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/A_vendored/dune-project @@ -0,0 +1,2 @@ +(lang dune 3.2) +(using coq 0.3) diff --git a/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/B/b.v b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/B/b.v new file mode 100644 index 000000000000..daa1e640ee1b --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/B/b.v @@ -0,0 +1,7 @@ +From Coq Require Import String. +From A Require Import a. + +Local Open Scope string_scope. + +Print message. + diff --git a/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/B/dune b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/B/dune new file mode 100644 index 000000000000..f087163ebd4d --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/B/dune @@ -0,0 +1,3 @@ +(coq.theory + (name B) + (theories A)) diff --git a/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/C.opam b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/C.opam new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/C/c.v b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/C/c.v new file mode 100644 index 000000000000..daa1e640ee1b --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/C/c.v @@ -0,0 +1,7 @@ +From Coq Require Import String. +From A Require Import a. + +Local Open Scope string_scope. + +Print message. + diff --git a/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/C/dune b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/C/dune new file mode 100644 index 000000000000..036c18c2a371 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/C/dune @@ -0,0 +1,6 @@ +(coq.theory + (name C) + (package C) + (theories A)) + + diff --git a/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/dune-project b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/dune-project new file mode 100644 index 000000000000..06314b536ad9 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/dune-project @@ -0,0 +1,2 @@ +(lang dune 3.2) +(using coq 0.3) diff --git a/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/run.t b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/run.t new file mode 100644 index 000000000000..cc55f34adfdb --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-private-ambiguous.t/run.t @@ -0,0 +1,16 @@ +We have two theories, A and A_vendored both called A. We test which one a +private plugin B and the public package C will pick up. + +B will pick up the private one: + $ dune build B + message = "I am the the private A " + : string + +C picks up the private one too: + $ dune build C + File "C/dune", line 4, characters 11-12: + 4 | (theories A)) + ^ + Theory "A" is private, it cannot be a dependency of a public theory. You need + to associate "A" to a package. + [1] diff --git a/test/blackbox-tests/test-cases/coq/compose-private.t/A/A.opam b/test/blackbox-tests/test-cases/coq/compose-private.t/A/A.opam new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/test/blackbox-tests/test-cases/coq/compose-private.t/A/a.v b/test/blackbox-tests/test-cases/coq/compose-private.t/A/a.v new file mode 100644 index 000000000000..831752c569d8 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-private.t/A/a.v @@ -0,0 +1,2 @@ + +Inductive Hello := World | Bye. diff --git a/test/blackbox-tests/test-cases/coq/compose-private.t/A/dune b/test/blackbox-tests/test-cases/coq/compose-private.t/A/dune new file mode 100644 index 000000000000..dc6e6bf392b4 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-private.t/A/dune @@ -0,0 +1,3 @@ +(coq.theory + (name A)) + diff --git a/test/blackbox-tests/test-cases/coq/compose-private.t/B/b.v b/test/blackbox-tests/test-cases/coq/compose-private.t/B/b.v new file mode 100644 index 000000000000..5659f2682e6d --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-private.t/B/b.v @@ -0,0 +1,4 @@ +From A Require Import a. + +Check Hello. + diff --git a/test/blackbox-tests/test-cases/coq/compose-private.t/B/dune b/test/blackbox-tests/test-cases/coq/compose-private.t/B/dune new file mode 100644 index 000000000000..f087163ebd4d --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-private.t/B/dune @@ -0,0 +1,3 @@ +(coq.theory + (name B) + (theories A)) diff --git a/test/blackbox-tests/test-cases/coq/compose-private.t/C.opam b/test/blackbox-tests/test-cases/coq/compose-private.t/C.opam new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/test/blackbox-tests/test-cases/coq/compose-private.t/C/c.v b/test/blackbox-tests/test-cases/coq/compose-private.t/C/c.v new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/test/blackbox-tests/test-cases/coq/compose-private.t/C/dune b/test/blackbox-tests/test-cases/coq/compose-private.t/C/dune new file mode 100644 index 000000000000..6ddaa5c1f9a9 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-private.t/C/dune @@ -0,0 +1,4 @@ +(coq.theory + (name C) + (package C) + (theories B)) diff --git a/test/blackbox-tests/test-cases/coq/compose-private.t/dune-project b/test/blackbox-tests/test-cases/coq/compose-private.t/dune-project new file mode 100644 index 000000000000..06314b536ad9 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-private.t/dune-project @@ -0,0 +1,2 @@ +(lang dune 3.2) +(using coq 0.3) diff --git a/test/blackbox-tests/test-cases/coq/compose-private.t/run.t b/test/blackbox-tests/test-cases/coq/compose-private.t/run.t new file mode 100644 index 000000000000..02db95b3c18a --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-private.t/run.t @@ -0,0 +1,13 @@ +Testing composition of theories with two private theories and a third public +theory. As expected, the private theories build, but the public theory fails +because a public theory cannot depend on a private theory. + + $ dune build + Hello + : Set + File "C/dune", line 4, characters 11-12: + 4 | (theories B)) + ^ + Theory "B" is private, it cannot be a dependency of a public theory. You need + to associate "B" to a package. + [1] diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/A/a.v b/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/A/a.v new file mode 100644 index 000000000000..5a866abb19f3 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/A/a.v @@ -0,0 +1,10 @@ + + +Print LoadPath. +Print Prelude. + +Require Import mytheory. + +Check Hello. + + diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/A/dune b/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/A/dune new file mode 100644 index 000000000000..3057f0ae2112 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/A/dune @@ -0,0 +1,3 @@ +(coq.theory + (name A) + (theories Coq)) diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/A/dune-project b/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/A/dune-project new file mode 100644 index 000000000000..05af5ca5dce3 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/A/dune-project @@ -0,0 +1,2 @@ +(lang dune 3.3) +(using coq 0.4) diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/B/Coq/Init/Prelude.v b/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/B/Coq/Init/Prelude.v new file mode 100644 index 000000000000..e6778dee0305 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/B/Coq/Init/Prelude.v @@ -0,0 +1,2 @@ +Unset Elimination Schemes. +Inductive PrivateBootType := private_boot | private_type. diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/B/Foo.opam b/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/B/Foo.opam new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/B/Stuff/b.v b/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/B/Stuff/b.v new file mode 100644 index 000000000000..8a23f1a1419a --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/B/Stuff/b.v @@ -0,0 +1 @@ +Check private_boot. diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/B/Stuff/dune b/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/B/Stuff/dune new file mode 100644 index 000000000000..c17977370fb5 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/B/Stuff/dune @@ -0,0 +1,3 @@ + (coq.theory + (name B) + (modules b)) \ No newline at end of file diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/B/dune-project b/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/B/dune-project new file mode 100644 index 000000000000..05af5ca5dce3 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/B/dune-project @@ -0,0 +1,2 @@ +(lang dune 3.3) +(using coq 0.4) diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/Coq/Coq.opam b/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/Coq/Coq.opam new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/Coq/Init/Prelude.v b/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/Coq/Init/Prelude.v new file mode 100644 index 000000000000..9de480a5ab81 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-boot.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.t/boot/dune b/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/Coq/dune similarity index 77% rename from test/blackbox-tests/test-cases/coq/compose-boot.t/boot/dune rename to test/blackbox-tests/test-cases/coq/compose-projects-boot.t/Coq/dune index cb370c83b613..323f2d22b4b7 100644 --- a/test/blackbox-tests/test-cases/coq/compose-boot.t/boot/dune +++ b/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/Coq/dune @@ -1,7 +1,6 @@ (coq.theory (name Coq) - (package cboot) + (package Coq) (boot)) (include_subdirs qualified) - diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/Coq/dune-project b/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/Coq/dune-project new file mode 100644 index 000000000000..05af5ca5dce3 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-boot.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-projects-boot.t/Coq/mytheory.v b/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/Coq/mytheory.v new file mode 100644 index 000000000000..831752c569d8 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/Coq/mytheory.v @@ -0,0 +1,2 @@ + +Inductive Hello := World | Bye. diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/dune-workspace b/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/dune-workspace new file mode 100644 index 000000000000..7b17fb2d3089 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/dune-workspace @@ -0,0 +1 @@ +(lang dune 3.3) diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/run.t b/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/run.t new file mode 100644 index 000000000000..9924728e6baf --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/run.t @@ -0,0 +1,53 @@ +Testing composition of theories accross a dune workspace with a boot library. A +boot library must have the following: + +- Under the module prefix "Coq" +- Have a file Init/Prelude.v + +When composing with a (boot) library, every library must have -boot passed to +coqdep and coqc. + + $ 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 + +We can even have a secondary private boot library in another scope and only the +private boot library will be loaded implicitly. + + $ cat > B/Coq/dune << EOF + > (include_subdirs qualified) + > (coq.theory + > (name Coq) + > (boot)) + > EOF + + $ dune build B + private_boot + : PrivateBootType + +However if this boot library is public Dune will complain + + $ cat > B/Coq/dune << EOF + > (include_subdirs qualified) + > (coq.theory + > (name Coq) + > (package Foo) + > (boot)) + > EOF + + $ dune build B + Error: Cannot have more than one boot theory in scope: + - Coq at Coq/dune:1 + - Coq at B/Coq/dune:2 + [1] diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/A/A.opam b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/A/A.opam new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/A/a.v b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/A/a.v new file mode 100644 index 000000000000..92d80e770f16 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/A/a.v @@ -0,0 +1,3 @@ +From C Require Import c. + +Inductive Hello := World | Bye. diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/A/dune b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/A/dune new file mode 100644 index 000000000000..f8bc0053ff65 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/A/dune @@ -0,0 +1,5 @@ +(coq.theory + (name A) + (package A) + (theories C)) + diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/A/dune-project b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/A/dune-project new file mode 100644 index 000000000000..05af5ca5dce3 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/A/dune-project @@ -0,0 +1,2 @@ +(lang dune 3.3) +(using coq 0.4) diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/B/B.opam b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/B/B.opam new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/B/b.v b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/B/b.v new file mode 100644 index 000000000000..5659f2682e6d --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/B/b.v @@ -0,0 +1,4 @@ +From A Require Import a. + +Check Hello. + diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/B/dune b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/B/dune new file mode 100644 index 000000000000..d421f8800b5a --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/B/dune @@ -0,0 +1,4 @@ +(coq.theory + (name B) + (package B) + (theories A)) diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/B/dune-project b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/B/dune-project new file mode 100644 index 000000000000..05af5ca5dce3 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/B/dune-project @@ -0,0 +1,2 @@ +(lang dune 3.3) +(using coq 0.4) diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/C/C.opam b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/C/C.opam new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/C/c.v b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/C/c.v new file mode 100644 index 000000000000..b68952f12fa6 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/C/c.v @@ -0,0 +1 @@ +From B Require Import b. \ No newline at end of file diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/C/dune b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/C/dune new file mode 100644 index 000000000000..292624eb16d3 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/C/dune @@ -0,0 +1,4 @@ +(coq.theory + (name C) + (package C) + (theories B)) \ No newline at end of file diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/C/dune-project b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/C/dune-project new file mode 100644 index 000000000000..05af5ca5dce3 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/C/dune-project @@ -0,0 +1,2 @@ +(lang dune 3.3) +(using coq 0.4) diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/dune-workspace b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/dune-workspace new file mode 100644 index 000000000000..7b17fb2d3089 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/dune-workspace @@ -0,0 +1 @@ +(lang dune 3.3) diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/run.t b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/run.t new file mode 100644 index 000000000000..acf813e8090d --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/run.t @@ -0,0 +1,38 @@ +Testing composition of theories accross a dune workspace with cyclic +dependencies. + + $ dune build A + Error: Dependency cycle between: + theory A in A + -> theory B in B + -> theory C in C + -> theory A in A + -> required by _build/default/A/a.v.d + -> required by _build/default/A/.a.aux + -> required by alias A/all + -> required by alias A/default + [1] + + $ dune build B + Error: Dependency cycle between: + theory B in B + -> theory C in C + -> theory A in A + -> theory B in B + -> required by _build/default/B/b.v.d + -> required by _build/default/B/.b.aux + -> required by alias B/all + -> required by alias B/default + [1] + + $ dune build C + Error: Dependency cycle between: + theory C in C + -> theory A in A + -> theory B in B + -> theory C in C + -> required by _build/default/C/c.v.d + -> required by _build/default/C/.c.aux + -> required by alias C/all + -> required by alias C/default + [1] diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/A/A.opam b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/A/A.opam new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/A/a.v b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/A/a.v new file mode 100644 index 000000000000..831752c569d8 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/A/a.v @@ -0,0 +1,2 @@ + +Inductive Hello := World | Bye. diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/A/dune b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/A/dune new file mode 100644 index 000000000000..dc6e6bf392b4 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/A/dune @@ -0,0 +1,3 @@ +(coq.theory + (name A)) + diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/A/dune-project b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/A/dune-project new file mode 100644 index 000000000000..05af5ca5dce3 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/A/dune-project @@ -0,0 +1,2 @@ +(lang dune 3.3) +(using coq 0.4) diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/B/B.opam b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/B/B.opam new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/B/b.v b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/B/b.v new file mode 100644 index 000000000000..5659f2682e6d --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/B/b.v @@ -0,0 +1,4 @@ +From A Require Import a. + +Check Hello. + diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/B/dune b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/B/dune new file mode 100644 index 000000000000..d421f8800b5a --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/B/dune @@ -0,0 +1,4 @@ +(coq.theory + (name B) + (package B) + (theories A)) diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/B/dune-project b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/B/dune-project new file mode 100644 index 000000000000..05af5ca5dce3 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/B/dune-project @@ -0,0 +1,2 @@ +(lang dune 3.3) +(using coq 0.4) diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/C/C.opam b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/C/C.opam new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/C/c.v b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/C/c.v new file mode 100644 index 000000000000..c4484984fbef --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/C/c.v @@ -0,0 +1,2 @@ + +Check bye. diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/C/dune b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/C/dune new file mode 100644 index 000000000000..292624eb16d3 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/C/dune @@ -0,0 +1,4 @@ +(coq.theory + (name C) + (package C) + (theories B)) \ No newline at end of file diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/C/dune-project b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/C/dune-project new file mode 100644 index 000000000000..05af5ca5dce3 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/C/dune-project @@ -0,0 +1,2 @@ +(lang dune 3.3) +(using coq 0.4) diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/dune-workspace b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/dune-workspace new file mode 100644 index 000000000000..7b17fb2d3089 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/dune-workspace @@ -0,0 +1 @@ +(lang dune 3.3) diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/run.t b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/run.t new file mode 100644 index 000000000000..61d86ca1a84f --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/run.t @@ -0,0 +1,15 @@ +Testing composition of theories accross a dune workspace with a missing +dependency. + + $ dune build C + File "B/dune", line 4, characters 11-12: + 4 | (theories A)) + ^ + Theory A not found + -> required by theory B in B + -> required by theory C in C + -> required by _build/default/C/c.v.d + -> required by _build/default/C/.c.aux + -> required by alias C/all + -> required by alias C/default + [1] diff --git a/test/blackbox-tests/test-cases/coq/compose-projects.t/A/A.opam b/test/blackbox-tests/test-cases/coq/compose-projects.t/A/A.opam new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/test/blackbox-tests/test-cases/coq/compose-projects.t/A/a.v b/test/blackbox-tests/test-cases/coq/compose-projects.t/A/a.v new file mode 100644 index 000000000000..831752c569d8 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects.t/A/a.v @@ -0,0 +1,2 @@ + +Inductive Hello := World | Bye. diff --git a/test/blackbox-tests/test-cases/coq/compose-projects.t/A/dune b/test/blackbox-tests/test-cases/coq/compose-projects.t/A/dune new file mode 100644 index 000000000000..084e1edeb448 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects.t/A/dune @@ -0,0 +1,4 @@ +(coq.theory + (name A) + (package A)) + diff --git a/test/blackbox-tests/test-cases/coq/compose-projects.t/A/dune-project b/test/blackbox-tests/test-cases/coq/compose-projects.t/A/dune-project new file mode 100644 index 000000000000..05af5ca5dce3 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects.t/A/dune-project @@ -0,0 +1,2 @@ +(lang dune 3.3) +(using coq 0.4) diff --git a/test/blackbox-tests/test-cases/coq/compose-projects.t/B/b.v b/test/blackbox-tests/test-cases/coq/compose-projects.t/B/b.v new file mode 100644 index 000000000000..5659f2682e6d --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects.t/B/b.v @@ -0,0 +1,4 @@ +From A Require Import a. + +Check Hello. + diff --git a/test/blackbox-tests/test-cases/coq/compose-projects.t/B/dune b/test/blackbox-tests/test-cases/coq/compose-projects.t/B/dune new file mode 100644 index 000000000000..f087163ebd4d --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects.t/B/dune @@ -0,0 +1,3 @@ +(coq.theory + (name B) + (theories A)) diff --git a/test/blackbox-tests/test-cases/coq/compose-projects.t/B/dune-project b/test/blackbox-tests/test-cases/coq/compose-projects.t/B/dune-project new file mode 100644 index 000000000000..05af5ca5dce3 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects.t/B/dune-project @@ -0,0 +1,2 @@ +(lang dune 3.3) +(using coq 0.4) diff --git a/test/blackbox-tests/test-cases/coq/compose-projects.t/dune-workspace b/test/blackbox-tests/test-cases/coq/compose-projects.t/dune-workspace new file mode 100644 index 000000000000..0c226b5b0c6e --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects.t/dune-workspace @@ -0,0 +1 @@ +(lang dune 3.2) diff --git a/test/blackbox-tests/test-cases/coq/compose-projects.t/run.t b/test/blackbox-tests/test-cases/coq/compose-projects.t/run.t new file mode 100644 index 000000000000..9ac12fbe5ada --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-projects.t/run.t @@ -0,0 +1,10 @@ +Testing composition of theories accross a dune workspace + $ dune build B + Hello + : Set + +Inspecting the build directory + $ ls _build/default/A/a.vo + _build/default/A/a.vo + $ ls _build/default/B/b.vo + _build/default/B/b.vo diff --git a/test/blackbox-tests/test-cases/coq/compose-self.t/A/a.v b/test/blackbox-tests/test-cases/coq/compose-self.t/A/a.v new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/test/blackbox-tests/test-cases/coq/compose-self.t/A/dune b/test/blackbox-tests/test-cases/coq/compose-self.t/A/dune new file mode 100644 index 000000000000..d44a666925a7 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-self.t/A/dune @@ -0,0 +1,3 @@ +(coq.theory + (name A) + (theories A)) diff --git a/test/blackbox-tests/test-cases/coq/compose-self.t/dune-project b/test/blackbox-tests/test-cases/coq/compose-self.t/dune-project new file mode 100644 index 000000000000..06314b536ad9 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-self.t/dune-project @@ -0,0 +1,2 @@ +(lang dune 3.2) +(using coq 0.3) diff --git a/test/blackbox-tests/test-cases/coq/compose-self.t/run.t b/test/blackbox-tests/test-cases/coq/compose-self.t/run.t new file mode 100644 index 000000000000..3bb751183049 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-self.t/run.t @@ -0,0 +1,9 @@ +Composing a theory with itself should cause a cycle + $ dune build + Error: Dependency cycle between: + theory A in A + -> required by _build/default/A/a.v.d + -> required by _build/default/A/.a.aux + -> required by alias A/all + -> required by alias default + [1] diff --git a/test/blackbox-tests/test-cases/coq/compose-simple.t/a/a.v b/test/blackbox-tests/test-cases/coq/compose-simple.t/A/a.v similarity index 100% rename from test/blackbox-tests/test-cases/coq/compose-simple.t/a/a.v rename to test/blackbox-tests/test-cases/coq/compose-simple.t/A/a.v diff --git a/test/blackbox-tests/test-cases/coq/compose-simple.t/A/dune b/test/blackbox-tests/test-cases/coq/compose-simple.t/A/dune new file mode 100644 index 000000000000..86ee2ef8f61e --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-simple.t/A/dune @@ -0,0 +1,3 @@ +(coq.theory + (name A) + (package Simple)) diff --git a/test/blackbox-tests/test-cases/coq/compose-simple.t/b/b.v b/test/blackbox-tests/test-cases/coq/compose-simple.t/B/b.v similarity index 50% rename from test/blackbox-tests/test-cases/coq/compose-simple.t/b/b.v rename to test/blackbox-tests/test-cases/coq/compose-simple.t/B/b.v index e184683b4d42..951f7a4ee5ef 100644 --- a/test/blackbox-tests/test-cases/coq/compose-simple.t/b/b.v +++ b/test/blackbox-tests/test-cases/coq/compose-simple.t/B/b.v @@ -1,3 +1,3 @@ -From a Require Import a. +From A Require Import a. Definition bar := a.foo. diff --git a/test/blackbox-tests/test-cases/coq/compose-simple.t/B/dune b/test/blackbox-tests/test-cases/coq/compose-simple.t/B/dune new file mode 100644 index 000000000000..7893d7c9e63e --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-simple.t/B/dune @@ -0,0 +1,4 @@ +(coq.theory + (name B) + (package Simple) + (theories A)) diff --git a/test/blackbox-tests/test-cases/coq/compose-simple.t/Simple.opam b/test/blackbox-tests/test-cases/coq/compose-simple.t/Simple.opam new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/test/blackbox-tests/test-cases/coq/compose-simple.t/a/dune b/test/blackbox-tests/test-cases/coq/compose-simple.t/a/dune deleted file mode 100644 index 099b8f56a24d..000000000000 --- a/test/blackbox-tests/test-cases/coq/compose-simple.t/a/dune +++ /dev/null @@ -1,3 +0,0 @@ -(coq.theory - (name a) - (package csimple)) diff --git a/test/blackbox-tests/test-cases/coq/compose-simple.t/b/dune b/test/blackbox-tests/test-cases/coq/compose-simple.t/b/dune deleted file mode 100644 index e4edf23190e7..000000000000 --- a/test/blackbox-tests/test-cases/coq/compose-simple.t/b/dune +++ /dev/null @@ -1,4 +0,0 @@ -(coq.theory - (name b) - (package csimple) - (theories a)) diff --git a/test/blackbox-tests/test-cases/coq/compose-simple.t/dune b/test/blackbox-tests/test-cases/coq/compose-simple.t/dune deleted file mode 100644 index f7a7db897dbd..000000000000 --- a/test/blackbox-tests/test-cases/coq/compose-simple.t/dune +++ /dev/null @@ -1,3 +0,0 @@ -(rule - (alias default) - (action (echo "%{read:csimple.install}"))) diff --git a/test/blackbox-tests/test-cases/coq/compose-simple.t/dune-project b/test/blackbox-tests/test-cases/coq/compose-simple.t/dune-project index 9ef6b81a34a1..06314b536ad9 100644 --- a/test/blackbox-tests/test-cases/coq/compose-simple.t/dune-project +++ b/test/blackbox-tests/test-cases/coq/compose-simple.t/dune-project @@ -1,3 +1,2 @@ -(lang dune 2.5) - -(using coq 0.2) +(lang dune 3.2) +(using coq 0.3) diff --git a/test/blackbox-tests/test-cases/coq/compose-simple.t/run.t b/test/blackbox-tests/test-cases/coq/compose-simple.t/run.t index d1626e74578f..b8ceff6e6393 100644 --- a/test/blackbox-tests/test-cases/coq/compose-simple.t/run.t +++ b/test/blackbox-tests/test-cases/coq/compose-simple.t/run.t @@ -1,16 +1,15 @@ - $ dune build --display short --debug-dependency-path - coqdep a/a.v.d - coqdep b/b.v.d - coqc a/.a.aux,a/a.{glob,vo} - coqc b/.b.aux,b/b.{glob,vo} - lib: [ - "_build/install/default/lib/csimple/META" - "_build/install/default/lib/csimple/dune-package" - "_build/install/default/lib/csimple/opam" - ] - lib_root: [ - "_build/install/default/lib/coq/user-contrib/a/a.v" {"coq/user-contrib/a/a.v"} - "_build/install/default/lib/coq/user-contrib/a/a.vo" {"coq/user-contrib/a/a.vo"} - "_build/install/default/lib/coq/user-contrib/b/b.v" {"coq/user-contrib/b/b.v"} - "_build/install/default/lib/coq/user-contrib/b/b.vo" {"coq/user-contrib/b/b.vo"} - ] +Testing a simple composition of theories. We have two theories A and B and B +depends on A. + + $ dune build + +We inspect the contents of the build directory. + + $ ls _build/install/default/lib/coq/user-contrib/A/a.vo + _build/install/default/lib/coq/user-contrib/A/a.vo + $ ls _build/default/A/a.vo + _build/default/A/a.vo + $ ls _build/install/default/lib/coq/user-contrib/B/b.vo + _build/install/default/lib/coq/user-contrib/B/b.vo + $ ls _build/default/B/b.vo + _build/default/B/b.vo diff --git a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/a/a.v b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/A/a.v similarity index 100% rename from test/blackbox-tests/test-cases/coq/compose-sub-theory.t/a/a.v rename to test/blackbox-tests/test-cases/coq/compose-sub-theory.t/A/a.v diff --git a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/A/dune b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/A/dune new file mode 100644 index 000000000000..237bfa399e64 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/A/dune @@ -0,0 +1,3 @@ +(coq.theory + (name Foo.A) + (package Subtheory)) diff --git a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/B/b.v b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/B/b.v new file mode 100644 index 000000000000..1379965e9ff3 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/B/b.v @@ -0,0 +1,3 @@ +From Foo Require Import a. + +Definition bar := a.foo. diff --git a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/B/dune b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/B/dune new file mode 100644 index 000000000000..d2d6fca00241 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/B/dune @@ -0,0 +1,4 @@ +(coq.theory + (name B) + (package Subtheory) + (theories Foo.A)) diff --git a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/Subtheory.opam b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/Subtheory.opam new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/a/dune b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/a/dune deleted file mode 100644 index d34c322f227e..000000000000 --- a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/a/dune +++ /dev/null @@ -1,3 +0,0 @@ -(coq.theory - (name foo.a) - (package subtheory)) diff --git a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/b/b.v b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/b/b.v deleted file mode 100644 index fc1eff1cce39..000000000000 --- a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/b/b.v +++ /dev/null @@ -1,3 +0,0 @@ -From foo Require Import a. - -Definition bar := a.foo. diff --git a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/b/dune b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/b/dune deleted file mode 100644 index 3ed0a09517cd..000000000000 --- a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/b/dune +++ /dev/null @@ -1,4 +0,0 @@ -(coq.theory - (name b) - (package subtheory) - (theories foo.a)) diff --git a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/dune b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/dune deleted file mode 100644 index 5ee910867dec..000000000000 --- a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/dune +++ /dev/null @@ -1,3 +0,0 @@ -(rule - (alias default) - (action (echo "%{read:subtheory.install}"))) diff --git a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/dune-project b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/dune-project index d18101b40de2..06314b536ad9 100644 --- a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/dune-project +++ b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/dune-project @@ -1,2 +1,2 @@ -(lang dune 2.5) -(using coq 0.2) +(lang dune 3.2) +(using coq 0.3) diff --git a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/run.t b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/run.t index 8f1321b1291c..2aa94afdd27b 100644 --- a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/run.t +++ b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/run.t @@ -1,16 +1,14 @@ - $ dune build --display short --debug-dependency-path - coqdep b/b.v.d - coqdep a/a.v.d - coqc a/.a.aux,a/a.{glob,vo} - coqc b/.b.aux,b/b.{glob,vo} - lib: [ - "_build/install/default/lib/subtheory/META" - "_build/install/default/lib/subtheory/dune-package" - "_build/install/default/lib/subtheory/opam" - ] - lib_root: [ - "_build/install/default/lib/coq/user-contrib/b/b.v" {"coq/user-contrib/b/b.v"} - "_build/install/default/lib/coq/user-contrib/b/b.vo" {"coq/user-contrib/b/b.vo"} - "_build/install/default/lib/coq/user-contrib/foo/a/a.v" {"coq/user-contrib/foo/a/a.v"} - "_build/install/default/lib/coq/user-contrib/foo/a/a.vo" {"coq/user-contrib/foo/a/a.vo"} - ] +Testing dependencies on subtheories. We have two theories A and B, but A is +defined as Foo.A. This changes the install layout of A. + + $ dune build + +Inspecting the build and install directory + $ ls _build/install/default/lib/coq/user-contrib/Foo/A/a.vo + _build/install/default/lib/coq/user-contrib/Foo/A/a.vo + $ ls _build/default/A/a.vo + _build/default/A/a.vo + $ ls _build/install/default/lib/coq/user-contrib/B/b.vo + _build/install/default/lib/coq/user-contrib/B/b.vo + $ ls _build/default/B/b.vo + _build/default/B/b.vo diff --git a/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/dune-project b/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/dune-project index 9ef6b81a34a1..05af5ca5dce3 100644 --- a/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/dune-project +++ b/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/dune-project @@ -1,3 +1,2 @@ -(lang dune 2.5) - -(using coq 0.2) +(lang dune 3.3) +(using coq 0.4) diff --git a/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/run.t b/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/run.t index 0285fd613ea8..d47473520f3c 100644 --- a/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/run.t +++ b/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/run.t @@ -1,12 +1,11 @@ - $ dune build --debug-dependency-path - File "b/dune", line 4, characters 11-12: - 4 | (theories a)) - ^ - Error: Theory a not found - -> required by _build/default/b/b.v.d - -> required by _build/default/b/b.vo - -> required by _build/install/default/lib/coq/user-contrib/b/b.vo - -> required by _build/default/cvendor.install - -> required by %{read:cvendor.install} at dune:3 - -> required by alias default in dune:1 - [1] + + $ dune build + lib: [ + "_build/install/default/lib/cvendor/META" + "_build/install/default/lib/cvendor/dune-package" + "_build/install/default/lib/cvendor/opam" + ] + lib_root: [ + "_build/install/default/lib/coq/user-contrib/b/b.v" {"coq/user-contrib/b/b.v"} + "_build/install/default/lib/coq/user-contrib/b/b.vo" {"coq/user-contrib/b/b.vo"} + ] diff --git a/test/blackbox-tests/test-cases/coq/github3624.t b/test/blackbox-tests/test-cases/coq/github3624.t index 1a2899d945cb..c11352e9680f 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.3) in your dune-project file. + file. You must enable it using (using coq 0.4) in your dune-project file. [1] diff --git a/test/blackbox-tests/test-cases/coq/public-dep-on-private.t/run.t b/test/blackbox-tests/test-cases/coq/public-dep-on-private.t/run.t index 09dac49026d7..785e823b623a 100644 --- a/test/blackbox-tests/test-cases/coq/public-dep-on-private.t/run.t +++ b/test/blackbox-tests/test-cases/coq/public-dep-on-private.t/run.t @@ -2,8 +2,9 @@ File "public/dune", line 4, characters 11-18: 4 | (theories private)) ^^^^^^^ - Error: Theory "private" is private, it cannot be a dependency of a public - theory. You need to associate "private" to a package. + Theory "private" is private, it cannot be a dependency of a public theory. + You need to associate "private" to a package. + -> required by theory public in public -> required by _build/default/public/b.v.d -> required by _build/default/public/b.vo -> required by _build/install/default/lib/coq/user-contrib/public/b.vo