Plugins

Alt-Ergo releases on OPAM support dynamically loading plugins. The command alt-ergo --where plugins can be used to get the absolute path that is searched by default when looking for plugins.

Binary releases on GitHub use static linking for portability, and hence do not support plugins.

Inequality plugins

The fm-simplex inequality plugin comes built-in with Alt-Ergo and no further installation is required. It is distributed under the same licensing conditions as Alt-Ergo. It can be used as follows:

$ alt-ergo --inequalities-plugin fm-simplex [other-options] file.<ext>

Note

If you are a developer of an external inequality plugin, your plugin needs to be registered in the (alt-ergo plugins) site using dune-site to be available as an option to --inequalities-plugin.

• What is this plugin ?
• What this plugin is not ?
• How to use it ?
• Licensing