Plugin loading is disturbed by optional dependencies
Hi!
We are facing issues when building a why3 plugin, due to its optional runtime dependencies. They make the build non-deterministic because linked libraries can differ depending on the installed optional dependencies. When dynamically linking a plugin, the libraries that have to be linked are therefore not deterministic either, since forgetting a link is obviously wrong, but linking to the same library twice is also rejected.
A concrete example to support this claim is the Gospel plugin:
- The plugin depends on
sexplib
. -
sexplib
is an optional dependency ofwhy3
. Therefore it may or may not be linked statically to thewhy3
executable. - Therefore,
- Linking
sexplib
in the plugin is wrong if it was already there forwhy3
; - Not linking
sexplib
in the plugin is wrong if it wasn't.
- Linking
These non-deterministic builds make it impossible to release the plugin, since it's not reliable enough for opam
users.
I can see at least one solution to this: move all dependencies to non-optional; plugins don't link to why3 dependencies.
- pro: I think this tends to be good practice for build reproducibility regardless of the plugin-specific issue.
- pro: You don't need to make a new release: we only have to modify the
opam
files. - con: Dependencies changes in
why3
can be breaking changes for plugins
I'm happy to open a merge request for this solution (or another one if you have a better idea, perhaps I'm doing something wrong on my end).
/cc @filliatr