I am currently porting some Coq code and OCaml plugins to
coq.8.16.0, and it seems that
dune.3.4.1 is not happy about this. As I understand it, plugins are now loaded using findlib names, but even after doing that dune complains about not being able to find some
META.something file. Is that expected? Do I need to us (unreleased)
I'll try the development version of
dune to check, but in the meantime I though it might be useful to get an answer here because I might have missed something.
Turns out the development version does not help. I might have a bug on my hand, I'll investigate.
Yup that's known
@Ali Caglayan had a PR documenting this, but it got stuck
Oh OK, thanks for the info. Do you have a link to the PR?
Coq's manual documents this, the short story is
Declare ML Module "foo_plugin:pkg.foo.plugin".
Dune 3.5.0 will have the needed fix there
however coqdep seems quite buggy
so Coq needs to be fixed too
but using the legacy methods works fine for now
the coqdep bug is
(one of them)
OK I see, thanks!
quickest way to see how things should be is Dune test suite hehe
Yeah, I had a quick look to the test suite actually, but I obviously missed something. :smile:
Only thing you lose by the legacy syntax is dep loading, so not a big deal
Yeah it seems everyone is confused about this
@Rodolphe Lepigre do you need a backport of the coqdep patch?
I can do it very quickly
if you haven't got to it yet
I made my own quickly, I'll check if it works.
Do you want me to push that somewhere so that you can use it for 8.16.1?
Yes please do a draft pull request targetting the 8.16 branch, thanks!
I'm assumming @Pierre-Marie Pédrot will be OK with that PR to be backported
However we didn't run the CI on it yet, but a failure would be surprising
Last updated: Feb 04 2023 at 01:03 UTC