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