depot/third_party/nixpkgs/pkgs/development/ocaml-modules/cooltt/default.nix

{
  lib,
  fetchFromGitHub,
  buildDunePackage,
  bos,
  bwd,
  cmdliner,
  containers,
  ezjsonm,
  findlib,
  menhir,
  menhirLib,
  ppx_deriving,
  ppxlib,
  uuseg,
  uutf,
  yuujinchou,
  ounit2,
  qcheck,
  qcheck-core,
}:

let
  bantorra = buildDunePackage rec {
    pname = "bantorra";
    version = "unstable-2022-05-08";
    src = fetchFromGitHub {
      owner = "RedPRL";
      repo = "bantorra";
      rev = "d05c34295727dd06d0ac4416dc2e258732e8593d";
      hash = "sha256-s6lUTs3VRl6YhLAn3PO4aniANhFp8ytoTsFAgcOlee4=";
    };

    propagatedBuildInputs = [
      bos
      ezjsonm
      findlib
    ];

    meta = {
      description = "Extensible Library Management and Path Resolution";
      homepage = "https://github.com/RedPRL/bantorra";
      license = lib.licenses.asl20;
    };
  };
  kado = buildDunePackage rec {
    pname = "kado";
    version = "unstable-2023-10-03";
    src = fetchFromGitHub {
      owner = "RedPRL";
      repo = "kado";
      rev = "6b2e9ba2095e294e6e0fc6febc280d80c5799c2b";
      hash = "sha256-fP6Ade3mJeyOMjuDIvrW88m6E3jfb2z3L8ufgloz4Tc=";
    };

    propagatedBuildInputs = [ bwd ];

    doCheck = true;
    checkInputs = [ qcheck-core ];

    meta = {
      description = "Cofibrations in Cartecian Cubical Type Theory";
      homepage = "https://github.com/RedPRL/kado";
      license = lib.licenses.asl20;
    };
  };
in

buildDunePackage {
  pname = "cooltt";
  version = "unstable-2023-10-03";

  minimalOCamlVersion = "5.0";

  src = fetchFromGitHub {
    owner = "RedPRL";
    repo = "cooltt";
    rev = "a5eaf4db195b5166a7102d47d42724f59cf3de19";
    hash = "sha256-48bEf59rtPRrCRjab7+GxppjfR2c87HjQ+uKY2Bag0I=";
  };

  nativeBuildInputs = [
    menhir
  ];

  buildInputs = [
    cmdliner
    ppxlib
  ];

  propagatedBuildInputs = [
    bantorra
    bwd
    ezjsonm
    kado
    menhirLib
    ppx_deriving
    uuseg
    uutf
    yuujinchou
    containers
  ];

  checkInputs = [
    ounit2
    qcheck
  ];

  meta = with lib; {
    homepage = "https://github.com/RedPRL/cooltt";
    description = "Cool implementation of normalization by evaluation (nbe) & elaboration for Cartesian cubical type theory";
    license = licenses.asl20;
    maintainers = with maintainers; [ moni ];
  };
}