Commit 463643af authored by Ali Caglayan's avatar Ali Caglayan Committed by Vincent Laporte
Browse files

coqPackages.HoTT: 8.16 -> 8.17 



We bump the HoTT library to 8.17 and switch to using Dune for the
build.

I attempted to include the 8.10 - 8.13 builds but I couldn't get
autoconf to work the way I wanted so I gave up in the end.

Signed-off-by: default avatarAli Caglayan <alizter@gmail.com>
parent 9e109435

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

+27 −6
Original line number Diff line number Diff line 
{ lib, mkCoqDerivation, autoconf, automake, coq, version ? null }:

{ lib, mkCoqDerivation, coq, version ? null }:



mkCoqDerivation {

  pname = "HoTT";
@@ -6,12 +6,18 @@ mkCoqDerivation { 
  owner = "HoTT";

  inherit version;

  defaultVersion = with lib.versions; lib.switch coq.coq-version [

    { case = range "8.14" "8.16"; out = coq.coq-version; }

    { case = range "8.14" "8.17"; out = coq.coq-version; }

  ] null;

  releaseRev = v: "V${v}";

  release."8.16".sha256 = "sha256-xcEbz4ZQ+U7mb0SEJopaczfoRc2GSgF2BGzUSWI0/HY=";

  release."8.15".sha256 = "sha256-JfeiRZVnrjn3SQ87y6dj9DWNwCzrkK3HBogeZARUn9g=";

  release."8.14".sha256 = "sha256-7kXk2pmYsTNodHA+Qts3BoMsewvzmCbYvxw9Sgwyvq0=";

  release."8.15".sha256 = "sha256-JfeiRZVnrjn3SQ87y6dj9DWNwCzrkK3HBogeZARUn9g=";

  release."8.16".sha256 = "sha256-xcEbz4ZQ+U7mb0SEJopaczfoRc2GSgF2BGzUSWI0/HY=";

  release."8.17".sha256 = "sha256-GjTUpzL9UzJm4C2ilCaYEufLG3hcj7rJPc5Op+OMal8=";



  # versions of HoTT for Coq 8.17 and onwards will use dune

  # opam-name = if lib.versions.isLe "8.17" coq.coq-version then "coq-hott" else null;

  opam-name = "coq-hott";

  useDune = lib.versions.isGe "8.17" coq.coq-version;

  

  patchPhase = ''

    patchShebangs etc
@@ -19,7 +25,22 @@ mkCoqDerivation { 


  meta = {

    homepage = "https://homotopytypetheory.org/";

    description = "Homotopy type theory";

    maintainers = with lib.maintainers; [ siddharthist ];

    description = "The Homotopy Type Theory library";

    longDescription = ''

      Homotopy Type Theory is an interpretation of Martin-Löf’s intensional

      type theory into abstract homotopy theory. Propositional equality is

      interpreted as homotopy and type isomorphism as homotopy equivalence.

      Logical constructions in type theory then correspond to

      homotopy-invariant constructions on spaces, while theorems and even

      proofs in the logical system inherit a homotopical meaning. As the

      natural logic of homotopy, type theory is also related to higher

      category theory as it is used e.g. in the notion of a higher topos.



      The HoTT library is a development of homotopy-theoretic ideas in the Coq

      proof assistant. It draws many ideas from Vladimir Voevodsky's

      Foundations library (which has since been incorporated into the Unimath

      library) and also cross-pollinates with the HoTT-Agda library.

    '';

    maintainers = with lib.maintainers; [ alizter siddharthist ];

  };

}