pkgs/development/coq-modules/smtcoq/cvc4.nix

   1 { lib, stdenv, cln, fetchurl, gmp, gnumake42, swig, pkg-config
   2 , libantlr3c, boost, autoreconfHook
   3 , python3
   4 }:
   5
   6 stdenv.mkDerivation rec {
   7   pname = "cvc4";
   8   version = "1.6";
   9
  10   src = fetchurl {
  11     url = "https://cvc4.cs.stanford.edu/downloads/builds/src/cvc4-${version}.tar.gz";
  12     sha256 = "1iw793zsi48q91lxpf8xl8lnvv0jsj4whdad79rakywkm1gbs62w";
  13   };
  14
  15   # Build fails with GNUmake 4.4
  16   nativeBuildInputs = [ autoreconfHook gnumake42 pkg-config ];
  17   buildInputs = [ gmp swig libantlr3c boost python3 ]
  18     ++ lib.optionals stdenv.isLinux [ cln ];
  19
  20   configureFlags = [
  21     "--enable-language-bindings=c"
  22     "--enable-gpl"
  23     "--with-boost=${boost.dev}"
  24   ] ++ lib.optionals stdenv.isLinux [ "--with-cln" ];
  25
  26   prePatch = ''
  27     patch -p1 -i ${./minisat-fenv.patch} -d src/prop/minisat
  28     patch -p1 -i ${./minisat-fenv.patch} -d src/prop/bvminisat
  29   '';
  30
  31   patches = [
  32     ../../../applications/science/logic/cvc4/cvc4-bash-patsub-replacement.patch
  33   ];
  34
  35   preConfigure = ''
  36     patchShebangs ./src/
  37   '';
  38
  39   enableParallelBuilding = true;
  40
  41   meta = with lib; {
  42     description = "A high-performance theorem prover and SMT solver";
  43     homepage    = "http://cvc4.cs.stanford.edu/web/";
  44     license     = licenses.gpl3;
  45     platforms   = platforms.unix;
  46     maintainers = with maintainers; [ vbgl thoughtpolice gebner ];
  47   };
  48 }