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
68 lines
1.3 KiB
Nix
68 lines
1.3 KiB
Nix
{
|
|
lib,
|
|
stdenv,
|
|
fetchFromGitLab,
|
|
ocamlPackages,
|
|
eprover,
|
|
z3,
|
|
zlib,
|
|
}:
|
|
|
|
stdenv.mkDerivation {
|
|
pname = "iprover";
|
|
version = "3.8.1";
|
|
|
|
src = fetchFromGitLab {
|
|
owner = "korovin";
|
|
repo = "iprover";
|
|
rev = "f61edb113b705606c7314dc4dce0687832c3169f";
|
|
hash = "sha256-XXqbEoYKjoktE3ZBEIEFjLhA1B75zhnfPszhe8SvbI8=";
|
|
};
|
|
|
|
postPatch = ''
|
|
substituteInPlace configure --replace Linux Debian
|
|
'';
|
|
|
|
strictDeps = true;
|
|
|
|
nativeBuildInputs = [
|
|
eprover
|
|
]
|
|
++ (with ocamlPackages; [
|
|
ocaml
|
|
findlib
|
|
]);
|
|
buildInputs = [
|
|
zlib
|
|
ocamlPackages.z3
|
|
z3
|
|
]
|
|
++ (with ocamlPackages; [
|
|
ocamlgraph
|
|
yojson
|
|
zarith
|
|
]);
|
|
|
|
preConfigure = "patchShebangs .";
|
|
|
|
installPhase = ''
|
|
runHook preInstall
|
|
mkdir -p "$out/bin"
|
|
cp iproveropt "$out/bin"
|
|
|
|
echo -e "#! ${stdenv.shell}\\n$out/bin/iproveropt --clausifier \"${eprover}/bin/eprover\" --clausifier_options \" --tstp-format --silent --cnf \" \"\$@\"" > "$out"/bin/iprover
|
|
chmod a+x "$out"/bin/iprover
|
|
runHook postInstall
|
|
'';
|
|
|
|
meta = with lib; {
|
|
description = "Automated first-order logic theorem prover";
|
|
homepage = "http://www.cs.man.ac.uk/~korovink/iprover/";
|
|
maintainers = with maintainers; [
|
|
raskin
|
|
];
|
|
platforms = platforms.linux;
|
|
license = licenses.gpl3;
|
|
};
|
|
}
|