Stream: Dune devs & users

Topic: Dune 3.8 theories declarations

Karl Palmskog (Jun 05 2023 at 13:47):

So, I'm trying to do experimental ports to Dune 3.8 and (using coq 0.8) for some projects. However, it's not all that easy to figure out what to write in (theories ...). For example, I have a project where I need to add (theories Equations ...), and then I get this error during compilation:

Error: Can't find file equations_plugin.cmxs on loadpath.

Is there some special declaration needed for depending on coq_makefile-installed plugins?

Rodolphe Lepigre (Jun 05 2023 at 14:19):

You're gonna need to add something like (plugins coq-equations) as well, probably (or something similar).

Karl Palmskog (Jun 05 2023 at 14:43):

ah, declaring both based on package name and on the path prefix is going to be a major problem for most users.

Karl Palmskog (Jun 05 2023 at 14:44):

could one write some hack that uses a project's opam file and then generates the (theories ...) and (plugins ...) declarations?

Ali Caglayan (Jun 05 2023 at 14:47):

That would work for a single theory single package project, but more complicated projects with two or more theories would make this mapping a bit useless.

Ali Caglayan (Jun 05 2023 at 14:48):

There is unfortunately no way for us to scan an installed coq theory and work out if it is a plugin.

Ali Caglayan (Jun 05 2023 at 14:48):

In the future, we may design a new install layout where a package explicitly declares what it exports (like OCaml does today). That way we could understand if a theory needs a plugin or not.

Ali Caglayan (Jun 05 2023 at 14:49):

The best we can do today is document the Coq error and point people to the (plugins ) field unfrotunately.

Gaëtan Gilbert (Jun 05 2023 at 14:51):

shouldn't plugin dependencies be transitive? ie equations theory depends on equations plugin, so anything depending on equations theory also depends on equations plugin

Rodolphe Lepigre (Jun 05 2023 at 14:51):

Could we not provide a (libraries ...) field in theories that, in the case of a dune-generated package at least, would do things correctly (i.e., add the relevant theories and plugins)? I fear that for transitive deps the current approach will be a problem.

Ali Caglayan (Jun 05 2023 at 14:54):

The issue is that there are theories which use plugins but shouldn't reexport the plugins. For example the stdlib. There are multiple plugins that are not loaded for others by default unless you explicitly require a certain .v file.

Gaëtan Gilbert (Jun 05 2023 at 14:55):

true

Ali Caglayan (Jun 05 2023 at 14:56):

In the future, we could come up with a fine-grained plugin dependency at the level of coq modules. I worked on something like this before but it was tricky to get working and didn't seem worth it in the end.

Ali Caglayan (Jun 05 2023 at 14:57):

The idea would be that Dune would remember which plugins a .v file needs so if you declare a dependency on that then the new .v file would inherit those plugins etc.

Ali Caglayan (Jun 05 2023 at 14:58):

But there are some issues with library resoltuion and memory usage with this approach.

Ali Caglayan (Jun 05 2023 at 14:59):

I don't think it is a big ask for a user to declare exactly which plugins they wish to use. The same is true for OCaml libraries today anyway.

Rodolphe Lepigre (Jun 05 2023 at 14:59):

Could we not just make plugins private libraries? That is, they would only be directly usable in the library the defines them, and otherwise only be exposed via a .v file.

Karl Palmskog (Jun 05 2023 at 14:59):

asking regular users to find out (1) the exactly right path prefixes and (2) which of their deps are plugins, will unfortunately exclude most regular users from Dune at this point. I'd honestly advise most people to use coq_makefile until this is figured out (how to not have to know these things, like in coq_makefile)

Rodolphe Lepigre (Jun 05 2023 at 14:59):

For OCaml libraries, you don't need to ask for transitive dependencies that you do not directly depend on.

Gaëtan Gilbert (Jun 05 2023 at 15:00):

Ali Caglayan said:

I don't think it is a big ask for a user to declare exactly which plugins they wish to use. The same is true for OCaml libraries today anyway.

not when it's a transitive dep
indeed IMO users shouldn't have to care if a library is using a plugin, but this forces them to care

