rocq-core_9_2: init at 9.2+rc1 (#487257)

pkgs/applications/science/logic/coq/default.nix

@@ -19,6 +19,7 @@
   ocamlPackages_4_10,
   ocamlPackages_4_12,
   ocamlPackages_4_14,
+  ocamlPackages_5_4,
   rocqPackages, # for versions >= 9.0 that are transition shims on top of Rocq
   ncurses,
   buildIde ? null, # default is true for Coq < 8.14 and false for Coq >= 8.14
@@ -73,6 +74,7 @@ let
     "9.0.0".sha256 = "sha256-GRwYSvrJGiPD+I82gLOgotb+8Ra5xHZUJGcNwxWqZkU=";
     "9.0.1".sha256 = "sha256-gRgQhFiYvGR/Z46TmTl1bgN9O32nifxQGdrzfw0WHrk=";
     "9.1.0".sha256 = "sha256-+QL7I1/0BfT87n7lSaOmpHj2jJuDB4idWhAxwzvVQOE=";
+    "9.2+rc1".sha256 = "sha256-zKVhnBid5LOcd7uHWFGmUdHpyNLxIyB7RNNz5btz0mI=";
   };
   releaseRev = v: "V${v}";
   fetched =
@@ -111,7 +113,7 @@ let
     else
       lib.switch coq-version [
         {
-          case = lib.versions.range "8.16" "8.18";
+          case = lib.versions.range "8.16" "9.1";
           out = ocamlPackages_4_14;
         }
         {
@@ -126,7 +128,7 @@ let
           case = lib.versions.range "8.7" "8.10";
           out = ocamlPackages_4_09;
         }
-      ] ocamlPackages_4_14;
+      ] ocamlPackages_5_4;
   ocamlNativeBuildInputs = [
     ocamlPackages.ocaml
     ocamlPackages.findlib

pkgs/applications/science/logic/rocq-core/default.nix

@@ -14,6 +14,7 @@
   dune,
   customOCamlPackages ? null,
   ocamlPackages_4_14,
+  ocamlPackages_5_4,
   ncurses,
   csdp ? null,
   version,
@@ -26,6 +27,7 @@ let
     "9.0.0".sha256 = "sha256-GRwYSvrJGiPD+I82gLOgotb+8Ra5xHZUJGcNwxWqZkU=";
     "9.0.1".sha256 = "sha256-gRgQhFiYvGR/Z46TmTl1bgN9O32nifxQGdrzfw0WHrk=";
     "9.1.0".sha256 = "sha256-+QL7I1/0BfT87n7lSaOmpHj2jJuDB4idWhAxwzvVQOE=";
+    "9.2+rc1".sha256 = "sha256-zKVhnBid5LOcd7uHWFGmUdHpyNLxIyB7RNNz5btz0mI=";
   };
   releaseRev = v: "V${v}";
   fetched =
@@ -53,7 +55,17 @@ let
     substituteInPlace plugins/micromega/sos.ml --replace-warn "; csdp" "; ${csdp}/bin/csdp"
     substituteInPlace plugins/micromega/coq_micromega.ml --replace-warn "System.is_in_system_path \"csdp\"" "true"
   '';
