cc @Emilio Jesús Gallego Arias @Rudi Grinberg
For coq.theory, we should rename the libraries field to plugins
because they are, you know, plugins
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.
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.
Note that there are distinctions between libraries and plugins:
(preprocess (pps ..))specifications
The last point is subjective but I find it weird that coq uses the plugin terminology and then dune switches it to libraries
(libraries ...) is much weaker than general form as it really means "we will dynload this" (or we will Fl_dynload this now).
Which basically translate to:
for the new system
So it is pretty simple actually
Due to those additional reasons, the name plugins seems more appropriate
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