Stream: Dune devs & users

Topic: Dune problems for newer Coq versions?


view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 15:12):

@Ali Caglayan points out that there are some problems when using Coq and Dune in newer Coq versions. I didn't check for 8.16, but for 8.15, the Dune Coq language test suite runs well, so I can't detect any problem. Can you provide a reproduction case here?

view this post on Zulip Ali Caglayan (May 25 2022 at 15:18):

Plugin.tar.gz

dune build will work.

Do a dune clean.

dune build --cache=disabled theories/UsingMyPlugin.vo and it doesn't.

view this post on Zulip Ali Caglayan (May 25 2022 at 15:22):

Plugin2.tar.gz

Same with this.

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 15:23):

Which Coq version?

view this post on Zulip Ali Caglayan (May 25 2022 at 15:23):

8.16

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 15:23):

ok let me see

view this post on Zulip Ali Caglayan (May 25 2022 at 15:25):

In 8.15, once you modify to the legacy names they work

view this post on Zulip Ali Caglayan (May 25 2022 at 15:26):

I believe the crux of the problem is that the dune rules don't rely on the META file.

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 15:34):

Oh, the problem is that Dune doesn't support that method

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 15:34):

at all indeed

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 15:35):

you need to use

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 15:35):

Declare ML Module "MyPlugin".

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 15:37):

It should be like this Declare ML Module "my_plugin:my-coq-plugin.plugin".

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 15:38):

The new form is just not supported, the one I propose likely has a bug

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 15:38):

So indeed we need to document that.

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 15:47):

Yes master works fine for me

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 15:47):

great job by Enrico keeping the compat

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 15:47):

Actually my PR makes it fail, but the fix is easy

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 15:52):

Dune's test-suite works fine in master !

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 15:52):

Provided we adapt the test cases to the new declare ML syntax

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 15:55):

So @Ali Caglayan , does that solve your problem?

view this post on Zulip Ali Caglayan (May 25 2022 at 16:00):

@Emilio Jesús Gallego Arias Are you running the tests correctly? dune build @test/blackbox-tests/test-cases/coq/runtest?

view this post on Zulip Ali Caglayan (May 25 2022 at 16:01):

Also make sure you have a more recent version of dune or else dune skips the coq tests when coq is not present

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 16:04):

I think I'm running the tests correctly

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 16:05):

I'm using Dune master plus Coq master

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 16:05):

and this PR

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 16:05):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 16:11):

So actually things work fine with my PR, @Ali Caglayan you have another bug in your code

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 16:12):

the mlg should have DECLARE PLUGIN "my-coq-plugin.plugin"

view this post on Zulip Ali Caglayan (May 25 2022 at 16:18):

Why does it work the other way?

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 16:19):

What do you mean @Ali Caglayan ?

view this post on Zulip Ali Caglayan (May 25 2022 at 16:19):

Emilio Jesús Gallego Arias said:

the mlg should have DECLARE PLUGIN "my-coq-plugin.plugin"

Why?

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 16:19):

Oh because the table that checks required plugins is using the new plugin name as index

view this post on Zulip Ali Caglayan (May 25 2022 at 16:19):

It also worked when it was wrong so I am confused about the point of this.

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 16:19):

not after my PR, that was a bug in old code

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 16:20):

it was too loose

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 16:20):

and registered the wrong name

view this post on Zulip Ali Caglayan (May 25 2022 at 16:20):

Does it still work when you target a vo from a clean build?

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 16:20):

then it needed the hack, now we use the findlib name all the time

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 16:21):

yes it works for me, please test!

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 16:22):

So migration is basically to replace the old names

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 16:22):

and in dune we need to use the foo:pkg.foo syntax

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 16:22):

for now

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 16:48):

Does it work for you ?

view this post on Zulip Ali Caglayan (May 25 2022 at 17:04):

Looks like it

view this post on Zulip Ali Caglayan (May 25 2022 at 17:04):

Thanks for documenting it in the mltop PR

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 17:06):

I just learned how it works lol

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 17:06):

I mean a couple of days ago

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 17:06):

but it looks good to me

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 17:06):

now we need to fix (coq.theory ...)

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 17:07):

that'll be easy, I think we have been making things more complex than they are

view this post on Zulip Emilio Jesús Gallego Arias (May 25 2022 at 17:12):

but build stuff is tricky one needs a lot of discipline, specially with a system like dune which is so precise


Last updated: Jan 30 2023 at 18:04 UTC