pkgs/development/coq-modules/HoTT/default.nix

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