Karl Palmskog (Jun 05 2023 at 15:00):

with that said, since we have knowledgeable people around, we can still use Dune-Coq 0.8 widely in Coq-community and similar.

Ali Caglayan (Jun 05 2023 at 15:02):

Rodolphe Lepigre said:

Could we not just make plugins private libraries? That is, they would only be directly usable in the library the defines them, and otherwise only be exposed via a .v file.

So this seems sensible to do, however how do we install this? We need to install this in some private layout.

Rodolphe Lepigre (Jun 05 2023 at 15:03):

Dune has a notion of private module, I think, maybe that could be built upon. But I have no idea.

Ali Caglayan (Jun 05 2023 at 15:06):

Karl Palmskog said:

asking regular users to find out (1) the exactly right path prefixes and (2) which of their deps are plugins, will unfortunately exclude most regular users from Dune at this point. I'd honestly advise most people to use coq_makefile until this is figured out (how to not have to know these things, like in coq_makefile)

(1) The same exists in OCaml. There is a distriction between a library and a package. In Coq we have theories and packages. The theory name is obvious if the dependency was built with Dune, and not that hard to know if build with coq_makefile.

I am not seeing how this will exclude regular users from Dune. Could you eloborate?

Karl Palmskog (Jun 05 2023 at 15:06):

most people who use Coq don't know what a plugin is, and it might take them several hours to figure out

Karl Palmskog (Jun 05 2023 at 15:07):

someone will tell them: just use Equations to do something, and then it doesn't compile with dune unless you do (plugins coq-equations)

Karl Palmskog (Jun 05 2023 at 15:08):

this would be solved (as hinted at by Gaëtan) if you don't have to declare transitive dependencies, and the plugin stuff was hidden by Equations itself

Ali Caglayan (Jun 05 2023 at 15:10):

How is Dune meant to know about the coq-equations plugin just from a theory name however? It will look for Equations as a prefix in the install directories, but I don't see how it can work out that there is an ml library attached to this.

Ali Caglayan (Jun 05 2023 at 15:11):

Is coq_makefile able to load plugins from just the -Q flags?

Karl Palmskog (Jun 05 2023 at 15:12):

I'm sure there is a good reason for the requirement to have (plugins coq-equations) right now, but I'm saying it inadvertently leads to that Dune-Coq 0.8 can't be used by ordinary users (who use one of the many plugins in the Coq Platform, for example)

Rodolphe Lepigre (Jun 05 2023 at 15:13):

Actually, I'm now thinking: could we not just reconstruct the deps with something like:

find $(opam var lib)/coq/user-contrib -type f -name "*.v" | xargs grep "Declare \+ML \+Module"

and some filtering (we probably want some kind of parsing to eliminate false positives).

Karl Palmskog (Jun 05 2023 at 15:17):

but is this really robust? Does it work on Nix, etc.? I can see it may help some determined people, but hard to see it as a long time solution with the find.

Rodolphe Lepigre (Jun 05 2023 at 15:18):

That would work if you respect the COQPATH I think, this is just a rough sketch of a possible implementation.

Rodolphe Lepigre (Jun 05 2023 at 15:26):

After a bit of cleanup, here is what I get in a random switch locally:

$ (cd $(opam var lib) && find coq/user-contrib -type f -name "*.v" | xargs grep "^ *Declare \+ML \+Module \+\".*\" *\.$") | \
    sed 's/\:Declare *ML *Module *\"\([^"]*\)\"./: \1/g' | sed 's/\(.*: \).*:\(.*\)/\1\2/g'
coq/user-contrib/Ltac2/Init.v: coq-core.plugins.ltac2
coq/user-contrib/MetaCoq/Template/Loader.v: coq-metacoq-template-coq.plugin
coq/user-contrib/MetaCoq/Template/ExtractableLoader.v: coq-metacoq-template-ocaml.plugin
coq/user-contrib/Mtac2/Base.v: coq-unicoq.plugin
coq/user-contrib/Mtac2/Base.v: coq-mtac2.plugin
coq/user-contrib/Unicoq/Unicoq.v: coq-unicoq.plugin
coq/user-contrib/Equations/Prop/Loader.v: coq-equations.plugin
coq/user-contrib/Equations/Init.v: ltac_plugin
coq/user-contrib/Equations/Init.v: coq-equations.plugin
coq/user-contrib/Equations/Type/Loader.v: coq-equations.plugin
coq/user-contrib/elpi/elpi.v: coq-elpi.elpi

