From a package manager¶
Alt-ergo is available on opam, the ocaml package manager with the following command :
opam install alt-ergo
You can also install the GUI with
opam install altgr-ergo
This two command will install the Alt-ergo library
alt-ergo-lib and the parsers
alt-ergo-parsers, as well as other librairies detailled in dependencies.
External dependencies graph generated with
make archi for source files dependencies):
To compile the sources, you will need the following libraries :
ocaml >= 4.05.0 dune >= 2.0 zarith camlzip menhir ocplib-simplex >= 0.4 seq cmdliner stdlib-shims psmt2-frontend
To compile the GUI you will also need
You may need superuser permissions to perform the installation.
./configureto generate Makefile.config, in order to build everything (lib, parsers, binaries, and GUI).
Alternatively, you can configure with
./configure -prefix some-absolute-path-prefixto add a prefix for installation directories. You may also want to use
make gen && cat lib/util/config.mlto see directories where things will be installed.
You can use
./configure <package>to select which package you want to build.
<package>may be one of: alt-ergo-lib, alt-ergo-parsers, alt-ergo, altgr-ergo.
Build and Install¶
The steps below will build and install native or bytecode binaries depending on whether ocamlopt is installed or only ocamlc is detected.
Everything (binaries, plugins, library, …)¶
The steps below will build and install additional plugins (extension .cmxs if ocamlopt is installed or .cma if only ocamlc is detected).
The SatML Plugin¶
satML is now inlined and compiled directly with Alt-Ergo’s source code
The Fm-Simplex Plugin¶
The Fm-Simplex plugin is currently built and installed at the same time as the alt-ergo binary.
The AB-Why3 parser plugin¶
The AB-Why3 plugin is currently built and installed at the same time as the alt-ergo binary.
You can find more information in the AB-Why3 README
The profiler plugin¶
This plugin has been “inlined” in Alt-Ergo sources.