coq_8_13: init at 8.13+β1

5 files changed, 16 insertions, 2 deletions

diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix
index dc9e40912d5..5c16f7defa8 100644
--- a/pkgs/applications/science/logic/coq/default.nix
+++ b/pkgs/applications/science/logic/coq/default.nix
@@ -36,6 +36,7 @@ let
    "8.11.2" = "0f77ccyxdgbf1nrj5fa8qvrk1cyfy06fv8gj9kzfvlcgn0cf48sa";
    "8.12.0" = "18dc7k0piv6v064zgdadpw6mkkxk7j663hb3svgj5236fihjr0cz";
    "8.12.1" = "1rkcyjjrzcqw9xk93hsq0vvji4f8r5iq0f739mghk60bghkpnb7q";
+   "8.13+beta1" = "1v4a6dpj41flspa4ihcr7m5ahqz10kbn62fmrldmv7gzq6jsyfyq";
   }.${version};
   coq-version = stdenv.lib.versions.majorMinor version;
   versionAtLeast = stdenv.lib.versionAtLeast coq-version;
@@ -118,7 +119,9 @@ self = stdenv.mkDerivation {
      then [ ocamlPackages.lablgtk3-sourceview3 glib gnome3.defaultIconTheme wrapGAppsHook ]
      else [ ocamlPackages.lablgtk ]);
 
-  propagatedBuildInputs = stdenv.lib.optional (versionAtLeast "8.12") ocamlPackages.num;
+  propagatedBuildInputs =
+     stdenv.lib.optional (versionAtLeast "8.13") ocamlPackages.zarith
+  ++ stdenv.lib.optional (coq-version == "8.12") ocamlPackages.num;
 
   postPatch = ''
     UNAME=$(type -tp uname)
diff --git a/pkgs/development/coq-modules/bignums/default.nix b/pkgs/development/coq-modules/bignums/default.nix
index 7246382c9ae..f0434c4ae47 100644
--- a/pkgs/development/coq-modules/bignums/default.nix
+++ b/pkgs/development/coq-modules/bignums/default.nix
@@ -29,6 +29,10 @@ let params = {
         rev = "V8.12.0";
         sha256 = "14ijb3qy2hin3g4djx437jmnswxxq7lkfh3dwh9qvrds9a015yg8";
       };
+      "8.13" = {
+        rev = "V8.13.0";
+        sha256 = "1n66i7hd9222b2ks606mak7m4f0dgy02xgygjskmmav6h7g2sx7y";
+      };
     };
     param = params.${coq.coq-version};
 in
diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix
index 8cf502a1943..542fac861c5 100644
--- a/pkgs/development/coq-modules/mathcomp/default.nix
+++ b/pkgs/development/coq-modules/mathcomp/default.nix
@@ -66,6 +66,7 @@ let
   #######################################################################
     # sha256 of released mathcomp versions
     sha256 = {
+      "1.12.0"       = "1ccfny1vwgmdl91kz5xlmhq4wz078xm4z5wpd0jy5rn890dx03wp";
       "1.11.0"       = "06a71d196wd5k4wg7khwqb7j7ifr7garhwkd54s86i0j7d6nhl3c";
       "1.11+beta1"   = "12i3zznwajlihzpqsiqniv20rklj8d8401lhd241xy4s21fxkkjm";
       "1.10.0"       = "1b9m6pwxxyivw7rgx82gn5kmgv2mfv3h3y0mmjcjfypi8ydkrlbv";
@@ -76,6 +77,7 @@ let
     };
     # versions of coq compatible with released mathcomp versions
     coq-versions     = {
+      "1.12.0"       = flip elem [ "8.13" ];
       "1.11.0"       = flip elem [ "8.7" "8.8" "8.9" "8.10" "8.11" "8.12" ];
       "1.11+beta1"   = flip elem [ "8.7" "8.8" "8.9" "8.10" "8.11" "8.12" ];
       "1.10.0"       = flip elem [ "8.7" "8.8" "8.9" "8.10" "8.11" ];
@@ -96,7 +98,7 @@ let
     # mathcomp preferred versions by decreasing order
     # (the first version in the list will be tried first)
     version-preferences =
-      [ "1.10.0" "1.11.0" "1.9.0" "1.8.0" "1.7.0" "1.6.1" ];
+      [ "1.12.0" "1.10.0" "1.11.0" "1.9.0" "1.8.0" "1.7.0" "1.6.1" ];
 
     # list of core mathcomp packages sorted by dependency order
     packages = _version: # unused in current versions of mathcomp
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index eb8ba06ac00..5b049b1e1dd 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -26997,6 +26997,7 @@ in
     coqPackages_8_10 coq_8_10
     coqPackages_8_11 coq_8_11
     coqPackages_8_12 coq_8_12
+    coqPackages_8_13 coq_8_13
     coqPackages      coq
   ;
 
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index 46b7094cb3a..35f384a46c6 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -125,6 +125,9 @@ in rec {
   coq_8_12 = callPackage ../applications/science/logic/coq {
     version = "8.12.1";
   };
+  coq_8_13 = callPackage ../applications/science/logic/coq {
+    version = "8.13+beta1";
+  };
 
   coqPackages_8_5 = mkCoqPackages coq_8_5;
   coqPackages_8_6 = mkCoqPackages coq_8_6;
@@ -134,6 +137,7 @@ in rec {
   coqPackages_8_10 = mkCoqPackages coq_8_10;
   coqPackages_8_11 = mkCoqPackages coq_8_11;
   coqPackages_8_12 = mkCoqPackages coq_8_12;
+  coqPackages_8_13 = mkCoqPackages coq_8_13;
   coqPackages = recurseIntoAttrs (lib.mapDerivationAttrset lib.dontDistribute
     coqPackages_8_11
   );