Ali Caglayan (Jun 05 2023 at 15:26):

So the suggestions is for Dune to lex the "Declare ML Module" entries in a theory, and create a plugins field according to that? What would happen if there are library dependencies of the plugin?

Rodolphe Lepigre (Jun 05 2023 at 15:27):

Well, you get findlib packages in the Declare ML Module, right? So you can let dune handle the deps.

Rodolphe Lepigre (Jun 05 2023 at 15:28):

It is not quite right, since opam package and findlib packages are not exactly the same thing, but close enough I guess?

Rodolphe Lepigre (Jun 05 2023 at 15:32):

I guess that if coq-equations.plugin is not an opam package, you can depend on coq-equations instead, eliminating one suffix part at a time, and continue doing so until you hit an opam package.

Ali Caglayan (Jun 05 2023 at 15:35):

A while back I did an experiment called "coqmod" where essentially Dune lexed the .v files itself, bypassing coqdep. I did this so we could quickly and easily resolve dependencies between .v files, and furthermore it allowed us to guess the plugins field like you've suggested above.

Ali Caglayan (Jun 05 2023 at 15:36):

I stopped working on it to focus on installed composition, but maybe it is worth redoing some ideas from there since there is a demand for not writing the plugins field.

Ali Caglayan (Jun 05 2023 at 15:38):

It would be helpful if you could open a Dune issue so we can track such a feature. As for now, I disagree with @Karl Palmskog that it is a barrier for users. I think that with some well written documentation it could be resolved. It's really as simple as saying:

1. if you need a theory -> theories field
2. if you need a plugin -> plugins field

Ali Caglayan (Jun 05 2023 at 15:39):

Sure its more verbose, but its not like you will be writing a dune file all the time. You will do it once really per project with some minor tweaks.

Gaëtan Gilbert (Jun 05 2023 at 15:40):

the barrier is "I'm trying to use metacoq and it complains that it can"t fnd equations"
the metacoq user should not need to know that metacoq depends on equations

Rodolphe Lepigre (Jun 05 2023 at 15:40):

Yeah, but the problem is that if you depend on some Coq theories, that themselves (but not you directly) depend on, say, coq-equations, they you still need to specify the plugin.

Ali Caglayan (Jun 05 2023 at 15:42):

Do you not have the same issue with a coq_makefile project? You need to include the -I flags for equations when using metacoq?

Ali Caglayan (Jun 05 2023 at 15:47):

Anyway the reason I am asking is that we've been focusing on making sure that dune can do everything coq_makefile can do. Anything more would be a feature on top. If there isn't an obvious counter example, the feature proposed above (auto-detecting the plugins field) seems fine to me.

Gaëtan Gilbert (Jun 05 2023 at 15:49):

Ali Caglayan said:

Do you not have the same issue with a coq_makefile project? You need to include the -I flags for equations when using metacoq?

not AFAIK
everything findlb can find coq can also find

Paolo Giarrusso (Jun 05 2023 at 17:30):

Do you not have the same issue with a coq_makefile project? You need to include the -I flags for equations when using metacoq?

coq_makefile just gives you all of user-contrib unconditionally, so how would that ever show up? just like dune did that before 0.8

Paolo Giarrusso (Jun 05 2023 at 17:34):

in fact, since coq _on its own_ can autoload plugins when required by .vo files in user-contrib, the question is how does dune disable that, and whether it should.

Paolo Giarrusso (Jun 05 2023 at 17:35):

Maybe that's necessary so that dune _can_ track the dependency of the installed plugin — _that_ is the case where you must pass -I to coq_makefile

Paolo Giarrusso (Jun 05 2023 at 17:39):

