Join GitHub today
GitHub is home to over 36 million developers working together to host and review code, manage projects, and build software together.Sign up
[RFC] dune plugins #1855
This ticket describes a very simple plugin system for dune.
The aim of this proposal is to provide a simple form of extensibility to users, so that they can share common parts of their dune files in one place.
The simple is very simple and allows users to define new stanzas. User defined stanzas are translated to vanilla stanzas using functions written in OCaml. For now, the system is completely untyped, but we are hopping to evolve it into something more structured in the future.
This proposal makes sure that the use of plugins won't negatively impact the functioning of dune. In particular, building the plugins must be as fast as possible and shouldn't introduce too much staging.
The system provides the following function:
val Dune_plugin.V1.define_stanza : string -> Dune_lang.Ast.t -> Dune_lang.Ast.t list
this function will be used to expand stanzas of the form
Definition of plugins
Plugins are defined in files called
What can plugins do
Dune plugins can only be composed of a single module and cannot use libraries. They cannot use code from other plugins either. These limitations are to ensure we can build all the mappers as fast as possible and without introducing too much staging in the process. We might lift these limitations in the future if everything goes well.
The stanzas defined in a
Dune will compile and link all the
Dune will then execute this executable with as argument a file containing the list of queries. A query is composed of:
In return, this executable should provide a list of response. A response being:
The last point will allow dune to cache the output of plugins between runs.
Allow plugins to be packaged so that they can be reused by other projects.
Looking at this again, maybe we should just call these things plugins to be more generic. i.e. apply the following renaming:
We might want to add more functionalities here that are not just mappers.
Reading this again, we can start by not providing full file mappers. i.e. this should be enough to start with and will be easier to evolve into somethting more principled:
Does that mean at most one by directory? Why should we crawl all the workspace? Two projects could have competing plugins.
I would propose to restrict at least by project, or could we have a stanza in a dune file that tells which plugins to use for preprocessing the stanzas of the file?
Yes, at most one per directory. I propose to use the usual scoping: a
This proposal doesn't cover sharing plugins between projects. To do that, I had in mind something like this: we would declare in the
From the dune dev meeting:
With more though I would prefer to have a stanza
I thought a bit more about this and the only limitation it would have for my test uses cases is that I cannot call
I guess I could indeed add a special API for this to the plugin API as part of the Coq PR.