Installation
From a package manager
Alt-ergo is available on opam, the ocaml package manager with the following command :
opam install alt-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.
On Debian
Alt-ergo is also available in the debian package manager here. You can install it with the following command :
sudo apt install alt-ergo
From sources
Dependencies
External dependencies graph generated with dune-deps
(use make archi
for source files dependencies):
To compile the sources of the library alt-ergo-lib
and the binary alt-ergo
, you will need the
following libraries :
ocaml >= 4.08.0
dune >= 3.0
dune-build-info
dolmen >= 0.9
dolmen_loop >= 0.9
ocplib-simplex >= 0.5
zarith >= 1.4
seq
fmt
ppx_blob
camlzip >= 1.07
menhir
dune-site
cmdliner
psmt2-frontend >= 0.4
stdlib-shims
You can install dependencies using:
$ make deps
and create a development switch with:
$ make dev-switch
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.
Note: these are somewhat obsolete; nowadays you can just use dune
Everything (binaries, plugins, library, …)
Compile with
make
Install with
make install-all
Uninstall with
make uninstall-all
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
Alt-Ergo with Nodejs
You can install dependencies using:
$ make js-deps
Compile with
make js-node
For this build rule you will need the following aditional libraries :
js_of_ocaml between 4.0.1 and 5.0.1
zarith_stubs_js
Alt-Ergo web worker
Compile with
make js-worker
For this build rule you will need the following aditional libraries :
js_of_ocaml between 4.0.1 and 5.0.1
js_of_ocaml-lwt
zarith_stubs_js
data-encoding
Alt-Ergo web worker small example
Compile with
make js-example
This command create a www/
directory in which you can find a small js example running in the index.html
file
For this build rule you will need the following aditional libraries :
js_of_ocaml between 4.0.1 and 5.0.1
js_of_ocaml-lwt
js_of_ocaml-ppx
lwt_ppx
zarith_stubs_js
data-encoding
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.