Coq cannot find the cmxs file for transitive ocaml dependencies

[rlepigre]

When building Coq theories with plugins depending on OCaml libraries (everything being in a dune workspace) it seems like dune sometimes fails to place .cmxs files for transitive dependencies where Coq expects to find them. Since Coq relies on findlib, it seems like all the OCaml libraries depended on transitively by plugins should be made available in the _build/install directory (or at least a META file for them?).

Here is a tarball with a minimal example of workspace that exhibits the problem: dune_bug_plugin_deps.tar.gz. It contains the following files:

dune_bug_plugin_deps
├── coqlib
│   ├── coqlib.opam
│   ├── coqlib-plugin.opam
│   ├── dune-project
│   ├── plugin
│   │   ├── coqlib_plugin.mlpack
│   │   ├── dune
│   │   └── main.ml
│   └── theories
│       ├── dune
│       └── plugin.v
├── dune-workspace
└── somelib
    ├── dune-project
    ├── somelib.opam
    └── src
        ├── dune
        └── version.ml

To reproduce the problem, simply run:

$ cd dune_bug_plugin_deps
$ dune build coqlib/theories/plugin.vo
File "./coqlib/theories/plugin.v", line 1, characters 0-41:
Error:
Dynlink error: error loading shared library: Failure("[...]/dune_bug_plugin_deps/_build/install/default/lib/somelib/somelib.cmxs: cannot open shared object file: No such file or directory")

This was tested with Coq 8.19, and dune 3.16.0.

[rlepigre]

cc @ejgallego @Alizter

[rlepigre]

Note also that the example provides a workaround in file dune_bug_plugin_deps/coqlib/theories/dune:

(coq.theory
 (name coqlib)
 (package coqlib)
 (plugins coqlib-plugin.plugin))

;(rule
; (targets dummy.v)
; (deps (package coqlib-plugin))
; (action (with-stdout-to %{targets} (echo "(* dummy file *)"))))

Removing the comments on the rule will fix the issue by forcing a dependency over the coqlib-plugin package (which is the reason to have a separate package for the plugin in the example, I think the problem is the same if it is in the same package as the theory).

[ejgallego]

Indeed, thanks for the report, I am hoping to look into this (finally) next week.

Seems like a case of missing transitive deps, the implementation of Coq plugin building didn't take into account this possibility due to technical reasons that no longer hold. But I need to look into this more carefully.

So indeed, let's try to fix this case soon; I think that for now a workaround that could work is to list all the libs.

[rlepigre]

@ejgallego is there anything I can help with here? I'm lacking context to look into this myself, but I could try if you provided some guidance for example.

[ejgallego]

Hi @rlepigre , I hope I can allocate time to work on this soon, got hit by some unexpected stuff I had to take care of urgently :/ :/

If I am correct, the problem here is due to a missing dep for the installed .cmxs file, right?

In this case, the fix should be easy (and it shouldn't have a perf impact as we already depend on the direct .cmxs).

Actually we have code for both:

• grabbing the transitive deps of ML libraries
• depending on a "public" installed .cmxs

So I think we need to make the two parts cooperate in order to fix this issue.

Code here:

• dune/src/dune_rules/coq/coq_rules.ml

  Line 418 in f7af2d0

  let+ findlib_libs = Lib.closure ~linking:false (List.map ~f:snd libs) in

• dune/src/dune_rules/coq/coq_rules.ml

  Line 449 in f7af2d0

  let findlib_plugin_flags = Util.include_flags all_libs in

• https://github.com/ocaml/dune/blob/main/src/dune_rules/coq/coq_rules.ml#L32

So indeed, before we used to depend on all libraries but in their build dir, for example this typically was -I _build/default/lib-foo/.library.objs/ and a dep on -I _build/default/lib-foo/.library.objs/foo.cmxs

But indeed, coq_rules:Util.include_paths seems not useful anymore, we don't need to pass any -I anymore to coqdep.

On the other hand, the bug comes because we rely on coqdep outputting the .cmxs deps. However coqdep doesn't output the transitive cmxs deps.

So I'm unsure what is the best rule approximation... We have two choices:

• detect when coqdep adds a .cmxs dep, and then complete with the transitive closure
• require the transitive closure of a theory OCaml deps to be build before the theory, however this will block building of files in that theory that don't depend on the plugin, and bloat the dep graph non trivially.

I suggest we continue discussion on Zulip or in a visio.

[rlepigre]

I suggest we continue discussion on Zulip or in a visio.

OK thanks, sounds good.