Rodolphe Lepigre

> What is your `Declare ML Module` ? I have several plugins, and hence several `Declare ML Module`. They are all placed in the same opam package. So for each...

Yes, on Coq 8.16.0. I'm not sure what the name of the generated `META` file is. How do I figure that out? I expected I could just look in the...

Oh sorry. The error I get is something like: ``` Error: File unavailable: /absolute/path/to/_build/install/default/lib/my_plugins/META ``` I'll try out the MR later and let you know. Thanks!

@ejgallego I confirmed that your patch to Coq (or rather, my back-ported version of it) fixes my problem. Thanks! For reference, see https://github.com/coq/coq/pull/16664.

@rgrinberg any idea what would be needed to fix this? I'd be happy to give it a shot, but some hints on what might be happening and on how to...

OK, thanks. However, I must be missing something: it seemed to me that the failing example I gave in https://github.com/ocaml/dune/pull/6233 shows that there is a dune bug, but you seem...

Actually, I'm wondering: doesn't the fix completely break dune's compositionality? Isn't it often the case that the dune workspace is not the same as the root of a dune project?...

@ppedrot is this blocked on anything? This would still be amazing to have!

Thanks for the MR @gares! Sorry it took so long to get back to you. The change indeed seems to fix the problem on the minimized example, but the issue...

> [...] but the issue actually still remains with our actual (more complicated) example. Actually, the issue seems to have been fixed, as we do not rely on `#[arguments(raw)]` at...