Files
nixpkgs/pkgs/by-name/cv/cvc4/package.nix
Dark Steveneq 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
push sheeet
2025-10-09 14:15:47 +02:00

95 lines
1.9 KiB
Nix

{
lib,
stdenv,
fetchFromGitHub,
cmake,
cln,
gmp,
git,
swig,
pkg-config,
readline,
libantlr3c,
boost,
jdk,
python3,
antlr3_4,
}:
stdenv.mkDerivation rec {
pname = "cvc4";
version = "1.8";
src = fetchFromGitHub {
owner = "cvc4";
repo = "cvc4";
rev = version;
sha256 = "1rhs4pvzaa1wk00czrczp58b2cxfghpsnq534m0l3snnya2958jp";
};
nativeBuildInputs = [
pkg-config
cmake
];
buildInputs = [
gmp
git
python3.pkgs.toml
readline
swig
libantlr3c
antlr3_4
boost
jdk
python3
]
++ lib.optionals (!stdenv.hostPlatform.isDarwin) [ cln ];
configureFlags = [
"--enable-language-bindings=c,c++,java"
"--enable-gpl"
"--with-readline"
"--with-boost=${boost.dev}"
]
++ lib.optionals (!stdenv.hostPlatform.isDarwin) [ "--with-cln" ];
prePatch = ''
patch -p1 -i ${./minisat-fenv.patch} -d src/prop/minisat
patch -p1 -i ${./minisat-fenv.patch} -d src/prop/bvminisat
'';
patches = [
./cvc4-bash-patsub-replacement.patch
];
postPatch = ''
# Fix missing size_t declarations by adding after pragma once or include guards
sed -i '/#pragma once/a\
#include <cstddef>' src/expr/emptyset.h || sed -i '1i\
#include <cstddef>' src/expr/emptyset.h
sed -i '/#define CVC4__EXPR__EXPR_IOMANIP_H/a\
#include <cstddef>' src/expr/expr_iomanip.h
sed -i '/#define CVC4__UTIL__REGEXP_H/a\
#include <cstddef>' src/util/regexp.h
'';
preConfigure = ''
patchShebangs ./src/
'';
cmakeBuildType = "Production";
meta = with lib; {
description = "High-performance theorem prover and SMT solver";
mainProgram = "cvc4";
homepage = "http://cvc4.cs.stanford.edu/web/";
license = licenses.gpl3;
platforms = platforms.unix;
maintainers = with maintainers; [
vbgl
thoughtpolice
];
};
}