Package Details: alt-ergo 2.3.0-2

Git Clone URL: (read-only, click to copy)
Package Base: alt-ergo
Description: SMT solver for software verification
Upstream URL:
Keywords: sat-solver smt-solver
Licenses: custom:CeCILL-C
Submitter: mgrabovsky
Maintainer: None
Last Packager: Alad
Votes: 1
Popularity: 0.000000
First Submitted: 2016-03-23 18:59
Last Updated: 2019-11-30 19:49

Latest Comments

RobinWA commented on 2021-01-06 16:10

I can't get this build to work (see error below). A quick google search of the error points to some kind of incompatiblity with ocaml-num but I'm not sure how to handle it. Does anyone have an idea what to do here?

If you need to stay compatible with OCaml < 4.07, you can use the 
stdlib-shims library:
File "_none_", line 1:   
Error: Files /usr/lib/ocaml/num/nums.cmxa and /usr/lib/ocaml/stdlib.cmxa
       make inconsistent assumptions over implementation Stdlib__sys
File "tools/gui/", line 391, characters 20-34:
391 |             assert (Pervasives.(=) v v');

radrow commented on 2019-06-27 13:48

I get following error:

checking for ocp-ocamlc... no
checking for ocamlc... ocamlc
ocaml version is 4.07.1
ocaml library path is /usr/lib/ocaml
checking for ocamlfind... yes
ocamlfind: Package `zarith' not found
checking for /usr/lib/ocaml/zarith/zarith.cma... yes
ocamlfind found num in -I /home/radek/.opam/system/lib/num
ocamlfind: Package `camlzip' not found
checking for /usr/lib/ocaml/zip/zip.cma... yes
ocamlfind: Package `ocplib-simplex' not found
configure: error: Cannot find ocplib-simplex library.

NieDzejkob commented on 2019-04-23 19:34

Does not build:

File "/home/kuba/.cache/aurman/alt-ergo/src/alt-ergo-2.2.0/sources/parsers/smt2/", line 47, characters 17-21:
Error: This expression has type (Lexing.position * Lexing.position) option
       but an expression was expected of type
         Loc.t = Lexing.position * Lexing.position
make: *** [Makefile.users:305: parsers/smt2/psmt2_to_alt_ergo.cmx] Error 2

I have minutes of OCaml experience, but I think it might be caused by ocaml-psmt2-frontend-git, considering the error path.

Edit: updating to 2.3.0 fixes the issue. You'll need to add dune to makedepends and remove the autoconfig line.

untitled commented on 2018-08-28 10:55

To update to version 2.2.0, the following diff can be applied:

diff --git a/PKGBUILD b/PKGBUILD
index 6691d4d..f34e0b1 100644
@@ -1,28 +1,28 @@
 # Maintainer: Matej Grabovsky <matej.grabovsky at="" gmail="">
 pkgdesc='SMT solver for software verification'
 arch=('i686' 'x86_64')
-depends=('gtksourceview2' 'zarith')
+depends=('gtksourceview2' 'ocaml-zarith' 'ocaml-zip' 'ocaml-ocplib-simplex-git' 'ocaml-psmt2-frontend-git')

 build() {
-    cd "$srcdir/$pkgname-$pkgver"
-    ./configure -prefix /usr
+    cd "$srcdir/$pkgname-$pkgver/sources"
+    autoconf
+    ./configure --prefix=/usr
     make gui

 package() {
-    cd "$srcdir/$pkgname-$pkgver"
+    cd "$srcdir/$pkgname-$pkgver/sources"
     make DESTDIR="$pkgdir" install
     make DESTDIR="$pkgdir" install-gui
-    install -Dm644 LICENSE "${pkgdir}/usr/share/licenses/${pkgname}/LICENSE"

 # vim:set et sw=4 sts=4 et:

mgrabovsky commented on 2016-12-31 17:12

@IooNag: Sorry, I'm having some trouble compiling the latest version right now.

IooNag commented on 2016-12-31 11:54

alt-ergo version 1.01 is no longer available on . The package needs to be updated to version 1.30.
Moreover could you please add the version number to the downloaded archive, for example by using this line do define "source"?