tjh.dev
nixpkgs mirror (for testing)
github.com/NixOS/nixpkgs
nix
1{
2 lib,
3 stdenv,
4 fetchFromGitLab,
5 ocamlPackages,
6 eprover,
7 z3,
8 zlib,
9}:
10
11stdenv.mkDerivation {
12 pname = "iprover";
13 version = "3.9.2";
14
15 src = fetchFromGitLab {
16 owner = "korovin";
17 repo = "iprover";
18 rev = "v3.9.2";
19 hash = "sha256-CbqPtP2pKLFgo67EF0IhvIdv1dAog2vb3Es0asmmSyY=";
20 };
21
22 postPatch = ''
23 substituteInPlace configure --replace Linux Debian
24 '';
25
26 strictDeps = true;
27
28 nativeBuildInputs = [
29 eprover
30 ]
31 ++ (with ocamlPackages; [
32 ocaml
33 findlib
34 ]);
35 buildInputs = [
36 zlib
37 ocamlPackages.z3
38 z3
39 ]
40 ++ (with ocamlPackages; [
41 ocamlgraph
42 yojson
43 zarith
44 ]);
45
46 preConfigure = "patchShebangs .";
47
48 env = {
49 NIX_CFLAGS_COMPILE = "-std=gnu17";
50 };
51
52 installPhase = ''
53 runHook preInstall
54 mkdir -p "$out/bin"
55 cp iproveropt "$out/bin"
56
57 echo -e "#! ${stdenv.shell}\\n$out/bin/iproveropt --clausifier \"${eprover}/bin/eprover\" --clausifier_options \" --tstp-format --silent --cnf \" \"\$@\"" > "$out"/bin/iprover
58 chmod a+x "$out"/bin/iprover
59 runHook postInstall
60 '';
61
62 meta = {
63 description = "Automated first-order logic theorem prover";
64 homepage = "http://www.cs.man.ac.uk/~korovink/iprover/";
65 maintainers = with lib.maintainers; [
66 raskin
67 ];
68 platforms = lib.platforms.linux;
69 license = lib.licenses.gpl3;
70 };
71}