Improved support for build-time Fl_dynload ?

[ejgallego]

Dear findlib maintainers,

in Coq we have started to use Fl_dynload to allow the loading of Coq's plugins that have dependencies. Also, this means we identify our plugin namespace with findlib's namespace which I think is a good think.

However, we are facing some limitations to make this work at build-time with dune (so we can compose packages, etc...)

In particular, when generating the build rules for a .v file that depends on a plugin, we need to translate a findlib library name pkg.foo to the plugin .cmxs file, while we are in the build layout. We face two problems here:

• findlib's package path is determined at initialization time, moreover it seems we can use some of the API without calling init and init will be called automatically. Should maybe the contract be made stronger? Would a more dynamic handling of the include path make sense?

• a critical problem is that Dune generates _build/default/META.coq-core , however that file is not usable as it is meant to be installed in _build/install/lib/coq-core/META, thus findlib will complain that a top-level directory field is missing. Would making the API more flexible make sense?

• an alternative choice would be to depend on installed plugins and libraries, however that may be problematic for Dune's build / install phase separation. On the other hand, maybe that is what we should do, as the scheme Coq has adopted requires plugins to be public (which is IMHO a bit unfortunate, but that's an orthogonal problem)

cc @Alizter @rgrinberg @gares

[gares]

I think dune should generate two META files, one META.coq-core for the build layout (with the directory directive) and another one for the installed layout, in a hidden place.

[ejgallego]

@gares that would be nice, but I'm not sure it is possible. In the build layout, users are free to setup their sources in a lot of different ways, that's not going to work always with ocamlfind I'm afraid. In fact, I now realize that what I propose would only work for Coq and not in general. So we are in bad spot.

[Alizter]

We could always fork/vendor findlib ourselves giving us full control and saving the findlib maintainers from having to resolve our qualms.

[gares]

The file META.coq-core produced by dune in the source tree is not usable by findlib. As I said elsewhere, this is a bug.
I don't think it makes sense to ask findlib to tolerate it.

users are free to setup their sources in a lot of different ways, that's not going to work always with ocamlfind I'm afraid.

If a user puts an invalid META file in his sources, it is not our problem. Also, if you have a META.pkg-name file at the root of your project, dune complains (since there is an hard coded rule to produce it), so I'm not sure this scenario is possible at all.

We could always fork/vendor findlib ourselves giving us full control and saving the findlib maintainers from having to resolve our qualms.

vendoring a patched copy of the META file parser is surely a way to circumvent the bug in dune, but frankly it would make more sense to patch dune. It can surely generate a META.pkg with the directory directive, and a META.pkg.for-install which is then symlinked in the _build/install folder. I don't see the difficulty with that, really.