Package Details: alt-ergo 2.3.0-2

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

Latest Comments

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/psmt2_to_alt_ergo.ml", 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
--- a/PKGBUILD
+++ b/PKGBUILD
@@ -1,28 +1,28 @@
 # Maintainer: Matej Grabovsky <matej.grabovsky at="" gmail="">
 pkgname=alt-ergo
-pkgver=1.01
+pkgver=2.2.0
 pkgrel=1
 pkgdesc='SMT solver for software verification'
 arch=('i686' 'x86_64')
 license=('custom:CeCILL-C')
 url='https://alt-ergo.ocamlpro.com'
-depends=('gtksourceview2' 'zarith')
+depends=('gtksourceview2' 'ocaml-zarith' 'ocaml-zip' 'ocaml-ocplib-simplex-git' 'ocaml-psmt2-frontend-git')
 makedepends=('lablgtk2')
-source=("${pkgname}::https://alt-ergo.ocamlpro.com/download_manager.php?target=alt-ergo-${pkgver}.tar.gz")
-sha256sums=('d51a9833acf265d475408cde04e9beb75f950355580b9c73292ffbfbebf280eb')
+source=("https://github.com/OCamlPro/alt-ergo/archive/${pkgver}.tar.gz")
+sha256sums=('61b09612be666d1f5ac0abcc41d94bae81e036cc07cd74898dd37f7fbf48da06')

 build() {
-    cd "$srcdir/$pkgname-$pkgver"
-    ./configure -prefix /usr
+    cd "$srcdir/$pkgname-$pkgver/sources"
+    autoconf
+    ./configure --prefix=/usr
     make
     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:
</matej.grabovsky>

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 https://alt-ergo.ocamlpro.com/ . 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"?

source=("${pkgname}-${pkgver}.tar.gz::https://alt-ergo.ocamlpro.com/download_manager.php?target=alt-ergo-${pkgver}.tar.gz")