Stream: Dune devs & users

Topic: Plugins with Coq 8.16


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 07:35):

Yup that's known

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 07:35):

@Ali Caglayan had a PR documenting this, but it got stuck

view this post on Zulip Rodolphe Lepigre (Oct 06 2022 at 07:36):

Oh OK, thanks for the info. Do you have a link to the PR?

view this post on Zulip 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".

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 07:37):

https://github.com/ocaml/dune/pull/5778

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 07:37):

Dune 3.5.0 will have the needed fix there

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 07:37):

however coqdep seems quite buggy

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 07:37):

so Coq needs to be fixed too

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 07:37):

but using the legacy methods works fine for now

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 07:37):

the coqdep bug is

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 07:37):

(one of them)

view this post on Zulip Rodolphe Lepigre (Oct 06 2022 at 07:38):

OK I see, thanks!

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 07:38):

https://github.com/coq/coq/issues/16571

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 07:38):

quickest way to see how things should be is Dune test suite hehe

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2022 at 07:39):

Yeah it seems everyone is confused about this

view this post on Zulip Emilio Jesús Gallego Arias (Oct 14 2022 at 11:06):

@Rodolphe Lepigre do you need a backport of the coqdep patch?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 14 2022 at 11:06):

I can do it very quickly

view this post on Zulip Emilio Jesús Gallego Arias (Oct 14 2022 at 11:07):

if you haven't got to it yet

view this post on Zulip Rodolphe Lepigre (Oct 14 2022 at 11:07):

I made my own quickly, I'll check if it works.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 14 2022 at 11:09):

Ok great

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 14 2022 at 11:14):

Yes please do a draft pull request targetting the 8.16 branch, thanks!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Rodolphe Lepigre (Oct 14 2022 at 11:27):

See https://github.com/coq/coq/pull/16664.


Last updated: Feb 04 2023 at 01:03 UTC