Expected Behavior

When I create a dune-project and dune file for a Coq project with Dune 3.8 and depend on a Coq plugin installed via coq_makefile like Equations, it should suffice to add (theories Equations) into (coq.theory ...) to enable compilation of the project.

Actual Behavior

When I run dune build, I get the following error:

Error: Can't find file equations_plugin.cmxs on loadpath.

Reproduction

1. Create a dune-project file like the following:

(lang dune 3.8)
(using coq 0.8)
(name TestEquations)

2. Create a dune file like the following:

(coq.theory
 (name TestEquations)
 (synopsis "Test Equations")
 (theories Equations)
 ;(plugins coq-equations)
)

3. Create Eqn.v or other .v file like the following:

From Equations Require Import Equations.

4. Run dune build, get the following error:

File "./Eqn.v", line 1, characters 0-40:
Error: Can't find file equations_plugin.cmxs on loadpath.

Note that the error disappears if ;(plugins coq-equations) in dune is uncommented.

Specifications

• Version of dune (output of dune --version): 3.8.0
• Version of ocaml (output of ocamlc --version): 4.14.1
• Operating system (distribution and version): Ubuntu LTS 22.04

Additional information

This bug report was submitted at the suggestion of @ejgallego.

• Coq version: 8.16.0
• Equations version: 1.3+8.16