{ provers ? []
, devDeps ? []
, testDeps ? false
}:

let
  version = "git";
  src = ./.;
in

with import <nixpkgs> {};

let inherit (lib) optionals; in

let runtest = optionals testDeps (python3Packages.buildPythonApplication rec {
  pname = "easycrypt-runtest";
  inherit src version;

  dontConfigure = true;
  dontBuild = true;
  doCheck = false;

  pythonPath = with python3Packages; [ pyyaml ];

  installPhase = ''
    runHook preInstall
    mkdir -p $out/bin
    cp scripts/testing/runtest $out/bin/ec-runtest
    runHook postInstall
  '';
}); in

stdenv.mkDerivation {
  pname = "easycrypt";
  inherit version src;

  buildInputs = [ git ] ++ (with ocamlPackages; [
    ocaml findlib dune_2
    batteries inifiles dune-build-info menhir menhirLib yojson zarith
  ]);
  propagatedBuildInputs = [ why3 runtest ]
    ++ devDeps
    ++ provers;

  installPhase = ''
    runHook preInstall
    dune install --prefix $out -p $pname
    rm $out/bin/ec-runtest
    runHook postInstall
  '';

  passthru = {
    inherit runtest;
  };
}