Unverified Commit b62a94ca authored by Théo Zimmermann's avatar Théo Zimmermann Committed by GitHub
Browse files

Rocq platform 9.0 update (#485359)

parents 13b356cf 9079f5a1

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

+4 −1
Original line number Diff line number Diff line
@@ -2,6 +2,7 @@ 
  lib,

  mkCoqDerivation,

  coq,

  stdlib,

  version ? null,

}:
@@ -9,13 +10,15 @@ mkCoqDerivation { 
  pname = "LibHyps";

  owner = "Matafou";

  inherit version;

  defaultVersion = if (lib.versions.range "8.11" "8.20") coq.version then "2.0.8" else null;

  defaultVersion = if (lib.versions.range "8.11" "9.0") coq.version then "2.0.8" else null;

  release = {

    "2.0.8".sha256 = "sha256-u8T7ZWfgYNFBsIPss0uUS0oBvdlwPp3t5yYIMjYzfLc=";

  };



  configureScript = "./configure.sh";



  propagatedBuildInputs = [ stdlib ];



  releaseRev = (v: "libhyps-${v}");



  meta = {

pkgs/development/coq-modules/aac-tactics/default.nix

+5 −0
Original line number Diff line number Diff line
@@ -11,6 +11,7 @@ mkCoqDerivation { 


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



  release."9.0.0".sha256 = "sha256-mln1182EOeXZCa1NzjAiovK93Xm+5JMZpGqJVrM67Jo=";

  release."8.20.0".sha256 = "sha256-VQzeINIZAfP3Qyh29uPqcNVlNJfIzzRLtN0Cm4EuGCk=";

  release."8.19.1".sha256 = "sha256-W/V57h+rjb3m0ktCG83PquMHfXiv6H1Nhvw9sVEPLqM=";

  release."8.19.0".sha256 = "sha256-IeCBd8gcu4bAXH5I/XIT7neQIILi+EWR6qqAA4GzQD0=";
@@ -34,6 +35,10 @@ mkCoqDerivation { 
  defaultVersion =



    lib.switch coq.coq-version [

      {

        case = "9.0";

        out = "9.0.0";

      }

      {

        case = "8.20";

        out = "8.20.0";

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

+8 −2
Original line number Diff line number Diff line
@@ -2,6 +2,7 @@ 
  lib,

  mkCoqDerivation,

  coq,

  stdlib,

  unicoq,

  version ? null,

}:
@@ -14,14 +15,19 @@ mkCoqDerivation { 
    with lib.versions;

    lib.switch coq.version [

      {

        case = range "8.19" "8.19";

        case = range "8.19" "9.0";

        out = "1.4-coq${coq.coq-version}";

      }

    ] null;

  release."1.4-coq9.0".sha256 = "sha256-pAPBRCW7M46UZPJ+v/0xAT8mpQURN8czMmlrfYz/MVU=";

  release."1.4-coq8.20".sha256 = "sha256-3nu/8zDvdnl6WzGtw46mVcdqgkRgc6Xy8/I+lUOrSIY=";

  release."1.4-coq8.19".sha256 = "sha256-G9eK0eLyECdT20/yf8yyz7M8Xq2WnHHaHpxVGP0yTtU=";

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

  mlPlugin = true;

  propagatedBuildInputs = [ unicoq ];

  propagatedBuildInputs = [

    stdlib

    unicoq

  ];

  meta = {

    description = "Typed tactic language for Coq";

    license = lib.licenses.mit;

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

+2 −1
Original line number Diff line number Diff line
@@ -12,7 +12,7 @@ mkCoqDerivation { 
    with lib.versions;

    lib.switch coq.version [

      {

        case = range "8.10" "8.20";

        case = range "8.10" "9.0";

        out = "1.1.3+coq${coq.coq-version}";

      }

      {
@@ -23,6 +23,7 @@ mkCoqDerivation { 
  displayVersion = {

    paramcoq = "...";

  };

  release."1.1.3+coq9.0".sha256 = "sha256-zibQ9nBadSElpyI8iMTDRW/mqtxmxClaVb24o5W6ajE=";

  release."1.1.3+coq8.20".sha256 = "sha256-34xDOz/2xO39fnQW6Zb9CI2EKFuJZjrAdOpMEmwuzY0=";

  release."1.1.3+coq8.19".sha256 = "sha256-5NVsdLXaoz6qrr5ra5YfoHeuK4pEf8JX/X9+SZA0U+U=";

  release."1.1.3+coq8.18".sha256 = "sha256-hNBaj9hB+OzwXsOX+TOXtDLjA5oP4EmEgseLwxFxW+I=";

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

+3 −3
Original line number Diff line number Diff line
@@ -16,12 +16,12 @@ mkCoqDerivation { 
    in

    lib.switch coq.coq-version [

      {

        case = range "8.17" "8.19";

        out = "0.0.11";

        case = range "8.17" "9.0";

        out = "0.0.15";

      }

    ] null;

  release = {

    "0.0.11".sha256 = "sha256-aYoO08nwItlOoE5BnKRGib2Zk4Fz4Ni/L4QaqkObPow=";

    "0.0.15".sha256 = "sha256-zxNIMppFXUKShOXLbdZphy0Je5ii6cjcWUUcQMTcaHk=";

  };

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