diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix index 1884ef85fe57..5f8526d879aa 100644 --- a/pkgs/applications/science/logic/coq/default.nix +++ b/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 diff --git a/pkgs/applications/science/logic/rocq-core/default.nix b/pkgs/applications/science/logic/rocq-core/default.nix index 3d76ff2d0fda..bf8776d13d70 100644 --- a/pkgs/applications/science/logic/rocq-core/default.nix +++ b/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 diff --git a/pkgs/development/coq-modules/coqutil/default.nix b/pkgs/development/coq-modules/coqutil/default.nix index 67655165ae14..0fd659c2d098 100644 --- a/pkgs/development/coq-modules/coqutil/default.nix +++ b/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}"; diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 78cc0f997b23..ff104c4f6f5a 100644 --- a/pkgs/top-level/all-packages.nix +++ b/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 ; diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix index 04e481cb08f3..b24ab749b997 100644 --- a/pkgs/top-level/coq-packages.nix +++ b/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; diff --git a/pkgs/top-level/rocq-packages.nix b/pkgs/top-level/rocq-packages.nix index ed0327ee96ec..0ce9d5f897de 100644 --- a/pkgs/top-level/rocq-packages.nix +++ b/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;