pkgs/applications/science/logic/cvc3/default.nix

   1 { lib, stdenv, fetchurl, flex, bison, gmp, perl }:
   2
   3 stdenv.mkDerivation rec {
   4     pname = "cvc3";
   5     version = "2.4.1";
   6
   7     src = fetchurl {
   8       url = "https://cs.nyu.edu/acsys/cvc3/releases/${version}/${pname}-${version}.tar.gz";
   9       sha256 = "1xxcwhz3y6djrycw8sm6xz83wb4hb12rd1n0skvc7fng0rh1snym";
  10     };
  11
  12   buildInputs = [ gmp flex bison perl ];
  13
  14   patches = [ ./cvc3-2.4.1-gccv6-fix.patch ];
  15
  16   # fails to configure on darwin due to gmp not found
  17   configureFlags = [ "LIBS=-L${gmp}/lib" "CXXFLAGS=-I${gmp.dev}/include" ];
  18
  19   postPatch = ''
  20     sed -e "s@ /bin/bash@bash@g" -i Makefile.std
  21     find . -exec sed -e "s@/usr/bin/perl@${perl}/bin/perl@g" -i '{}' ';'
  22
  23     # bison 3.7 workaround
  24     for f in parsePL parseLisp parsesmtlib parsesmtlib2 ; do
  25       ln -s ../parser/''${f}_defs.h src/include/''${f}.hpp
  26     done
  27   '';
  28
  29   meta = with lib; {
  30     description = "Prover for satisfiability modulo theory (SMT)";
  31     mainProgram = "cvc3";
  32     maintainers = with maintainers;
  33       [ raskin ];
  34     platforms = platforms.unix;
  35     license = licenses.free;
  36     homepage = "https://cs.nyu.edu/acsys/cvc3/index.html";
  37   };
  38   passthru = {
  39     updateInfo = {
  40       downloadPage = "https://cs.nyu.edu/acsys/cvc3/download.html";
  41     };
  42   };
  43 }