Installation¶
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.
From sources¶
Dependencies¶
External dependencies graph generated with dune-deps
(use 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
lablgtk2
gtksourceview2
You may need superuser permissions to perform the installation.
Configuration¶
Configure with
./configure
to generate Makefile.config, in order to build everything (lib, parsers, binaries, and GUI).Alternatively, you can configure with
./configure -prefix some-absolute-path-prefix
to add a prefix for installation directories. You may also want to usemake gen && cat lib/util/config.ml
to 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, …)¶
Compile with
make
Install with
make install
Uninstall with
make uninstall
Alt-Ergo library¶
Compile with
make alt-ergo-lib
Install with
make install-lib
Alt-Ergo parsers¶
Compile with
make alt-ergo-parsers
Install with
make install-parsers
Alt-Ergo binary¶
Compile with
make alt-ergo
Install with
make install-bin
AltGr-Ergo binary¶
Compile with
make altgr-ergo
Install with
make install-gui
Plugins¶
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¶
Compile with
make fm-simplex
The Fm-Simplex plugin is currently built and installed at the same time as the alt-ergo binary.
The AB-Why3 parser plugin¶
Compile with
make AB-Why3
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.