tjh.dev
1{
2 lib,
3 mkCoqDerivation,
4 coq,
5 version ? null,
6}:
7
8mkCoqDerivation {
9 pname = "HoTT";
10 repo = "Coq-HoTT";
11 owner = "HoTT";
12 inherit version;
13 defaultVersion =
14 with lib.versions;
15 lib.switch coq.coq-version [
16 {
17 case = range "8.14" "9.0";
18 out = coq.coq-version;
19 }
20 ] null;
21 releaseRev = v: "V${v}";
22 release."8.14".sha256 = "sha256-7kXk2pmYsTNodHA+Qts3BoMsewvzmCbYvxw9Sgwyvq0=";
23 release."8.15".sha256 = "sha256-JfeiRZVnrjn3SQ87y6dj9DWNwCzrkK3HBogeZARUn9g=";
24 release."8.16".sha256 = "sha256-xcEbz4ZQ+U7mb0SEJopaczfoRc2GSgF2BGzUSWI0/HY=";
25 release."8.17".sha256 = "sha256-GjTUpzL9UzJm4C2ilCaYEufLG3hcj7rJPc5Op+OMal8=";
26 release."8.18".sha256 = "sha256-URoUoQOsG0432wg9i6pTRomWQZ+ewutq2+V29TBrVzc=";
27 release."8.19".sha256 = "sha256-igG3mhR6uPXV+SCtPH9PBw/eAtTFFry6HPT5ypWj3tQ=";
28 release."8.20".sha256 = "sha256-XHAvomi0of11j4x5gpTgD5Mw53eF1FpnCyBvdbV3g6I=";
29 release."9.0".sha256 = "sha256-etdLH1qDyDc+ZM7K/65iib0MRlLhsnVmzWBCULUDD50=";
30
31 # versions of HoTT for Coq 8.17 and onwards will use dune
32 # opam-name = if lib.versions.isLe "8.17" coq.coq-version then "coq-hott" else null;
33 opam-name = "coq-hott";
34 useDune = lib.versions.isGe "8.17" coq.coq-version;
35
36 patchPhase = ''
37 patchShebangs etc
38 '';
39
40 meta = {
41 homepage = "https://homotopytypetheory.org/";
42 description = "Homotopy Type Theory library";
43 longDescription = ''
44 Homotopy Type Theory is an interpretation of Martin-Löf’s intensional
45 type theory into abstract homotopy theory. Propositional equality is
46 interpreted as homotopy and type isomorphism as homotopy equivalence.
47 Logical constructions in type theory then correspond to
48 homotopy-invariant constructions on spaces, while theorems and even
49 proofs in the logical system inherit a homotopical meaning. As the
50 natural logic of homotopy, type theory is also related to higher
51 category theory as it is used e.g. in the notion of a higher topos.
52
53 The HoTT library is a development of homotopy-theoretic ideas in the Coq
54 proof assistant. It draws many ideas from Vladimir Voevodsky's
55 Foundations library (which has since been incorporated into the Unimath
56 library) and also cross-pollinates with the HoTT-Agda library.
57 '';
58 maintainers = with lib.maintainers; [
59 alizter
60 siddharthist
61 ];
62 };
63}