{ 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 = "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;
  };
}