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

Git Clone URL: https://aur.archlinux.org/boolector-git.git (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: https://github.com/Boolector/boolector
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
--- a/PKGBUILD
+++ b/PKGBUILD
@@ -1,49 +1,43 @@
 # Maintainer: Deian Stefan
+# Contributor: xiretza <xiretza+aur@xiretza.xyz>

 _pkgname=boolector
 pkgname=boolector-git
-pkgver=r10285.6fce0ac3
+pkgver=3.2.2.r8.g0783aa84
 pkgrel=1
 pkgdesc="A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions"
-arch=('any')
+arch=('x86_64')
 url="https://github.com/Boolector/boolector"
 license=('MIT')
 depends=('btor2tools-git')
-makedepends=()
-provides=(boolector)
-conflicts=(boolector)
+makedepends=('git' 'cmake' 'lingeling' 'gtest')
+checkdepends=('python')
+provides=("$_pkgname=$pkgver")
+conflicts=("$_pkgname")
 source=("git://github.com/Boolector/boolector.git")
 sha256sums=('SKIP')
 sha512sums=('SKIP')

 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" \
+    -DCMAKE_INSTALL_PREFIX="/usr" \
+    -DBUILD_SHARED_LIBS=on \
+    -DTESTING=on
+  make -C build
+}

-  cd "$srcdir/boolector"
-
-  # Download and build Lingeling
-  ./contrib/setup-lingeling.sh
-
-  CFLAGS="" ./configure.sh --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?

Error:

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)