tjh.dev
nixpkgs mirror (for testing)
github.com/NixOS/nixpkgs
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
22let
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 };
62in
63
64buildDunePackage {
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}