646b892680
Some checks failed
Periodic Merges (6h) / master → staging-nixos (push) Failing after 12m50s
Periodic Merges (6h) / master → staging-next (push) Failing after 12m54s
Periodic Merges (24h) / merge-base(master,staging) → haskell-updates (push) Failing after 11m54s
Periodic Merges (6h) / staging-next → staging (push) Failing after 12m13s
Periodic Merges (24h) / staging-next-25.05 → staging-25.05 (push) Failing after 13m24s
Periodic Merges (24h) / release-25.05 → staging-next-25.05 (push) Failing after 14m28s
62 lines
1.3 KiB
Nix
62 lines
1.3 KiB
Nix
{
|
|
lib,
|
|
stdenv,
|
|
fetchFromGitHub,
|
|
cudd,
|
|
gmp,
|
|
gperf,
|
|
autoreconfHook,
|
|
libpoly,
|
|
ncurses5,
|
|
}:
|
|
|
|
let
|
|
gmp-static = gmp.override { withStatic = true; };
|
|
in
|
|
stdenv.mkDerivation (finalAttrs: {
|
|
pname = "yices";
|
|
version = "2.7.0";
|
|
|
|
src = fetchFromGitHub {
|
|
owner = "SRI-CSL";
|
|
repo = "yices2";
|
|
tag = "yices-${finalAttrs.version}";
|
|
hash = "sha256-siyepgxqKWRyO4+SB95lmhJ98iDubk0R0ErEJdSsM8o=";
|
|
};
|
|
|
|
postPatch = ''
|
|
patchShebangs tests/regress/check.sh
|
|
''
|
|
# operation not permitted
|
|
+ lib.optionalString stdenv.hostPlatform.isDarwin ''
|
|
substituteInPlace utils/make_source_version \
|
|
--replace-fail '"/usr/bin/mktemp -t out"' "mktemp"
|
|
'';
|
|
|
|
nativeBuildInputs = [ autoreconfHook ];
|
|
buildInputs = [
|
|
cudd
|
|
gmp-static
|
|
gperf
|
|
libpoly
|
|
];
|
|
configureFlags = [
|
|
"--with-static-gmp=${gmp-static.out}/lib/libgmp.a"
|
|
"--with-static-gmp-include-dir=${gmp-static.dev}/include"
|
|
"--enable-mcsat"
|
|
];
|
|
|
|
enableParallelBuilding = true;
|
|
doCheck = true;
|
|
|
|
nativeCheckInputs = [ ncurses5 ];
|
|
|
|
meta = {
|
|
description = "High-performance theorem prover and SMT solver";
|
|
homepage = "https://yices.csl.sri.com";
|
|
license = lib.licenses.gpl3Plus;
|
|
platforms = lib.platforms.linux ++ lib.platforms.darwin;
|
|
maintainers = with lib.maintainers; [ thoughtpolice ];
|
|
};
|
|
})
|