@@ -0,0 +1,47 @@
1+{ lib
2+, fetchFromGitHub
3+, buildDunePackage
4+, cmdliner
5+, menhir
6+, menhirLib
7+, ppx_deriving
8+, ppxlib
9+, uuseg
10+, uutf
11+}:
12+
13+buildDunePackage {
14+ pname = "cooltt";
15+ version = "unstable-2021-05-25";
16+
17+ minimumOCamlVersion = "4.10";
18+
19+ useDune2 = true;
20+
21+ src = fetchFromGitHub {
22+ owner = "RedPRL";
23+ repo = "cooltt";
24+ rev = "8ac06cbf7e05417d777f3ac6a471fe3576249f79";
25+ sha256 = "sha256-JBLNJaRuP/gwlg8RS3cpOpzxChOVKfmFulf5HKhhHh4=";
26+ };
27+
28+ nativeBuildInputs = [
29+ cmdliner
30+ menhir
31+ ppxlib
32+ ];
33+
34+ propagatedBuildInputs = [
35+ menhirLib
36+ ppx_deriving
37+ uuseg
38+ uutf
39+ ];
40+
41+ meta = with lib; {
42+ homepage = "https://github.com/RedPRL/cooltt";
43+ description = "A cool implementation of normalization by evaluation (nbe) & elaboration for Cartesian cubical type theory";
44+ license = licenses.asl20;
45+ maintainers = with maintainers; [ fortuneteller2k ];
46+ };
47+}