Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Coq cannot find the cmxs file for transitive ocaml dependencies #11012

Open
rlepigre opened this issue Oct 15, 2024 · 4 comments
Open

Coq cannot find the cmxs file for transitive ocaml dependencies #11012

rlepigre opened this issue Oct 15, 2024 · 4 comments
Labels
coq

Comments

@rlepigre
Copy link
Contributor

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
Copy link
Contributor Author

cc @ejgallego @Alizter

@rlepigre
Copy link
Contributor Author

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

@maiste maiste added the coq label Oct 15, 2024
@ejgallego
Copy link
Collaborator

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 rlepigre mentioned this issue Nov 4, 2024
Open
@rlepigre
Copy link
Contributor Author

rlepigre commented Nov 4, 2024

@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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
coq
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@rlepigre @ejgallego @maiste