tjh.dev
1{
2 lib,
3 stdenv,
4 fetchFromGitHub,
5 cudd,
6 gmp-static,
7 gperf,
8 autoreconfHook,
9 libpoly,
10}:
11
12stdenv.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}