indeed, you _can_ write in _CoqProject -Q ../random/theories prefix -I ../random/plugin even when random is already with (with either coq_makefile or dune, tho IIRC @Rodolphe Lepigre had to plug in work for the latter case): then coqdep _will_ emit dependencies to the random library and plugin and Makefile will track them correctly and rebuild your project when the dependency changes.

Gaëtan Gilbert (Jun 05 2023 at 17:42):

plugins don't go in user-contrib, they go in some lib/ directory findlib knows about (coq_makefile does literally ocamlfind install)

Paolo Giarrusso (Jun 05 2023 at 17:42):

you're right, but either way the normal user doesn't need to know :-)

Karl Palmskog (Jun 05 2023 at 17:45):

actually, coq_makefile to my knowledge puts the cmxs file both in user-contrib/<Prefix> and also elsewhere by doing ocamlfind install.

Paolo Giarrusso (Jun 05 2023 at 17:45):

yes, but the META is only in the later place

Paolo Giarrusso (Jun 05 2023 at 17:45):

In sum, IIUC: _if_ you want to track dependencies against already-built code, I agree with @Ali Caglayan that this is similarly hard with coq_makefile and dune. But @Karl Palmskog is right, because today next to nobody does it with coq_makefile, but everybody has to with dune-coq 0.8

Paolo Giarrusso (Jun 05 2023 at 17:46):

here's equations_plugin.cmxs on my switch:

$ ls /Users/pgiarrusso1/.opam/4.14.1+flambda/lib/coq-equations/
META             covering.cmi  depelim.cmx  eqdec.cmi      equations.cmx         equations_plugin.cmxa  extra_tactics.cmx
noconf.cmi      noconf_hom.cmx  principles_proofs.cmi  sigma_types.cmx  splitting.cmi  subterm.cmx
context_map.cmi  covering.cmx  ederive.cmi  eqdec.cmx      equations_common.cmi  equations_plugin.cmxs
g_equations.cmi    noconf.cmx      principles.cmi  principles_proofs.cmx  simplify.cmi     splitting.cmx  syntax.cmi
context_map.cmx  depelim.cmi   ederive.cmx  equations.cmi  equations_common.cmx  extra_tactics.cmi
g_equations.cmx    noconf_hom.cmi  principles.cmx  sigma_types.cmi        simplify.cmx     subterm.cmi    syntax.cmx
$ ls /Users/pgiarrusso1/.opam/4.14.1+flambda/lib/coq/user-contrib/Equations/
CoreTactics.glob  CoreTactics.v  CoreTactics.vo  Init.glob  Init.v  Init.vo  Prop  Signature.glob  Signature.v  Signature.vo
Type  equations_plugin.cmxs

Karl Palmskog (Jun 05 2023 at 17:48):

I have:

ls ~/.opam/4.14.1+flambda+coq.8.16/lib/coq/user-contrib/Equations/
CoreTactics.glob  CoreTactics.v  CoreTactics.vo  equations_plugin.cmxs  Init.glob  Init.v  Init.vo
Prop  Signature.glob  Signature.v  Signature.vo  Type

Karl Palmskog (Jun 05 2023 at 17:49):

so the same as Paolo it seems

Paolo Giarrusso (Jun 05 2023 at 17:51):

should I expect that one .cmxs is used by legacy loading and the other by findlib loading — so which is needed depends on style used in the .v file?

Gaëtan Gilbert (Jun 05 2023 at 17:52):

yes

Emilio Jesús Gallego Arias (Jun 05 2023 at 18:38):

I think that @Karl Palmskog 's error is due to a bug in 0.8

Emilio Jesús Gallego Arias (Jun 05 2023 at 18:39):

Indeed the legacy layout plugin install requires cmxs files to be in user-contrib too, Dune should add that path to the plugin loadpath.

Emilio Jesús Gallego Arias (Jun 05 2023 at 18:39):

@Ali Caglayan is 3.8.1 out already? If so we'll need to add this fix to 3.8.2

Emilio Jesús Gallego Arias (Jun 05 2023 at 18:43):

