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;
|
||
|
|
};
|
||
|
|
}
|