From 398a7c1f589c514c7f6ce3a86a3e0043528f9d0c Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Tue, 23 May 2023 17:21:03 +0200 Subject: [PATCH 1/2] test(coq): duplicate theory prefix in COQPATH bug This bug happens when using COQPATH so it won't affect most users. When having two theories A.B and A.C installed, dune will erroneously fail saying that the theory A has been defined twice. Signed-off-by: Ali Caglayan --- .../coq/compose-installed-prefix-dupe.t/B/a.v | 0 .../compose-installed-prefix-dupe.t/B/dune | 3 ++ .../B/dune-project | 3 ++ .../coq/compose-installed-prefix-dupe.t/C/a.v | 0 .../compose-installed-prefix-dupe.t/C/dune | 3 ++ .../C/dune-project | 3 ++ .../coq/compose-installed-prefix-dupe.t/run.t | 41 +++++++++++++++++++ .../coq/compose-installed-sub.t/run.t | 9 +--- .../test-cases/coq/compose-installed.t/run.t | 9 +--- 9 files changed, 57 insertions(+), 14 deletions(-) create mode 100644 test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/B/a.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/B/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/B/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/C/a.v create mode 100644 test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/C/dune create mode 100644 test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/C/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/run.t diff --git a/test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/B/a.v b/test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/B/a.v new file mode 100644 index 00000000000..e69de29bb2d diff --git a/test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/B/dune b/test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/B/dune new file mode 100644 index 00000000000..96d24775589 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/B/dune @@ -0,0 +1,3 @@ +(coq.theory + (name A.B) + (package Theory1)) diff --git a/test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/B/dune-project b/test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/B/dune-project new file mode 100644 index 00000000000..0b60c2ca75e --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/B/dune-project @@ -0,0 +1,3 @@ +(lang dune 3.8) +(using coq 0.8) +(package (name Theory1)) diff --git a/test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/C/a.v b/test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/C/a.v new file mode 100644 index 00000000000..e69de29bb2d diff --git a/test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/C/dune b/test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/C/dune new file mode 100644 index 00000000000..e6f4949e56f --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/C/dune @@ -0,0 +1,3 @@ +(coq.theory + (name A.C) + (package Theory2)) diff --git a/test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/C/dune-project b/test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/C/dune-project new file mode 100644 index 00000000000..d13619154a3 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/C/dune-project @@ -0,0 +1,3 @@ +(lang dune 3.8) +(using coq 0.8) +(package (name Theory2)) diff --git a/test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/run.t b/test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/run.t new file mode 100644 index 00000000000..be1cb93318a --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/run.t @@ -0,0 +1,41 @@ +If we have installed theories A.B and A.C then Dune should not complain that A +is a duplicate theory. + +First we install our two theories with the conflicting name prefix. + + $ (cd B && dune build @install && dune install --prefix .) + $ (cd C && dune build @install && dune install --prefix .) + +We add these to COQPATH + + $ export COQPATH=../B/lib/coq/user-contrib:../C/lib/coq/user-contrib:$COQPATH + +Now we create a theory that depends on both + + $ mkdir mytheory && cd mytheory + + $ cat > dune-project << EOF + > (lang dune 3.8) + > (using coq 0.8) + > EOF + + $ cat > dune << EOF + > (coq.theory + > (name mytheory) + > (theories A.B A.C)) + > EOF + + $ cat > a.v << EOF + > From A.B Require a. + > From A.C Require a. + > EOF + + + $ dune build a.vo --display short + Error: Coq theory A is defined twice: + - theory A in + $TESTCASE_ROOT/mytheory/../B/lib/coq/user-contrib/A + - theory A in + $TESTCASE_ROOT/mytheory/../C/lib/coq/user-contrib/A + [1] + 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 7416b29cc06..6f5ec1ae38c 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 @@ -187,7 +187,8 @@ We test updating the dune file for user to use the super-theory works: Leaving directory 'user' We test whether installing `global` again in user-contrib will cause Dune to reject the -build. +build. Currently this is not the case and the first theory is preferred inline +with the loadpath semantics of Coq. $ dune install --root global --prefix=$PWD --display=short Installing $TESTCASE_ROOT/lib/global/META @@ -203,10 +204,4 @@ build. $ dune build --root user Entering directory 'user' - Error: Coq theory global is defined twice: - - theory global in - $TESTCASE_ROOT/another-place/lib/coq/user-contrib/global - - theory global in - $TESTCASE_ROOT/lib/coq/user-contrib/global Leaving directory 'user' - [1] 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 3a083498571..af02c8cc5d4 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 @@ -103,7 +103,8 @@ any problems. It shouldn't do, as the workspace should take precedence. I : hello | am : hello | an : hello | install : hello | loc : hello. We test whether installing B again in user-contrib will cause Dune to reject the -build. +build. Currently this is not the case and the first theory is preferred inline +with the loadpath semantics of Coq. $ dune install --root B --prefix=$PWD --display=short Installing $TESTCASE_ROOT/lib/B/META @@ -115,10 +116,4 @@ build. $ dune build --root A Entering directory 'A' - Error: Coq theory B is defined twice: - - theory B in - $TESTCASE_ROOT/another-place/lib/coq/user-contrib/B - - theory B in - $TESTCASE_ROOT/lib/coq/user-contrib/B Leaving directory 'A' - [1] From 7cc014a5055e402d4ad713d1c83b156af47d2fb8 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Wed, 31 May 2023 22:50:37 +0200 Subject: [PATCH 2/2] fix(coq): first theory in COQPATH takes precedence always Signed-off-by: Ali Caglayan --- src/dune_rules/coq/coq_lib.ml | 12 ++++-------- .../coq/compose-installed-prefix-dupe.t/B/a.v | 1 + .../coq/compose-installed-prefix-dupe.t/C/a.v | 1 + .../coq/compose-installed-prefix-dupe.t/run.t | 15 +++++---------- 4 files changed, 11 insertions(+), 18 deletions(-) diff --git a/src/dune_rules/coq/coq_lib.ml b/src/dune_rules/coq/coq_lib.ml index d0a9d5c8f3e..25e29365625 100644 --- a/src/dune_rules/coq/coq_lib.ml +++ b/src/dune_rules/coq/coq_lib.ml @@ -647,14 +647,10 @@ module DB = struct (* Map is eager, this may not be very convenient in large trees, but should be fine for now *) let map = - match - Coq_lib_name.Map.of_list_map cps ~f:(fun cp -> (Coq_path.name cp, cp)) - with - | Ok m -> m - | Error (name, cp1, cp2) -> - let id1 = Id.create ~path:(Coq_path.path cp1) ~name:(Loc.none, name) in - let id2 = Id.create ~path:(Coq_path.path cp2) ~name:(Loc.none, name) in - Error.duplicate_theory_name id1 id2 + List.rev_map cps ~f:(fun cp -> (Coq_path.name cp, cp)) + (* Since we reversed the order, the second coqpath should take + precedence. This is in line with Coq semantics. *) + |> Coq_lib_name.Map.of_list_reducei ~f:(fun _name _cp1 cp2 -> cp2) in let resolve name : t Resolve_result.t = match Coq_lib_name.Map.find map name with diff --git a/test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/B/a.v b/test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/B/a.v index e69de29bb2d..07bf8ad935c 100644 --- a/test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/B/a.v +++ b/test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/B/a.v @@ -0,0 +1 @@ +Inductive b := . \ No newline at end of file diff --git a/test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/C/a.v b/test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/C/a.v index e69de29bb2d..761e6637d52 100644 --- a/test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/C/a.v +++ b/test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/C/a.v @@ -0,0 +1 @@ +Inductive c := . \ No newline at end of file diff --git a/test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/run.t b/test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/run.t index be1cb93318a..edeedb6fe25 100644 --- a/test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/run.t +++ b/test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/run.t @@ -26,16 +26,11 @@ Now we create a theory that depends on both > EOF $ cat > a.v << EOF - > From A.B Require a. - > From A.C Require a. + > From A.B Require Import a. + > From A.C Require Import a. + > Print b. > EOF - - $ dune build a.vo --display short - Error: Coq theory A is defined twice: - - theory A in - $TESTCASE_ROOT/mytheory/../B/lib/coq/user-contrib/A - - theory A in - $TESTCASE_ROOT/mytheory/../C/lib/coq/user-contrib/A - [1] + $ dune build a.vo + Inductive b : Prop := .