coq: test and fix duplicate theory prefix in COQPATH bug

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

test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/B/a.v

@@ -0,0 +1 @@
+Inductive 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))

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))

test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/C/a.v

@@ -0,0 +1 @@
+Inductive c := .

test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/C/dune

@@ -0,0 +1,3 @@
+(coq.theory
+ (name A.C)
+ (package Theory2))

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))

test/blackbox-tests/test-cases/coq/compose-installed-prefix-dupe.t/run.t

@@ -0,0 +1,36 @@
+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 Import a.
+  > From A.C Require Import a.
+  > Print b.
+  > EOF
+
+  $ dune build a.vo
+  Inductive b : Prop :=  .
+

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]

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]