pkgs/development/ocaml-modules/cooltt/default.nix

   1 { lib
   2 , fetchFromGitHub
   3 , buildDunePackage
   4 , bos
   5 , bwd
   6 , cmdliner
   7 , containers
   8 , ezjsonm
   9 , findlib
  10 , menhir
  11 , menhirLib
  12 , ppx_deriving
  13 , ppxlib
  14 , uuseg
  15 , uutf
  16 , yuujinchou
  17 , ounit2
  18 , qcheck
  19 , qcheck-core
  20 }:
  21
  22 let
  23   bantorra = buildDunePackage rec {
  24     pname = "bantorra";
  25     version = "unstable-2022-05-08";
  26     src = fetchFromGitHub {
  27       owner = "RedPRL";
  28       repo = "bantorra";
  29       rev = "d05c34295727dd06d0ac4416dc2e258732e8593d";
  30       hash = "sha256-s6lUTs3VRl6YhLAn3PO4aniANhFp8ytoTsFAgcOlee4=";
  31     };
  32
  33     propagatedBuildInputs = [ bos ezjsonm findlib ];
  34
  35     meta = {
  36       description = "Extensible Library Management and Path Resolution";
  37       homepage = "https://github.com/RedPRL/bantorra";
  38       license = lib.licenses.asl20;
  39     };
  40   };
  41   kado = buildDunePackage rec {
  42     pname = "kado";
  43     version = "unstable-2023-10-03";
  44     src = fetchFromGitHub {
  45       owner = "RedPRL";
  46       repo = "kado";
  47       rev = "6b2e9ba2095e294e6e0fc6febc280d80c5799c2b";
  48       hash = "sha256-fP6Ade3mJeyOMjuDIvrW88m6E3jfb2z3L8ufgloz4Tc=";
  49     };
  50
  51     propagatedBuildInputs = [ bwd ];
  52
  53     doCheck = true;
  54     checkInputs = [ qcheck-core ];
  55
  56     meta = {
  57       description = "Cofibrations in Cartecian Cubical Type Theory";
  58       homepage = "https://github.com/RedPRL/kado";
  59       license = lib.licenses.asl20;
  60     };
  61   };
  62 in
  63
  64 buildDunePackage {
  65   pname = "cooltt";
  66   version = "unstable-2023-10-03";
  67
  68   minimalOCamlVersion = "5.0";
  69
  70   src = fetchFromGitHub {
  71     owner = "RedPRL";
  72     repo = "cooltt";
  73     rev = "a5eaf4db195b5166a7102d47d42724f59cf3de19";
  74     hash = "sha256-48bEf59rtPRrCRjab7+GxppjfR2c87HjQ+uKY2Bag0I=";
  75   };
  76
  77   nativeBuildInputs = [
  78     menhir
  79   ];
  80
  81   buildInputs = [
  82     cmdliner
  83     ppxlib
  84   ];
  85
  86   propagatedBuildInputs = [
  87     bantorra
  88     bwd
  89     ezjsonm
  90     kado
  91     menhirLib
  92     ppx_deriving
  93     uuseg
  94     uutf
  95     yuujinchou
  96     containers
  97   ];
  98
  99   checkInputs = [
 100     ounit2
 101     qcheck
 102   ];
 103
 104   meta = with lib; {
 105     homepage = "https://github.com/RedPRL/cooltt";
 106     description = "Cool implementation of normalization by evaluation (nbe) & elaboration for Cartesian cubical type theory";
 107     license = licenses.asl20;
 108     maintainers = with maintainers; [ moni ];
 109   };
 110 }