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.19"; 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   release."8.19".sha256 = "sha256-igG3mhR6uPXV+SCtPH9PBw/eAtTFFry6HPT5ypWj3tQ=";
  18
  19   # versions of HoTT for Coq 8.17 and onwards will use dune
  20   # opam-name = if lib.versions.isLe "8.17" coq.coq-version then "coq-hott" else null;
  21   opam-name = "coq-hott";
  22   useDune = lib.versions.isGe "8.17" coq.coq-version;
  23
  24   patchPhase = ''
  25     patchShebangs etc
  26   '';
  27
  28   meta = {
  29     homepage = "https://homotopytypetheory.org/";
  30     description = "The Homotopy Type Theory library";
  31     longDescription = ''
  32       Homotopy Type Theory is an interpretation of Martin-Löf’s intensional
  33       type theory into abstract homotopy theory. Propositional equality is
  34       interpreted as homotopy and type isomorphism as homotopy equivalence.
  35       Logical constructions in type theory then correspond to
  36       homotopy-invariant constructions on spaces, while theorems and even
  37       proofs in the logical system inherit a homotopical meaning. As the
  38       natural logic of homotopy, type theory is also related to higher
  39       category theory as it is used e.g. in the notion of a higher topos.
  40
  41       The HoTT library is a development of homotopy-theoretic ideas in the Coq
  42       proof assistant. It draws many ideas from Vladimir Voevodsky's
  43       Foundations library (which has since been incorporated into the Unimath
  44       library) and also cross-pollinates with the HoTT-Agda library.
  45     '';
  46     maintainers = with lib.maintainers; [ alizter siddharthist ];
  47   };
  48 }