-  ocamlPackages = if customOCamlPackages != null then customOCamlPackages else ocamlPackages_4_14;
+  ocamlPackages =
+    if customOCamlPackages != null then
+      customOCamlPackages
+    else
+      let
+        case = case: out: { inherit case out; };
+        inherit (lib.versions) range;
+      in
+      lib.switch rocq-version [
+        (case (range "9.0" "9.1") ocamlPackages_4_14)
+      ] ocamlPackages_5_4;
   ocamlNativeBuildInputs = [
     ocamlPackages.ocaml
     ocamlPackages.findlib

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

@@ -13,20 +13,14 @@
 
   inherit version;
   defaultVersion =
-    with lib.versions;
+    let
+      case = case: out: { inherit case out; };
+      inherit (lib.versions) range;
+    in
     lib.switch coq.version [
-      {
-        case = isGe "9.0";
-        out = "0.0.7";
-      }
-      {
-        case = range "8.18" "8.20";
-        out = "0.0.6";
-      }
-      {
-        case = range "8.17" "8.20";
-        out = "0.0.5";
-      }
+      (case (range "9.0" "9.1") "0.0.7")
+      (case (range "8.18" "8.20") "0.0.6")
+      (case (range "8.17" "8.20") "0.0.5")
     ] null;
 
   releaseRev = v: "v${v}";

pkgs/top-level/all-packages.nix

@@ -12306,6 +12306,7 @@ with pkgs;
     (callPackage ./rocq-packages.nix {
       inherit (ocaml-ng)
         ocamlPackages_4_14
+        ocamlPackages_5_4
         ;
     })
     mkRocqPackages
@@ -12313,6 +12314,8 @@ with pkgs;
     rocq-core_9_0
     rocqPackages_9_1
     rocq-core_9_1
+    rocqPackages_9_2
+    rocq-core_9_2
     rocqPackages
     rocq-core
     ;
@@ -12324,10 +12327,12 @@ with pkgs;
         ocamlPackages_4_10
         ocamlPackages_4_12
         ocamlPackages_4_14
+        ocamlPackages_5_4
         ;
       inherit
         rocqPackages_9_0
         rocqPackages_9_1
+        rocqPackages_9_2
         rocqPackages
         ;
     })
@@ -12364,6 +12369,8 @@ with pkgs;
     coq_9_0
     coqPackages_9_1
     coq_9_1
+    coqPackages_9_2
+    coq_9_2
     coqPackages
     coq
     ;

pkgs/top-level/coq-packages.nix

@@ -9,8 +9,10 @@
   ocamlPackages_4_10,
   ocamlPackages_4_12,
   ocamlPackages_4_14,
+  ocamlPackages_5_4,
   rocqPackages_9_0,
   rocqPackages_9_1,
+  rocqPackages_9_2,
   rocqPackages,
   fetchpatch,
   makeWrapper,
@@ -292,6 +294,7 @@ let
         ocamlPackages_4_10
         ocamlPackages_4_12
         ocamlPackages_4_14
+        ocamlPackages_5_4
         ;
       rocqPackages = rp;
     };
@@ -330,6 +333,7 @@ rec {
   coqPackages_8_20 = mkCoqPackages (mkCoq "8.20" { });
   coqPackages_9_0 = mkCoqPackages (mkCoq "9.0" rocqPackages_9_0);
   coqPackages_9_1 = mkCoqPackages (mkCoq "9.1" rocqPackages_9_1);
+  coqPackages_9_2 = mkCoqPackages (mkCoq "9.2" rocqPackages_9_2);
 
   coq_8_7 = coqPackages_8_7.coq;
   coq_8_8 = coqPackages_8_8.coq;
@@ -347,6 +351,7 @@ rec {
   coq_8_20 = coqPackages_8_20.coq;
   coq_9_0 = coqPackages_9_0.coq;
   coq_9_1 = coqPackages_9_1.coq;
+  coq_9_2 = coqPackages_9_2.coq;
 
   coqPackages = lib.recurseIntoAttrs coqPackages_9_0;
   coq = coqPackages.coq;

pkgs/top-level/rocq-packages.nix

@@ -6,6 +6,7 @@
   callPackage,
   newScope,
   ocamlPackages_4_14,
+  ocamlPackages_5_4,
   fetchpatch,
   makeWrapper,
 }@args:
@@ -75,6 +76,7 @@ let
       inherit
         version
         ocamlPackages_4_14
+        ocamlPackages_5_4
         ;
     };
 in
@@ -98,9 +100,11 @@ rec {
 
   rocq-core_9_0 = mkRocq "9.0";
   rocq-core_9_1 = mkRocq "9.1";
+  rocq-core_9_2 = mkRocq "9.2";
 
   rocqPackages_9_0 = mkRocqPackages rocq-core_9_0;
   rocqPackages_9_1 = mkRocqPackages rocq-core_9_1;
+  rocqPackages_9_2 = mkRocqPackages rocq-core_9_2;
 
   rocqPackages = lib.recurseIntoAttrs rocqPackages_9_0;
   rocq-core = rocqPackages.rocq-core;