Stream: Coq devs & plugin devs

Topic: Plugins and theories in same package?


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

Do we want plugins and theories in the same package? I am updating some documentation in dune, and I think it would be good to be clear about this point.

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

Now that a plugin requires a META.plug_file for findlib to work, does it really make sense to have .v files be built as part of that package?

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

Before the findlib patch, I see a lot of writing about mixing ml files and v files when writing plugins. I think this is a completely bonkers workflow today, but I am open to be convinced otherwise.

view this post on Zulip Li-yao (May 23 2022 at 16:05):

Having dune take care of the Declare ML Module boilerplate sounds like a good idea to me.

view this post on Zulip Karl Palmskog (May 23 2022 at 16:06):

I agree it would be nice to have Dune do Declare ML Module by default, but I don't think it should be impossible to override (i.e., allow people opt in or out)

view this post on Zulip Pierre-Marie Pédrot (May 23 2022 at 16:06):

Declare ML as a vernac command is pretty much unrelated to the build system though.

view this post on Zulip Ali Caglayan (May 23 2022 at 16:07):

coqdep still reads it and talks to dune

view this post on Zulip Ali Caglayan (May 23 2022 at 16:08):

The issue is that coqdep reads Declare ML Module "public_name" and then adds a dependency on META.public_name.

view this post on Zulip Ali Caglayan (May 23 2022 at 16:08):

Dune will not build the META file until everything in the package has been built (which apparently sometimes included .v files)

view this post on Zulip Karl Palmskog (May 23 2022 at 16:08):

if we can somehow make Declare ML be unrelated to the build system, that'd be great...

view this post on Zulip Karl Palmskog (May 23 2022 at 16:09):

but there have been 10+ instances where Declare ML and build systems were a headache for me, just in the last six months

view this post on Zulip Ali Caglayan (May 23 2022 at 16:09):

The only reason coq_makefile works is because it makes up a META file and inserts it.

view this post on Zulip Ali Caglayan (May 23 2022 at 16:12):

This also means that complicated META files have to be preprepared for coq_makefile

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

I don't see a problem with plugin and theories in the same package. Regarding dune support for newer Coq versions, we need some changes in Coq as the compatiblity layer is broken, and there is a large discrepancy of the meaning of -I for coqdep and coqc in master.

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

I think for now the easiest is to fix the compat layer which I figured out in https://github.com/coq/coq/pull/15991 , just needs a bit more testing.

The basic problem is that we were not storing if legacy mode was used in the .vo file, but that's needed in order to have a robust setup, there are many other subtle bugs in current code due to non-determinism and the aforementioned discrepancies.

view this post on Zulip Ali Caglayan (May 23 2022 at 16:34):

Writing a plugin today is difficult.

view this post on Zulip Ali Caglayan (May 23 2022 at 16:34):

Half the time the example plugins I write don't even work.

view this post on Zulip Ali Caglayan (May 23 2022 at 16:35):

At the moment, we are not making the plugin authors life easy.

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

Dune was making the life very easy before the META PR tho

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

Using dune I could create overlays over all the plugins simultaneously

view this post on Zulip Ali Caglayan (May 23 2022 at 16:36):

Right, but today dune is not making life easy, it is making it harder.

view this post on Zulip Ali Caglayan (May 23 2022 at 16:37):

So we need to change something in Coq to make this easier.

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

how is dune making life harder?

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

it is the Coq implementation that is broken

view this post on Zulip Ali Caglayan (May 23 2022 at 16:37):

Not intentionally.

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

just we didn't test enough

view this post on Zulip Ali Caglayan (May 23 2022 at 16:37):

Right, but we are about to do another release and writing a plugin has never been so finicky with dune.

view this post on Zulip Ali Caglayan (May 23 2022 at 16:38):

coq_makefile works today, only because it is using a hack

view this post on Zulip Ali Caglayan (May 23 2022 at 16:38):

at the moment, the state of affairs is completely broken

view this post on Zulip Ali Caglayan (May 23 2022 at 16:39):

What is it that we need to change in Coq to fix this?

view this post on Zulip Ali Caglayan (May 23 2022 at 16:42):

POV of the plugin authors:

  1. Use coq_makefile plugin works
  2. Switch to dune before 8.15 plugin works
  3. 8.15 and so on starts complaining about META files
  4. switch back to coq_makefile everything is fine

view this post on Zulip Ali Caglayan (May 23 2022 at 16:42):

I am not saying it is dune's fault. I agree with you that dune is doing the right thing.

view this post on Zulip Ali Caglayan (May 23 2022 at 16:43):

But Coq is not doing the right thing and it is annoying plugin authors.

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

Yes, we need to finish https://github.com/coq/coq/pull/15991 which only needs to restore the old -I setup for the compat setting

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

And additionally cleanup the code as we discussed the other day in the zoom call, in particular remove the non deterministic behavior

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

also we need to make coqdep and coqc agree on what -I means

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

which now they don't

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

IIUC

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

For https://github.com/coq/coq/pull/15991 , I have a lot of local changes that makes things almost work

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

and remove all these hacks

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

I don't know tho when I'll get cycles for that

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

Emilio Jesús Gallego Arias said:

I don't know tho when I'll get cycles for that

But the fix is pretty easy conceptually: store in the .vo what loading method was used (legacy or META) and add the -I legacy paths

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

So that is to say, when in legacy mode, do what was done in legacy mode!


Last updated: Feb 05 2023 at 20:03 UTC