From ddd8f66677d51a6f4467d01c7d8b9902c16fea06 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 11 Jun 2022 13:10:42 +0200 Subject: [PATCH] [coq_lib] Enforce that boot libraries depend on no theories Signed-off-by: Emilio Jesus Gallego Arias --- src/dune_rules/coq_stanza.ml | 12 ++++++++++++ .../test-cases/coq/compose-boot-nodeps.t/A/A.opam | 0 .../test-cases/coq/compose-boot-nodeps.t/A/a.v | 1 + .../test-cases/coq/compose-boot-nodeps.t/A/dune | 5 +++++ .../coq/compose-boot-nodeps.t/A/dune-project | 3 +++ .../test-cases/coq/compose-boot-nodeps.t/B/B.opam | 0 .../test-cases/coq/compose-boot-nodeps.t/B/b.v | 1 + .../test-cases/coq/compose-boot-nodeps.t/B/dune | 5 +++++ .../coq/compose-boot-nodeps.t/B/dune-project | 3 +++ .../coq/compose-boot-nodeps.t/dune-workspace | 1 + .../test-cases/coq/compose-boot-nodeps.t/run.t | 8 ++++++++ 11 files changed, 39 insertions(+) create mode 100644 test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/A/A.opam create mode 100644 test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/A/a.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/A/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/A/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/B/B.opam create mode 100644 test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/B/b.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/B/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/B/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/dune-workspace create mode 100644 test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/run.t diff --git a/src/dune_rules/coq_stanza.ml b/src/dune_rules/coq_stanza.ml index 93de0b1beda3..22d0371254f6 100644 --- a/src/dune_rules/coq_stanza.ml +++ b/src/dune_rules/coq_stanza.ml @@ -133,6 +133,16 @@ module Theory = struct 1.0 version of the Coq language" ] + let boot_has_deps loc = + User_error.raise ~loc + [ Pp.textf "(boot) libraries cannot have dependencies" ] + + let check_boot_has_no_deps boot { Buildable.theories; _ } = + if boot then + match theories with + | [] -> () + | (loc, _) :: _ -> boot_has_deps loc + let decode = fields (let+ loc, name = field "name" Coq_lib_name.decode @@ -145,6 +155,8 @@ module Theory = struct and+ modules = Stanza_common.modules_field "modules" and+ enabled_if = Enabled_if.decode ~allowed_vars:Any ~since:None () and+ buildable = Buildable.decode in + (* boot libraries cannot depend on other theories *) + check_boot_has_no_deps boot buildable; let package = select_deprecation ~package ~public in { loc ; name diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/A/A.opam b/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/A/A.opam new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/A/a.v b/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/A/a.v new file mode 100644 index 000000000000..8089bf38ce4c --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/A/a.v @@ -0,0 +1 @@ +Inductive AnotherBegining := Of | The | Universe. diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/A/dune b/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/A/dune new file mode 100644 index 000000000000..dfe57b7234e7 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/A/dune @@ -0,0 +1,5 @@ +(coq.theory + (name A) + (package A) + (theories B) + (boot)) diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/A/dune-project b/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/A/dune-project new file mode 100644 index 000000000000..9ef6b81a34a1 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/A/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-nodeps.t/B/B.opam b/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/B/B.opam new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/B/b.v b/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/B/b.v new file mode 100644 index 000000000000..46e4b397d40e --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/B/b.v @@ -0,0 +1 @@ +Inductive Begining := Of | The | Universe. diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/B/dune b/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/B/dune new file mode 100644 index 000000000000..d357edca3062 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/B/dune @@ -0,0 +1,5 @@ +(coq.theory + (name B) + (package B)) + + diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/B/dune-project b/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/B/dune-project new file mode 100644 index 000000000000..9ef6b81a34a1 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.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-nodeps.t/dune-workspace b/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/dune-workspace new file mode 100644 index 000000000000..0c226b5b0c6e --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/dune-workspace @@ -0,0 +1 @@ +(lang dune 3.2) diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/run.t b/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/run.t new file mode 100644 index 000000000000..7418f4cec856 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/run.t @@ -0,0 +1,8 @@ +Testing composition with two boot libraries + + $ dune build + File "A/dune", line 4, characters 11-12: + 4 | (theories B) + ^ + Error: (boot) libraries cannot have dependencies + [1]