In fact I think we had code for this in the first resolution implementation Ali did, but seems like it was lost in the rewrite. However I am kind of puzzled as we are correctly adding the -I paths for the stdlib, so we should also add them for Equations for example.

Emilio Jesús Gallego Arias (Jun 05 2023 at 18:44):

Paolo Giarrusso said:

in fact, since coq _on its own_ can autoload plugins when required by .vo files in user-contrib, the question is how does dune disable that, and whether it should.

Coq doesn't really "autoload", it just scans all directories and adds all of them to the plugin search path. Dune tells Coq not to do this, and instead does its own scanning, hiding the parts of the user-contrib that you don't want to show up.

Karl Palmskog (Jun 05 2023 at 18:45):

OK, for the record I was testing this project which uses Equations: https://github.com/runtimeverification/vlsm
and this is what theories/VLSM/dune has to look like to work with 3.8.0:

(coq.theory
 (name VLSM)
 (package coq-vlsm)
 (synopsis "Core definitions in Coq for VLSMs")
 (theories stdpp Cdcl Equations)
 (plugins coq-equations coq-itauto)
 (flags :standard
   -w -future-coercion-class-field
   -w -deprecated-tacopt-without-locality))

(include_subdirs qualified)

Emilio Jesús Gallego Arias (Jun 05 2023 at 18:47):

Gaëtan Gilbert said:

shouldn't plugin dependencies be transitive? ie equations theory depends on equations plugin, so anything depending on equations theory also depends on equations plugin

Yes, but this requires to install a .dune-pkg file with this metadata, we hope to do that at some point (contributions welcome).

However for (lang coq 1.0) the goal is to be 100% compatible with coq_makefile projects, so indeed the situation is:

• Dune can't know about dependencies of theories because we don't record this info yet (neither does coq-makefile)
• Dune can indeed determine the plugin loadpath from (theories Equations) as the .cmxs file is next to the .vo files when installed in the "legacy" layout.

Karl Palmskog (Jun 05 2023 at 18:47):

the error is triggered by:

From Equations Require Export Equations.

Emilio Jesús Gallego Arias (Jun 05 2023 at 18:48):

Thanks @Karl Palmskog , this seems like a bug, can you open an issue in Dune repos?

Karl Palmskog (Jun 05 2023 at 18:48):

OK, let me try if I can minimize it first

Karl Palmskog (Jun 05 2023 at 19:02):

https://github.com/ocaml/dune/issues/7893

Emilio Jesús Gallego Arias (Jun 05 2023 at 20:45):

Fix at https://github.com/ocaml/dune/pull/7895

Emilio Jesús Gallego Arias (Jun 05 2023 at 20:45):

We had a pretty serious bug in the path scanning !

Emilio Jesús Gallego Arias (Jun 05 2023 at 20:46):

And indeed I bet we reversed the logic on some parts of the test suite, otherwise I can't explain the tests passed.

Indeed as I discussed with Ali, would be great if people using Dune could be sure that their use case is properly reflected in Dune's test suite.

Emilio Jesús Gallego Arias (Jun 05 2023 at 20:46):

Creating tests is very easy!

Karl Palmskog (Jun 06 2023 at 13:27):

the test cases I can imagine:

• extracting Coq code to OCaml to build a Coq plugin, then use the Coq plugin in another package
• monorepo project with 3-4 packages where some packages depend on each other and some don't

Ali Caglayan (Jun 06 2023 at 14:46):

@Karl Palmskog can you expand on your second idea?

Karl Palmskog (Jun 06 2023 at 14:51):

I'm just saying this is how we use Dune in several places in Coq-community, most prominently in https://github.com/coq-community/hydra-battles

Emilio Jesús Gallego Arias (Jun 06 2023 at 16:58):

Thanks Karl, can you add these cases to https://github.com/ocaml/dune/issues/7598 ?

Karl Palmskog (Jun 06 2023 at 17:17):

I mean, minimizing code representing these use cases in a meaningful way is not trivial, probably around an hour's work. Can you maybe point to some code to use as template in the issue?

I can describe the use cases as a comment in the issue, but don't have enough cycles this week to provide code.

Emilio Jesús Gallego Arias (Jun 06 2023 at 17:55):

