pyrox.dev
lol
moni.tngl.sh
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
23let
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 };
63in
64
65buildDunePackage {
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}