feat(plugins): Use dune-site for inequalities plugins

We already use dune-site to manage plugin files. With this patch, we now
also use the dune-site mechanism to manage plugin loading for the
inequalities plugin. This should make alt-ergo work with bytecode-only
compilers again (see [1]).

We still use Dynlink directly for additional parsers. Support for parser
plugins is deprecated as it is not supported with the Dolmen frontend
and will be removed in a future release, so the churn doesn't seem worth
it.

Fixes OCamlPro#1047

[1] : ocaml/opam-repository#25294

docs/sphinx_docs/Usage/index.md

@@ -238,16 +238,10 @@ See the [AB-Why3 README] file for the documentation of the AB-Why3 plugin
 
 The Fm-Simplex plugin can be used as follows:
 
-        $ alt-ergo --inequalities-plugin fm-simplex-plugin.cmxs [other-options] file.<ext>
-        $ alt-ergo --inequalities-plugin some-path/fm-simplex-plugin.cmxs [other-options] file.<ext>
+        $ alt-ergo --inequalities-plugin fm-simplex [other-options] file.<ext>
 
-   Alt-Ergo will try to load a local plugin called
-   "fm-simplex-plugin.cmxs". If this fails, Alt-Ergo tries to load it
-   from the default plugins directory (run `alt-ergo --where plugins`
-   to see its absolute path). You can also provide a relative or an
-   absolute path as shown by the second command above. Also, you
-   should replace ".cmxs" by ".cma" if you are working with bytcode
-   binaries.
+The inequalities plugins are [Dune-site plugins] registered in the `(alt-ergo
+plugins)` site. The `fm-simplex` plugin comes built-in with Alt-Ergo.
 
 ### Preludes
 
@@ -339,3 +333,4 @@ A small example of how to use the Alt-Ergo web worker can be build with the comm
 [API documentation]: ../API/index.md
 [AB-Why3 README]: ../Plugins/ab_why3.md
 [Input section]: ../Input_file_formats/index
+[Dune-site plugins]: https://dune.readthedocs.io/en/stable/sites.html#plugins

src/bin/common/config.ml

@@ -20,3 +20,14 @@ let lookup_file locations filename =
 let lookup_prelude = lookup_file preludes_locations
 
 let lookup_plugin = lookup_file plugins_locations
+
+let load_plugin plugin =
+  try
+    AltErgoSites.Plugins.Plugins.load plugin
+  with e ->
+    AltErgoLib.Errors.run_error
+      (Dynlink_error
+         (Format.asprintf
+            "@[<v>Loading the plugin %S failed!@,\
+             >> Failure message: %s"
+            plugin (Printexc.to_string e)))

src/bin/common/dune

@@ -12,6 +12,7 @@
    stdlib-shims
    cmdliner
    dune-site
+   dune-site.plugins
  )
  (modules
    Config
@@ -25,4 +26,6 @@
 
 (generate_sites_module
  (module AltErgoSites)
- (sites alt-ergo))
+ (sites alt-ergo)
+ (plugins
+  (alt-ergo plugins)))

src/bin/common/parse_command.ml

@@ -1318,12 +1318,14 @@ let parse_theory_opt =
       | "" ->
         if debug then
           Printer.print_dbg
-            "[Dynlink] Using the 'FM module' for arithmetic inequalities";
+            "Using the 'FM module' for arithmetic inequalities";
         Ok ()
       | path ->
         try
-          MyDynlink.load debug path
-            "'inequalities' reasoner (FM module)";
+          Config.load_plugin path;
+          if debug then
+            Printer.print_dbg
+              "Using the 'inequalities' reasoner (FM module) %S" path;
           Ok ()
         with Errors.Error e ->
           Error (Format.asprintf "%a" Errors.report e)

src/plugins/fm-simplex/dune

@@ -3,13 +3,13 @@
   (mld_files :standard))
 
 (library
+ (public_name alt-ergo.plugins.fm-simplex)
  (name FmSimplexPlugin)
  (libraries alt-ergo-lib)
  (modules Simplex Simplex_cache FmSimplexIneqs))
 
-(install
+(plugin
  (package alt-ergo)
- (section (site (alt-ergo plugins)))
- (files
-  FmSimplexPlugin.cma
-  FmSimplexPlugin.cmxs))
+ (name fm-simplex)
+ (libraries alt-ergo.plugins.fm-simplex)
+ (site (alt-ergo plugins)))

tests/cram.t/run.t

@@ -1,6 +1,5 @@
-  $ echo '(check-sat)' | alt-ergo --inequalities-plugin does-not-exist -i smtlib2 -o smtlib2 2>&1 >/dev/null | sed -E 's/(error loading shared library):.*/\1/'
-  alt-ergo: Fatal Error: [Dynlink] Loading the 'inequalities' reasoner (FM module) plugin in "does-not-exist" failed!
-            >> Failure message: error loading shared library
+  $ echo '(check-sat)' | alt-ergo --inequalities-plugin does-not-exist -i smtlib2 -o smtlib2 2>&1 >/dev/null | sed -e '/^[[:space:]]*>>/d'
+  alt-ergo: Fatal Error: [Dynlink] Loading the plugin "does-not-exist" failed!
 
 Now we will have some tests for the models. Note that it is okay if the format
 changes slightly, you should be concerned with ensuring the semantic is