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.

AB why3 plugin (deprecated)

Warning

The AB Why3 plugin requires the use of the --frontend legacy option, which is deprecated and will be removed in the next version of Alt-Ergo.

If you are using this plugin and would like it to be available in new versions of Alt-Ergo, please contact the Alt-Ergo developers.

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