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

   1 {
   2   lib,
   3   stdenv,
   4   fetchFromGitHub,
   5   cudd,
   6   gmp-static,
   7   gperf,
   8   autoreconfHook,
   9   libpoly,
  10 }:
  11
  12 stdenv.mkDerivation rec {
  13   pname = "yices";
  14   version = "2.6.5";
  15
  16   src = fetchFromGitHub {
  17     owner = "SRI-CSL";
  18     repo = "yices2";
  19     rev = "Yices-${version}";
  20     hash = "sha256-/sKyHkFW5I5kojNIRPEKojzTvfRZiyVIN5VlBIbAV7k=";
  21   };
  22
  23   postPatch = "patchShebangs tests/regress/check.sh";
  24
  25   nativeBuildInputs = [ autoreconfHook ];
  26   buildInputs = [
  27     cudd
  28     gmp-static
  29     gperf
  30     libpoly
  31   ];
  32   configureFlags = [
  33     "--with-static-gmp=${gmp-static.out}/lib/libgmp.a"
  34     "--with-static-gmp-include-dir=${gmp-static.dev}/include"
  35     "--enable-mcsat"
  36   ];
  37
  38   enableParallelBuilding = true;
  39   doCheck = true;
  40
  41   meta = with lib; {
  42     description = "High-performance theorem prover and SMT solver";
  43     homepage = "https://yices.csl.sri.com";
  44     license = licenses.gpl3;
  45     platforms = with platforms; linux ++ darwin;
  46     maintainers = with maintainers; [ thoughtpolice ];
  47   };
  48 }