[3.8] backport ocaml#7790 and ocaml#7862 (ocaml#7889)

* 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 <alizter@gmail.com>
Signed-off-by: Etienne Millon <me@emillon.org>

* fix(coq): first theory in COQPATH takes precedence always

Signed-off-by: Ali Caglayan <alizter@gmail.com>
Signed-off-by: Etienne Millon <me@emillon.org>

* coq: add missing changelog entry

Signed-off-by: Ali Caglayan <alizter@gmail.com>
Signed-off-by: Etienne Millon <me@emillon.org>

---------

Signed-off-by: Ali Caglayan <alizter@gmail.com>
Signed-off-by: Etienne Millon <me@emillon.org>
Co-authored-by: Ali Caglayan <alizter@gmail.com>

CHANGES.md

@@ -5,6 +5,11 @@
   config variable being missing. We now explicitly default to `(mode vo)` for
   these older versions of Coq. (#7847, fixes #7846, @Alizter)
 
+- Duplicate installed Coq theories are now allowed with the first appearing in
+  COQPATH being preferred. This is inline with Coq's loadpath semantics. This
+  fixes an issue with install layouts based on COQPATH such as those found in
+  nixpkgs. (#7790, @Alizter)
+
 3.8.0 (2023-05-23)
 ------------------
 

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]