Package Details: boolector-git r10285.6fce0ac3-1

Git Clone URL: (read-only, click to copy)
Package Base: boolector-git
Description: A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions
Upstream URL:
Keywords: boolector smt
Licenses: MIT
Conflicts: boolector
Provides: boolector
Submitter: deian
Maintainer: deian
Last Packager: deian
Votes: 0
Popularity: 0.000000
First Submitted: 2018-06-15 19:03
Last Updated: 2020-08-18 21:51

Dependencies (1)

Required by (4)

Sources (1)

Latest Comments

xiretza commented on 2021-07-15 10:15

A few things:

  • boolector is a compiled C++ application, so the package can't possibly be arch=('any').
  • building requires makedepends=('git' 'cmake').
  • downloading sources outside of source= is a no-no, especially when it's totally unnecessary - there's a lingeling package that can just be added as a dependency instead of using the bundled build script.
  • setting CFLAGS="" is just not ok. If there's an incompatibility with some default flag, either patch it upstream or, as a last resort, remove that specific flag from CFLAGS. As it stands right now, the build is completely fine without messing with any variables.
  • because MIT is not a common license, it needs to be installed to /usr/share/licenses/$pkgname/ by the PKGBUILD.
  • boolector has a testsuite, the PKGBUILD should offer the option of running it by providing a check() function.
  • the upstream repo has release tags, these should be incorporated into pkgver() and subsequently used for provides=.

Here's a patch that addresses all of those issues:

diff --git a/PKGBUILD b/PKGBUILD
index 297ec1e..450d78a 100644
@@ -1,49 +1,43 @@
 # Maintainer: Deian Stefan
+# Contributor: xiretza <>

 pkgdesc="A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions"
+makedepends=('git' 'cmake' 'lingeling' 'gtest')

 pkgver() {
-  cd $_pkgname
-  printf "r%s.%s" "$(git rev-list --count HEAD)" "$(git rev-parse --short HEAD)"
-prepare() {
-  cd $srcdir
+  cd "$_pkgname"
+  git describe --long --tags | sed 's/^v//;s/\([^-]*-g\)/r\1/;s/-/./g'

 build() {
+  cmake -B build -S "$_pkgname" \
+    -DTESTING=on
+  make -C build

-  cd "$srcdir/boolector"
-  # Download and build Lingeling
-  ./contrib/
-  CFLAGS="" ./ --shared
-  cd build
-  make
+check() {
+  make -C build test

 package() {
-  mkdir -p "$pkgdir/usr/bin/"
-  mkdir -p "$pkgdir/usr/lib/"
-  mkdir -p "$pkgdir/usr/include/boolector"
-  install -m755 boolector/build/bin/boolector "$pkgdir/usr/bin/"
-  install -m755 boolector/build/lib/*.so "$pkgdir/usr/lib/"
-  install -m644 boolector/src/*.h "$pkgdir/usr/include/boolector/"
+  make -C build DESTDIR="$pkgdir" install
+  install -Dm644 "$_pkgname/COPYING" "$pkgdir/usr/share/licenses/$pkgname/COPYING"
+# vim: set et ts=2:

xiretza commented on 2020-06-10 20:25

This should be provides=(boolector); conflicts=(boolector).

deian commented on 2019-06-13 22:30

Should be fixed now. Just added btor2tools as a dependency.

maximaximal commented on 2019-03-08 15:54

This package is currently not building, CMake doesn't find Btor2Tools. Could the installation scripts in the contrib/ of the boolector repository help solving this issue?


CMake Error at /usr/share/cmake-3.13/Modules/FindPackageHandleStandardArgs.cmake:137 (message):
  Could NOT find Btor2Tools (missing: Btor2Tools_INCLUDE_DIR)
Call Stack (most recent call first):
  /usr/share/cmake-3.13/Modules/FindPackageHandleStandardArgs.cmake:378 (_FPHSA_FAILURE_MESSAGE)
  cmake/FindBtor2Tools.cmake:10 (find_package_handle_standard_args)
  CMakeLists.txt:284 (find_package)