[coq] [test] Add test for missing plugins flags from boot (issue intr…

…oduced in ocaml#5866)
ejgallego · Sep 27, 2022 · 957a705 · 957a705
1 parent 63ad40f
commit 957a705
Show file tree

Hide file tree

Showing 21 changed files with 32 additions and 26 deletions.
diff --git a/...ts/test-cases/coq/compose-boot.t/A/A.opam → .../compose-boot-plugins.t/Coq/coq-boot.opam b/...ts/test-cases/coq/compose-boot.t/A/A.opam → .../compose-boot-plugins.t/Coq/coq-boot.opam
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/Coq/dune-project b/test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/Coq/dune-project
@@ -0,0 +1,3 @@
+(lang dune 3.4)
+
+(using coq 0.5)
diff --git a/...ts/test-cases/coq/compose-boot.t/B/B.opam → ...-plugins.t/Coq/plugins/boot_plugin.mlpack b/...ts/test-cases/coq/compose-boot.t/B/B.opam → ...-plugins.t/Coq/plugins/boot_plugin.mlpack
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/Coq/plugins/dune b/test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/Coq/plugins/dune
@@ -0,0 +1,4 @@
+(library
+ (name boot_plugin)
+ (public_name coq-boot.boot_plugin))
+
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/Coq/plugins/main.ml b/test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/Coq/plugins/main.ml
@@ -0,0 +1 @@
+let () = Format.eprintf "plugin loaded@\n%!"
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/Coq/theories/Init/Prelude.v b/test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/Coq/theories/Init/Prelude.v
@@ -0,0 +1,2 @@
+Declare ML Module "boot_plugin:coq-boot.boot_plugin".
+Inductive AnotherBegining := Of | The | Universe.
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/Coq/theories/dune b/test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/Coq/theories/dune
@@ -0,0 +1,7 @@
+(coq.theory
+ (name Coq)
+ (boot)
+ (package coq-boot)
+ (plugins coq-boot.boot_plugin))
+
+(include_subdirs qualified)
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/User/coq-user.opam b/test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/User/coq-user.opam
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/User/dune b/test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/User/dune
@@ -0,0 +1,5 @@
+(coq.theory
+ (name User)
+ (package coq-user))
+
+
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/User/dune-project b/test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/User/dune-project
@@ -0,0 +1,3 @@
+(lang dune 3.4)
+
+(using coq 0.5)
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/User/user.v b/test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/User/user.v
@@ -0,0 +1 @@
+Definition from_boot : AnotherBegining := Universe.
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/dune-workspace b/test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/dune-workspace
@@ -0,0 +1 @@
+(lang dune 3.4)
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/run.t b/test/blackbox-tests/test-cases/coq/compose-boot-plugins.t/run.t
@@ -0,0 +1,5 @@
+Testing composition with a boot library with plugins
+
+  $ dune build
+  plugin loaded
+  plugin loaded
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
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
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot.t/A/dune-project b/test/blackbox-tests/test-cases/coq/compose-boot.t/A/dune-project
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
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
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
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
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
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		Declare ML Module "boot_plugin:coq-boot.boot_plugin".
		Inductive AnotherBegining := Of \| The \| Universe.
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		Definition from_boot : AnotherBegining := Universe.