Stream: Dune devs & users

Topic: Renaming libraries field to plugins

Ali Caglayan (Jun 02 2022 at 16:15):

cc @Emilio Jesús Gallego Arias @Rudi Grinberg

Ali Caglayan (Jun 02 2022 at 16:16):

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

Ali Caglayan (Jun 02 2022 at 16:16):

because they are, you know, plugins

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.

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.

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

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

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

Emilio Jesús Gallego Arias (Jun 03 2022 at 08:19):

Which basically translate to:

• "Pass the right -I paths to coqc/coqdep" so the cmxs are found (the actual dep to the cmxs is emitted by coqdep which is cool)
• "Build the meta file and setup OCAMLPATH" so the cmxs are found using findlib (still coqdep emits the cmxs dep)

Emilio Jesús Gallego Arias (Jun 03 2022 at 08:19):

for the new system

Emilio Jesús Gallego Arias (Jun 03 2022 at 08:19):

So it is pretty simple actually

Rudi Grinberg (Jun 03 2022 at 14:21):

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

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: Jun 04 2023 at 22:30 UTC