feat: Add support for user-defined builtins with Dune plugins

[bclement-ocp]

This patch adds support for model extensions in Dolmen_loop using a similar mechanism to typing extensions.

Model extensions and typing extensions are now loaded by the binary through Dune's plugin mechanism, and the existing bvconv extension is moved to use the plugin mechanism.

Fixes #203

[bclement-ocp]

the existing bvconv extension is moved to use the plugin mechanism

In retrospect, I am not 100% sure this is a good idea. I did this initially to have an example of usage of the plugin mechanism, but ended up writing two example plugins (abs_real, abs_real_split) which I think is better for that purpose since. I am open to reverting this part of the change.

[bclement-ocp]

the existing bvconv extension is moved to use the plugin mechanism

This was causing build failures on the CI so no longer part of the PR. Instead there is support for builtin extensions when loading them at the CLI level.

[bclement-ocp]

I did some late cleanup but this should be ready to review @Gbury

[Gbury]

Overall this looks good.

Note: you can rebase on current master to fix the CI bugs.

[bclement-ocp]

Made the requested changes + some others following (old) offline discussions:

• Move code dealing with extensions out of the Options module and into
  a new Extensions module

• Clean up examples (notably avoid an almost-empty plugin in
  abs_real_split by defining the builtin in the typing plugin; it does
  not make sense to use the model plugin without the typing plugin)

• Load dune plugins lazily

• Use a hash table to find binary extensions (but not typing
  extensions/model extensions)

• Allow override of builtin extensions by dune plugins

[bclement-ocp]

@Gbury ping

[Gbury]

Oops, sorry for dropping the ball on this. What's the status of this one (just waiting for review or do we want to change the architecture of the PR) ?

[bclement-ocp]

It's been a while, I don't remember the conclusion of our last discussion. I'll go over the code again while applying review changes (probably sometime next week); if you are happy with the current architecture I'd say we keep it the way it is but if there are architectural issues we can fix them.

[bclement-ocp]

Rebased, looking at the review now.

[bclement-ocp]

Updated code for loading builtin extensions. I'm a bit unhappy about the fact that other modules loaded by the binary could create new extensions that would not get picked up (depending on module load order), but I think that's mostly a theoretical concern --- builtin extensions should be defined in the shared extension module, and plugin extensions should be defined in plugins (which are loaded dynamically and won't be seen when listing extensions at toplevel).

[Gbury]

Thanks a lot ! I have a few comments on how warnings and errors are reported around plugin loading, and after that it'll be good to merge.

[bclement-ocp]

Dropped the lazy and moved to use Dolmen's warning and errors.

[Gbury]

There's a CI failure: very likely, we need an additional lower bound on dune to use sites, and this will also induce a lower bound on the ocaml compiler version I suppose.

[bclement-ocp]

I have moved the dune-site dependency to the binary only since only the binary needs the Sites module now. Hopefully that should work.

[bclement-ocp]

Ah, this is actually a small issue — we need to decide whether we want plugins to be 100% a dolmen binary thing (and put them in the dolmen_bin namespace) or if we want them to go into the dolmen namespace (so that installed plugins could be accessed by other users of the Dolmen library).

I think both choices make sense — using the dolmen_bin namespace is a bit cleaner in terms of dependencies, but using the dolmen namespace would allow seamless integration with other tools using the Dolmen library (e.g. alt-ergo could pick up installed Dolmen plugins, which is nice). I'll let you make the call (in both cases this does not require changing the lower bound on either dune or the compiler -- just adding a dependency to dune-site >= 3.0 in addition to dune >= 3.0 for the appropriate package).

[bclement-ocp]

(Ignore the CI failures, I have botched things with an intermediate state between the two solutions — I should be able to make either of them work)

[bclement-ocp]

I have set the code back so that the plugins are registered with the dolmen library, even though they are used by the dolmen binary. I think this is the best course of action as it lets other binaries using the dolmen library access the plugins (through Dolmen.Sites) for seamless integration.

[Gbury]

Last round of questions !

[Gbury]

Great, this is good to merge ! If you want to write the CHANGES.md entry you can, else I'll do it right after merging.

[bclement-ocp]

Done!