I think a brief description of the uses cases is good for now.

Emilio Jesús Gallego Arias (Jun 06 2023 at 17:56):

The idea of the issue is to build the Coq Dune test matrix, once the test matrix feels complete we need to review what items are covered, which ones are not, and then implement

Karl Palmskog (Jun 20 2023 at 10:32):

Dune 3.8.2 with Emilio's fix for the plugin issue is now out on opam. I tested it locally on the project where I previously found the bug, and now dune build works great.

Emilio Jesús Gallego Arias (Jun 20 2023 at 12:05):

Thanks for the feedback @Karl Palmskog , there are still some minor issues lurking around, but I think that 8.17.1 + Dune 3.8.2 provides a full preview of what to expect for a fully working Dune + Coq setup.

Emilio Jesús Gallego Arias (Jun 20 2023 at 12:06):

I don't have time this week, but it is time to update the plugin template etc...

Emilio Jesús Gallego Arias (Jun 20 2023 at 12:06):

And maybe find a better place for it, I guess we could move it to Coq Community?

Emilio Jesús Gallego Arias (Jun 20 2023 at 12:07):

Actually the Coq + Dune mode could be maintained by Coq Community, but unfortunately Dune still works as a mono repos... Would be nice to figure out a way to do it tho.

Théo Zimmermann (Jun 20 2023 at 12:14):

The Coq + Dune mode is probably better in the Dune repository with the people who know how Dune works.

Théo Zimmermann (Jun 20 2023 at 12:14):

However, it makes sense indeed to have the plugin example repo in Coq-community (with the people who are experienced in maintained Coq packages).

Emilio Jesús Gallego Arias (Jun 20 2023 at 12:33):

Théo Zimmermann said:

The Coq + Dune mode is probably better in the Dune repository with the people who know how Dune works.

As of today yes, however in the medium term it is not so far-fetched to think of Coq people maintaining the build rules.

Dune mainly provides a language to write rules, and some helpers such as stanza parsing etc... So the Dune Coq mode hooks into dune in the following way:

• when scanning sources, keep track of .v files
• for each Coq stanza found, interpret it. Stanzas are used in two ways:
  • to generate a set of rules
  • to generate the DB of Coq theories

The set of rules is much specific to Coq, as it is the DB of Coq theories, and quite independent of the rest of Dune.

Dune's API used by the Coq rules is not large, basically:

• resolution of binaries to find coqc etc...
• regular rule building tools (Memo, Action_builder, Command)
• variable expansion in stanzas
• lookup for ML artifacts (for ML plugin support)

Gaëtan Gilbert (Jun 20 2023 at 12:34):

maybe someday dune will support plugins, then coqdune can be split off

Emilio Jesús Gallego Arias (Jun 20 2023 at 12:40):

Gaëtan Gilbert said:

maybe someday dune will support plugins, then coqdune can be split off

That has been in the Dune roadmap for a long time, main problem is that reaching a stable API is not easy and moreover quite costly.

Emilio Jesús Gallego Arias (Jun 20 2023 at 12:41):

But if we put API / code issues to one side, the real matter is "what the Coq rules are", this is something to be decided by the Coq users / community / team.

Ali Caglayan (Jun 20 2023 at 21:51):

"dune plugins" that allow the access needed for the coq features is not coming anytime soon unfortunately. There are other focues in Dune atm such as package management and distributed cache.

Ali Caglayan (Jun 20 2023 at 21:52):

There are also not many use cases for it. So far it is only Coq that needs such access and it wouldn't be worth designing a whole API for a single user when it works fine in the main repo today.

Emilio Jesús Gallego Arias (Jun 20 2023 at 21:56):

Yes, it won't happen any time soon I think. I'd be nice if we could actually have a better way to maintain Dune with Coq Community

Emilio Jesús Gallego Arias (Jun 20 2023 at 21:56):

thinking about it

Ali Caglayan (Jun 20 2023 at 21:59):

stablise the plugin would be a start. We are heading that direction anyway now that we have installed theories out of the way.

Last updated: Oct 13 2024 at 01:02 UTC