Plugins and theories in same package? · Coq devs & plugin devs

Stream: Coq devs & plugin devs

Topic: Plugins and theories in same package?

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.

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?

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.

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.

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)

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.

Ali Caglayan (May 23 2022 at 16:07):

coqdep still reads it and talks to dune

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.

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)

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...

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

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.

Ali Caglayan (May 23 2022 at 16:12):

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

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.

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.