blob: 77e5919c0eee151196d66ea52e017364c90d9cab (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
|
{ lib, stdenv, fetchFromGitLab, ocamlPackages, eprover, z3, zlib }:
stdenv.mkDerivation rec {
pname = "iprover";
version = "3.8.1";
src = fetchFromGitLab {
owner = "korovin";
repo = pname;
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 = "An automated first-order logic theorem prover";
homepage = "http://www.cs.man.ac.uk/~korovink/iprover/";
maintainers = with maintainers; [ raskin gebner ];
platforms = platforms.linux;
license = licenses.gpl3;
};
}
|