dolmen icon indicating copy to clipboard operation
dolmen copied to clipboard

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

Open bclement-ocp opened this issue 1 year ago • 5 comments

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 avatar May 06 '24 16:05 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 avatar May 06 '24 16:05 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 avatar May 07 '24 09:05 bclement-ocp

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

bclement-ocp avatar May 07 '24 10:05 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 avatar Jun 26 '24 09:06 bclement-ocp

@Gbury ping

bclement-ocp avatar Jul 09 '24 09:07 bclement-ocp