Stream: Dune devs & users

Topic: Renaming libraries field to plugins


view this post on Zulip Ali Caglayan (Jun 02 2022 at 16:15):

cc @Emilio Jesús Gallego Arias @Rudi Grinberg

view this post on Zulip Ali Caglayan (Jun 02 2022 at 16:16):

For coq.theory, we should rename the libraries field to plugins

view this post on Zulip Ali Caglayan (Jun 02 2022 at 16:16):

because they are, you know, plugins

view this post on Zulip Emilio Jesús Gallego Arias (Jun 02 2022 at 16:17):

a plugin is just a library tho; my reasoning for the name choice is that the field is exactly the same as the field in the OCaml stanzas.

I am not a fan of different names for the same concept.

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

Dynamic linking could make things different, but if you still have in mind static linking, then the field has almost the same exact semantics then.

view this post on Zulip Rudi Grinberg (Jun 02 2022 at 17:13):

Note that there are distinctions between libraries and plugins:

  1. libraries are sometimes transitive (depends on a project setting) while plugins are always
  2. only libraries in OCaml are allowed select and re_export forms
    Imo, there's a bigger similarity between libraries in coq.theory and dune's (preprocess (pps ..)) specifications

view this post on Zulip Rudi Grinberg (Jun 02 2022 at 17:14):

The last point is subjective but I find it weird that coq uses the plugin terminology and then dune switches it to libraries

view this post on Zulip Emilio Jesús Gallego Arias (Jun 03 2022 at 08:12):

Yeah, (libraries ...) is much weaker than general form as it really means "we will dynload this" (or we will Fl_dynload this now).

view this post on Zulip Emilio Jesús Gallego Arias (Jun 03 2022 at 08:19):

Which basically translate to:

view this post on Zulip Emilio Jesús Gallego Arias (Jun 03 2022 at 08:19):

for the new system

view this post on Zulip Emilio Jesús Gallego Arias (Jun 03 2022 at 08:19):

So it is pretty simple actually

view this post on Zulip Rudi Grinberg (Jun 03 2022 at 14:21):

Due to those additional reasons, the name plugins seems more appropriate

view this post on Zulip Emilio Jesús Gallego Arias (Jun 04 2022 at 10:07):

Ok, then I guess if you folks feel like plugin is better, we can deprecate (libraries in 0.4 and turn it into plugins


Last updated: Jan 30 2023 at 17:03 UTC