Rodolphe Lepigre (Oct 06 2022 at 07:16): Rodolphe Lepigre (Oct 06 2022 at 07:16):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) dune.3.5.0 for coq.8.16.0?
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.
Rodolphe Lepigre (Oct 06 2022 at 07:26):Turns out the development version does not help. I might have a bug on my hand, I'll investigate.
Emilio Jesús Gallego Arias (Oct 06 2022 at 07:35):Yup that's known
Emilio Jesús Gallego Arias (Oct 06 2022 at 07:35):@Ali Caglayan had a PR documenting this, but it got stuck
Rodolphe Lepigre (Oct 06 2022 at 07:36):Oh OK, thanks for the info. Do you have a link to the PR?
Emilio Jesús Gallego Arias (Oct 06 2022 at 07:36):Coq's manual documents this, the short story is
use
Declare ML Module "foo_plugin:pkg.foo.plugin".
Emilio Jesús Gallego Arias (Oct 06 2022 at 07:37):https://github.com/ocaml/dune/pull/5778
Emilio Jesús Gallego Arias (Oct 06 2022 at 07:37):Dune 3.5.0 will have the needed fix there
Emilio Jesús Gallego Arias (Oct 06 2022 at 07:37):however coqdep seems quite buggy
Emilio Jesús Gallego Arias (Oct 06 2022 at 07:37):so Coq needs to be fixed too
Emilio Jesús Gallego Arias (Oct 06 2022 at 07:37):but using the legacy methods works fine for now
Emilio Jesús Gallego Arias (Oct 06 2022 at 07:37):the coqdep bug is
Emilio Jesús Gallego Arias (Oct 06 2022 at 07:37):(one of them)
Rodolphe Lepigre (Oct 06 2022 at 07:38):OK I see, thanks!
Emilio Jesús Gallego Arias (Oct 06 2022 at 07:38):https://github.com/coq/coq/issues/16571
Emilio Jesús Gallego Arias (Oct 06 2022 at 07:38):quickest way to see how things should be is Dune test suite hehe
Rodolphe Lepigre (Oct 06 2022 at 07:39):Yeah, I had a quick look to the test suite actually, but I obviously missed something. :smile:
Emilio Jesús Gallego Arias (Oct 06 2022 at 07:39):Only thing you lose by the legacy syntax is dep loading, so not a big deal
Emilio Jesús Gallego Arias (Oct 06 2022 at 07:39):Yeah it seems everyone is confused about this
Emilio Jesús Gallego Arias (Oct 14 2022 at 11:06):@Rodolphe Lepigre do you need a backport of the coqdep patch?
Emilio Jesús Gallego Arias (Oct 14 2022 at 11:06):I can do it very quickly
Emilio Jesús Gallego Arias (Oct 14 2022 at 11:07):if you haven't got to it yet
Rodolphe Lepigre (Oct 14 2022 at 11:07):I made my own quickly, I'll check if it works.
Emilio Jesús Gallego Arias (Oct 14 2022 at 11:09):Ok great
Rodolphe Lepigre (Oct 14 2022 at 11:11):Do you want me to push that somewhere so that you can use it for 8.16.1?
Emilio Jesús Gallego Arias (Oct 14 2022 at 11:14):Yes please do a draft pull request targetting the 8.16 branch, thanks!
Emilio Jesús Gallego Arias (Oct 14 2022 at 11:14):I'm assumming @Pierre-Marie Pédrot will be OK with that PR to be backported
Emilio Jesús Gallego Arias (Oct 14 2022 at 11:15):However we didn't run the CI on it yet, but a failure would be surprising
Rodolphe Lepigre (Oct 14 2022 at 11:27):See https://github.com/coq/coq/pull/16664.
Last updated: Apr 19 2024 at 02:02 UTC