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

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