From d2869057d75d78142deb7d04fc8e659c48a4b661 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 30 May 2024 15:21:59 +0200 Subject: [PATCH] [coq] [fix] Install .glob files This seems like an omission from the beginning, I'm surprised this wasn't a problem for anyone until now. Signed-off-by: Emilio Jesus Gallego Arias --- doc/changes/10602.md | 1 + src/dune_rules/coq/coq_module.ml | 19 ++++++++++++------- .../test-cases/coq/base.t/run.t | 2 ++ .../coq/compose-installed-compat.t/run.t | 1 + .../coq/compose-installed-rebuild.t/run.t | 6 ++++++ .../coq/compose-installed-sub.t/run.t | 8 ++++++++ .../test-cases/coq/compose-installed.t/run.t | 4 ++++ .../test-cases/coq/compose-two-scopes.t/run.t | 1 + .../test-cases/coq/config-no-coqc.t/run.t | 6 +++--- .../test-cases/coq/native-compose.t/run.t | 3 +++ .../test-cases/coq/native-single.t/run.t | 2 ++ .../test-cases/coq/per_file_flags.t/run.t | 2 ++ .../coq/public-dep-on-private.t/run.t | 5 ++--- .../test-cases/coq/rec-module.t/run.t | 4 ++++ .../test-cases/coq/vos-build.t/run.t | 2 ++ 15 files changed, 53 insertions(+), 13 deletions(-) create mode 100644 doc/changes/10602.md diff --git a/doc/changes/10602.md b/doc/changes/10602.md new file mode 100644 index 00000000000..4dd61882fd7 --- /dev/null +++ b/doc/changes/10602.md @@ -0,0 +1 @@ +- install `.glob` files for Coq theories too (#10602, @ejgallego) diff --git a/src/dune_rules/coq/coq_module.ml b/src/dune_rules/coq/coq_module.ml index d302d466773..2ef2d8abff8 100644 --- a/src/dune_rules/coq/coq_module.ml +++ b/src/dune_rules/coq/coq_module.ml @@ -76,6 +76,17 @@ let glob_file x ~obj_dir = Path.Build.relative vo_dir (x.name ^ ".glob") ;; +(* As of today we do the same for build and install, it used not to be + the case *) +let standard_obj_files ~(mode : Coq_mode.t) _obj_files_mode name = + let ext, glob = + match mode with + | VosOnly -> ".vos", [] + | _ -> ".vo", [ name ^ ".glob" ] + in + [ name ^ ext ] @ glob +;; + (* XXX: Remove the install .coq-native hack once rules can output targets in multiple subdirs *) let obj_files x ~wrapper_name ~mode ~obj_dir ~obj_files_mode = @@ -92,13 +103,7 @@ let obj_files x ~wrapper_name ~mode ~obj_dir ~obj_files_mode = cmxs_obj | VoOnly | VosOnly | Legacy -> [] in - let obj_files = - match obj_files_mode with - | Build when mode = VosOnly -> [ x.name ^ ".vos" ] - | Build -> [ x.name ^ ".vo"; x.name ^ ".glob" ] - | Install when mode = VosOnly -> [ x.name ^ ".vos" ] - | Install -> [ x.name ^ ".vo" ] - in + let obj_files = standard_obj_files ~mode obj_files_mode x.name in List.map obj_files ~f:(fun fname -> Path.Build.relative vo_dir fname, Filename.concat install_vo_dir fname) @ native_objs diff --git a/test/blackbox-tests/test-cases/coq/base.t/run.t b/test/blackbox-tests/test-cases/coq/base.t/run.t index 2f58777b258..b1099f31562 100644 --- a/test/blackbox-tests/test-cases/coq/base.t/run.t +++ b/test/blackbox-tests/test-cases/coq/base.t/run.t @@ -18,8 +18,10 @@ "_build/install/default/lib/base/opam" ] lib_root: [ + "_build/install/default/lib/coq/user-contrib/basic/bar.glob" {"coq/user-contrib/basic/bar.glob"} "_build/install/default/lib/coq/user-contrib/basic/bar.v" {"coq/user-contrib/basic/bar.v"} "_build/install/default/lib/coq/user-contrib/basic/bar.vo" {"coq/user-contrib/basic/bar.vo"} + "_build/install/default/lib/coq/user-contrib/basic/foo.glob" {"coq/user-contrib/basic/foo.glob"} "_build/install/default/lib/coq/user-contrib/basic/foo.v" {"coq/user-contrib/basic/foo.v"} "_build/install/default/lib/coq/user-contrib/basic/foo.vo" {"coq/user-contrib/basic/foo.vo"} ] diff --git a/test/blackbox-tests/test-cases/coq/compose-installed-compat.t/run.t b/test/blackbox-tests/test-cases/coq/compose-installed-compat.t/run.t index ba684bf7759..0033bbfc8bd 100644 --- a/test/blackbox-tests/test-cases/coq/compose-installed-compat.t/run.t +++ b/test/blackbox-tests/test-cases/coq/compose-installed-compat.t/run.t @@ -40,6 +40,7 @@ so this also tests that it won't be a problem. Installing $TESTCASE_ROOT/lib/B/dune-package Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_b.cmi Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_b.cmxs + Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.glob Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.v Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.vo diff --git a/test/blackbox-tests/test-cases/coq/compose-installed-rebuild.t/run.t b/test/blackbox-tests/test-cases/coq/compose-installed-rebuild.t/run.t index 74cfe9c741c..5f67f47b741 100644 --- a/test/blackbox-tests/test-cases/coq/compose-installed-rebuild.t/run.t +++ b/test/blackbox-tests/test-cases/coq/compose-installed-rebuild.t/run.t @@ -33,6 +33,7 @@ so this also tests that it won't be a problem. Installing $TESTCASE_ROOT/lib/B/dune-package Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_b.cmi Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_b.cmxs + Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.glob Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.v Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.vo @@ -62,6 +63,8 @@ Next we update B and install it again. Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_b.cmi Deleting $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_b.cmxs Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_b.cmxs + Deleting $TESTCASE_ROOT/lib/coq/user-contrib/B/b.glob + Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.glob Deleting $TESTCASE_ROOT/lib/coq/user-contrib/B/b.v Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.v Deleting $TESTCASE_ROOT/lib/coq/user-contrib/B/b.vo @@ -101,10 +104,13 @@ Next we add a new file to B that should cause a call to coqdep, but no rebuild. Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_b.cmxs Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_c.cmi Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_c.cmxs + Deleting $TESTCASE_ROOT/lib/coq/user-contrib/B/b.glob + Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.glob Deleting $TESTCASE_ROOT/lib/coq/user-contrib/B/b.v Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.v Deleting $TESTCASE_ROOT/lib/coq/user-contrib/B/b.vo Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.vo + Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/c.glob Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/c.v Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/c.vo diff --git a/test/blackbox-tests/test-cases/coq/compose-installed-sub.t/run.t b/test/blackbox-tests/test-cases/coq/compose-installed-sub.t/run.t index 6f5ec1ae38c..cbb1eedfb94 100644 --- a/test/blackbox-tests/test-cases/coq/compose-installed-sub.t/run.t +++ b/test/blackbox-tests/test-cases/coq/compose-installed-sub.t/run.t @@ -42,10 +42,12 @@ so this also tests that it won't be a problem. Installing $TESTCASE_ROOT/lib/global/dune-package Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/algebra/.coq-native/Nglobal_algebra_b_alg.cmi Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/algebra/.coq-native/Nglobal_algebra_b_alg.cmxs + Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/algebra/b_alg.glob Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/algebra/b_alg.v Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/algebra/b_alg.vo Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/field/.coq-native/Nglobal_field_b_field.cmi Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/field/.coq-native/Nglobal_field_b_field.cmxs + Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/field/b_field.glob Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/field/b_field.v Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/field/b_field.vo @@ -76,10 +78,12 @@ somewhere else. Deleting $TESTCASE_ROOT/lib/global/dune-package Deleting $TESTCASE_ROOT/lib/coq/user-contrib/global/algebra/.coq-native/Nglobal_algebra_b_alg.cmi Deleting $TESTCASE_ROOT/lib/coq/user-contrib/global/algebra/.coq-native/Nglobal_algebra_b_alg.cmxs + Deleting $TESTCASE_ROOT/lib/coq/user-contrib/global/algebra/b_alg.glob Deleting $TESTCASE_ROOT/lib/coq/user-contrib/global/algebra/b_alg.v Deleting $TESTCASE_ROOT/lib/coq/user-contrib/global/algebra/b_alg.vo Deleting $TESTCASE_ROOT/lib/coq/user-contrib/global/field/.coq-native/Nglobal_field_b_field.cmi Deleting $TESTCASE_ROOT/lib/coq/user-contrib/global/field/.coq-native/Nglobal_field_b_field.cmxs + Deleting $TESTCASE_ROOT/lib/coq/user-contrib/global/field/b_field.glob Deleting $TESTCASE_ROOT/lib/coq/user-contrib/global/field/b_field.v Deleting $TESTCASE_ROOT/lib/coq/user-contrib/global/field/b_field.vo Deleting empty directory $TESTCASE_ROOT/lib/global @@ -93,10 +97,12 @@ somewhere else. Installing $TESTCASE_ROOT/another-place/lib/global/dune-package Installing $TESTCASE_ROOT/another-place/lib/coq/user-contrib/global/algebra/.coq-native/Nglobal_algebra_b_alg.cmi Installing $TESTCASE_ROOT/another-place/lib/coq/user-contrib/global/algebra/.coq-native/Nglobal_algebra_b_alg.cmxs + Installing $TESTCASE_ROOT/another-place/lib/coq/user-contrib/global/algebra/b_alg.glob Installing $TESTCASE_ROOT/another-place/lib/coq/user-contrib/global/algebra/b_alg.v Installing $TESTCASE_ROOT/another-place/lib/coq/user-contrib/global/algebra/b_alg.vo Installing $TESTCASE_ROOT/another-place/lib/coq/user-contrib/global/field/.coq-native/Nglobal_field_b_field.cmi Installing $TESTCASE_ROOT/another-place/lib/coq/user-contrib/global/field/.coq-native/Nglobal_field_b_field.cmxs + Installing $TESTCASE_ROOT/another-place/lib/coq/user-contrib/global/field/b_field.glob Installing $TESTCASE_ROOT/another-place/lib/coq/user-contrib/global/field/b_field.v Installing $TESTCASE_ROOT/another-place/lib/coq/user-contrib/global/field/b_field.vo $ rmdir lib/coq/user-contrib/global @@ -195,10 +201,12 @@ with the loadpath semantics of Coq. Installing $TESTCASE_ROOT/lib/global/dune-package Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/algebra/.coq-native/Nglobal_algebra_b_alg.cmi Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/algebra/.coq-native/Nglobal_algebra_b_alg.cmxs + Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/algebra/b_alg.glob Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/algebra/b_alg.v Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/algebra/b_alg.vo Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/field/.coq-native/Nglobal_field_b_field.cmi Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/field/.coq-native/Nglobal_field_b_field.cmxs + Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/field/b_field.glob Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/field/b_field.v Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/field/b_field.vo 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 index af02c8cc5d4..68a129f7a8d 100644 --- a/test/blackbox-tests/test-cases/coq/compose-installed.t/run.t +++ b/test/blackbox-tests/test-cases/coq/compose-installed.t/run.t @@ -34,6 +34,7 @@ so this also tests that it won't be a problem. Installing $TESTCASE_ROOT/lib/B/dune-package Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_b.cmi Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_b.cmxs + Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.glob Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.v Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.vo @@ -52,6 +53,7 @@ somewhere else. Deleting $TESTCASE_ROOT/lib/B/dune-package Deleting $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_b.cmi Deleting $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_b.cmxs + Deleting $TESTCASE_ROOT/lib/coq/user-contrib/B/b.glob Deleting $TESTCASE_ROOT/lib/coq/user-contrib/B/b.v Deleting $TESTCASE_ROOT/lib/coq/user-contrib/B/b.vo Deleting empty directory $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native @@ -63,6 +65,7 @@ somewhere else. Installing $TESTCASE_ROOT/another-place/lib/B/dune-package Installing $TESTCASE_ROOT/another-place/lib/coq/user-contrib/B/.coq-native/NB_b.cmi Installing $TESTCASE_ROOT/another-place/lib/coq/user-contrib/B/.coq-native/NB_b.cmxs + Installing $TESTCASE_ROOT/another-place/lib/coq/user-contrib/B/b.glob Installing $TESTCASE_ROOT/another-place/lib/coq/user-contrib/B/b.v Installing $TESTCASE_ROOT/another-place/lib/coq/user-contrib/B/b.vo @@ -111,6 +114,7 @@ with the loadpath semantics of Coq. Installing $TESTCASE_ROOT/lib/B/dune-package Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_b.cmi Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_b.cmxs + Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.glob Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.v Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.vo 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 5437e0982c5..7ef87258577 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 @@ -10,6 +10,7 @@ "_build/install/default/lib/cvendor/opam" ] lib_root: [ + "_build/install/default/lib/coq/user-contrib/b/b.glob" {"coq/user-contrib/b/b.glob"} "_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/config-no-coqc.t/run.t b/test/blackbox-tests/test-cases/coq/config-no-coqc.t/run.t index 6e7515cdcde..3c21911f8f7 100644 --- a/test/blackbox-tests/test-cases/coq/config-no-coqc.t/run.t +++ b/test/blackbox-tests/test-cases/coq/config-no-coqc.t/run.t @@ -51,6 +51,7 @@ We first test the package builds as normal, when both are in scope: "_build/install/default/lib/example-coq/opam" ] lib_root: [ + "_build/install/default/lib/coq/user-contrib/Common/Foo.glob" {"coq/user-contrib/Common/Foo.glob"} "_build/install/default/lib/coq/user-contrib/Common/Foo.v" {"coq/user-contrib/Common/Foo.v"} "_build/install/default/lib/coq/user-contrib/Common/Foo.vo" {"coq/user-contrib/Common/Foo.vo"} ] @@ -112,9 +113,8 @@ Coq package should fail: $ (unset INSIDE_DUNE; PATH=_path dune build -p example-coq) Couldn't find Coq standard library, and theory is not using (stdlib no) - -> required by _build/default/coq/extracted/CRelationClasses.ml - -> required by _build/default/coq/CRelationClasses.ml - -> required by _build/install/default/lib/example-coq/coq/CRelationClasses.ml + -> required by _build/default/coq/Common/Foo.glob + -> required by _build/install/default/lib/coq/user-contrib/Common/Foo.glob -> required by _build/default/example-coq.install -> required by alias install [1] diff --git a/test/blackbox-tests/test-cases/coq/native-compose.t/run.t b/test/blackbox-tests/test-cases/coq/native-compose.t/run.t index 4aa5086b7ce..e88c373c1e3 100644 --- a/test/blackbox-tests/test-cases/coq/native-compose.t/run.t +++ b/test/blackbox-tests/test-cases/coq/native-compose.t/run.t @@ -22,14 +22,17 @@ lib_root: [ "_build/install/default/lib/coq/user-contrib/bar/baz/.coq-native/Nbar_baz_bar.cmi" {"coq/user-contrib/bar/baz/.coq-native/Nbar_baz_bar.cmi"} "_build/install/default/lib/coq/user-contrib/bar/baz/.coq-native/Nbar_baz_bar.cmxs" {"coq/user-contrib/bar/baz/.coq-native/Nbar_baz_bar.cmxs"} + "_build/install/default/lib/coq/user-contrib/bar/baz/bar.glob" {"coq/user-contrib/bar/baz/bar.glob"} "_build/install/default/lib/coq/user-contrib/bar/baz/bar.v" {"coq/user-contrib/bar/baz/bar.v"} "_build/install/default/lib/coq/user-contrib/bar/baz/bar.vo" {"coq/user-contrib/bar/baz/bar.vo"} "_build/install/default/lib/coq/user-contrib/foo/.coq-native/Nfoo_foo.cmi" {"coq/user-contrib/foo/.coq-native/Nfoo_foo.cmi"} "_build/install/default/lib/coq/user-contrib/foo/.coq-native/Nfoo_foo.cmxs" {"coq/user-contrib/foo/.coq-native/Nfoo_foo.cmxs"} "_build/install/default/lib/coq/user-contrib/foo/a/.coq-native/Nfoo_a_a.cmi" {"coq/user-contrib/foo/a/.coq-native/Nfoo_a_a.cmi"} "_build/install/default/lib/coq/user-contrib/foo/a/.coq-native/Nfoo_a_a.cmxs" {"coq/user-contrib/foo/a/.coq-native/Nfoo_a_a.cmxs"} + "_build/install/default/lib/coq/user-contrib/foo/a/a.glob" {"coq/user-contrib/foo/a/a.glob"} "_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"} + "_build/install/default/lib/coq/user-contrib/foo/foo.glob" {"coq/user-contrib/foo/foo.glob"} "_build/install/default/lib/coq/user-contrib/foo/foo.v" {"coq/user-contrib/foo/foo.v"} "_build/install/default/lib/coq/user-contrib/foo/foo.vo" {"coq/user-contrib/foo/foo.vo"} ] diff --git a/test/blackbox-tests/test-cases/coq/native-single.t/run.t b/test/blackbox-tests/test-cases/coq/native-single.t/run.t index f5c43a4220b..d802b64ce8e 100644 --- a/test/blackbox-tests/test-cases/coq/native-single.t/run.t +++ b/test/blackbox-tests/test-cases/coq/native-single.t/run.t @@ -22,8 +22,10 @@ "_build/install/default/lib/coq/user-contrib/basic/.coq-native/Nbasic_bar.cmxs" {"coq/user-contrib/basic/.coq-native/Nbasic_bar.cmxs"} "_build/install/default/lib/coq/user-contrib/basic/.coq-native/Nbasic_foo.cmi" {"coq/user-contrib/basic/.coq-native/Nbasic_foo.cmi"} "_build/install/default/lib/coq/user-contrib/basic/.coq-native/Nbasic_foo.cmxs" {"coq/user-contrib/basic/.coq-native/Nbasic_foo.cmxs"} + "_build/install/default/lib/coq/user-contrib/basic/bar.glob" {"coq/user-contrib/basic/bar.glob"} "_build/install/default/lib/coq/user-contrib/basic/bar.v" {"coq/user-contrib/basic/bar.v"} "_build/install/default/lib/coq/user-contrib/basic/bar.vo" {"coq/user-contrib/basic/bar.vo"} + "_build/install/default/lib/coq/user-contrib/basic/foo.glob" {"coq/user-contrib/basic/foo.glob"} "_build/install/default/lib/coq/user-contrib/basic/foo.v" {"coq/user-contrib/basic/foo.v"} "_build/install/default/lib/coq/user-contrib/basic/foo.vo" {"coq/user-contrib/basic/foo.vo"} ] diff --git a/test/blackbox-tests/test-cases/coq/per_file_flags.t/run.t b/test/blackbox-tests/test-cases/coq/per_file_flags.t/run.t index 945f00fbe32..5f8bd5899b8 100644 --- a/test/blackbox-tests/test-cases/coq/per_file_flags.t/run.t +++ b/test/blackbox-tests/test-cases/coq/per_file_flags.t/run.t @@ -18,8 +18,10 @@ "_build/install/default/lib/coq/user-contrib/basic/.coq-native/Nbasic_bar.cmxs" {"coq/user-contrib/basic/.coq-native/Nbasic_bar.cmxs"} "_build/install/default/lib/coq/user-contrib/basic/.coq-native/Nbasic_foo.cmi" {"coq/user-contrib/basic/.coq-native/Nbasic_foo.cmi"} "_build/install/default/lib/coq/user-contrib/basic/.coq-native/Nbasic_foo.cmxs" {"coq/user-contrib/basic/.coq-native/Nbasic_foo.cmxs"} + "_build/install/default/lib/coq/user-contrib/basic/bar.glob" {"coq/user-contrib/basic/bar.glob"} "_build/install/default/lib/coq/user-contrib/basic/bar.v" {"coq/user-contrib/basic/bar.v"} "_build/install/default/lib/coq/user-contrib/basic/bar.vo" {"coq/user-contrib/basic/bar.vo"} + "_build/install/default/lib/coq/user-contrib/basic/foo.glob" {"coq/user-contrib/basic/foo.glob"} "_build/install/default/lib/coq/user-contrib/basic/foo.v" {"coq/user-contrib/basic/foo.v"} "_build/install/default/lib/coq/user-contrib/basic/foo.vo" {"coq/user-contrib/basic/foo.vo"} ] 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 4226112125f..234f62e4d40 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 @@ -9,9 +9,8 @@ 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/dune:2 - -> required by _build/default/public/.public.theory.d - -> required by _build/default/public/b.vo - -> required by _build/install/default/lib/coq/user-contrib/public/b.vo + -> required by _build/default/public/b.glob + -> required by _build/install/default/lib/coq/user-contrib/public/b.glob -> required by _build/default/public.install -> required by %{read:public.install} at dune:3 -> required by alias default in dune:1 diff --git a/test/blackbox-tests/test-cases/coq/rec-module.t/run.t b/test/blackbox-tests/test-cases/coq/rec-module.t/run.t index 0f6b6ec30bd..9f6ce5597a8 100644 --- a/test/blackbox-tests/test-cases/coq/rec-module.t/run.t +++ b/test/blackbox-tests/test-cases/coq/rec-module.t/run.t @@ -20,12 +20,16 @@ "_build/install/default/lib/rec/opam" ] lib_root: [ + "_build/install/default/lib/coq/user-contrib/rec_module/a/bar.glob" {"coq/user-contrib/rec_module/a/bar.glob"} "_build/install/default/lib/coq/user-contrib/rec_module/a/bar.v" {"coq/user-contrib/rec_module/a/bar.v"} "_build/install/default/lib/coq/user-contrib/rec_module/a/bar.vo" {"coq/user-contrib/rec_module/a/bar.vo"} + "_build/install/default/lib/coq/user-contrib/rec_module/b/foo.glob" {"coq/user-contrib/rec_module/b/foo.glob"} "_build/install/default/lib/coq/user-contrib/rec_module/b/foo.v" {"coq/user-contrib/rec_module/b/foo.v"} "_build/install/default/lib/coq/user-contrib/rec_module/b/foo.vo" {"coq/user-contrib/rec_module/b/foo.vo"} + "_build/install/default/lib/coq/user-contrib/rec_module/c/d/bar.glob" {"coq/user-contrib/rec_module/c/d/bar.glob"} "_build/install/default/lib/coq/user-contrib/rec_module/c/d/bar.v" {"coq/user-contrib/rec_module/c/d/bar.v"} "_build/install/default/lib/coq/user-contrib/rec_module/c/d/bar.vo" {"coq/user-contrib/rec_module/c/d/bar.vo"} + "_build/install/default/lib/coq/user-contrib/rec_module/c/ooo.glob" {"coq/user-contrib/rec_module/c/ooo.glob"} "_build/install/default/lib/coq/user-contrib/rec_module/c/ooo.v" {"coq/user-contrib/rec_module/c/ooo.v"} "_build/install/default/lib/coq/user-contrib/rec_module/c/ooo.vo" {"coq/user-contrib/rec_module/c/ooo.vo"} ] diff --git a/test/blackbox-tests/test-cases/coq/vos-build.t/run.t b/test/blackbox-tests/test-cases/coq/vos-build.t/run.t index 1b5e7031537..364af875235 100644 --- a/test/blackbox-tests/test-cases/coq/vos-build.t/run.t +++ b/test/blackbox-tests/test-cases/coq/vos-build.t/run.t @@ -44,8 +44,10 @@ Checking that we can go back to vo mode (without cleaning). "_build/install/default/lib/base/opam" ] lib_root: [ + "_build/install/default/lib/coq/user-contrib/basic/bar.glob" {"coq/user-contrib/basic/bar.glob"} "_build/install/default/lib/coq/user-contrib/basic/bar.v" {"coq/user-contrib/basic/bar.v"} "_build/install/default/lib/coq/user-contrib/basic/bar.vo" {"coq/user-contrib/basic/bar.vo"} + "_build/install/default/lib/coq/user-contrib/basic/foo.glob" {"coq/user-contrib/basic/foo.glob"} "_build/install/default/lib/coq/user-contrib/basic/foo.v" {"coq/user-contrib/basic/foo.v"} "_build/install/default/lib/coq/user-contrib/basic/foo.vo" {"coq/user-contrib/basic/foo.vo"} ]