diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix index aedee50cefef..39c8278a232e 100644 --- a/pkgs/applications/science/logic/coq/default.nix +++ b/pkgs/applications/science/logic/coq/default.nix @@ -19,7 +19,7 @@ ocamlPackages_4_10, ocamlPackages_4_12, ocamlPackages_4_14, - ocamlPackages_5_4, + ocamlPackages_5_5, 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 @@ -76,6 +76,7 @@ let "9.1.0".sha256 = "sha256-+QL7I1/0BfT87n7lSaOmpHj2jJuDB4idWhAxwzvVQOE="; "9.1.1".sha256 = "sha256-aFsGsFzexyDnOVarHPKs35HjiV8uUCpeOKSl15wXZ4s="; "9.2.0".sha256 = "sha256-rVhv2GLImdVPgRwwTQ+wiWNtRUflMrES0ElIrdTIN1s="; + "9.3+rc1".sha256 = "sha256-vGJkRRzf8ur7i9IUpRA/sxVEQvZGnxfV/ex28Lt1kWw="; }; releaseRev = v: "V${v}"; fetched = @@ -140,12 +141,15 @@ let case = lib.versions.range "8.7" "8.10"; out = ocamlPackages_4_09; } - ] ocamlPackages_5_4; + ] ocamlPackages_5_5; ocamlNativeBuildInputs = [ ocamlPackages.ocaml ocamlPackages.findlib ] ++ lib.optional (coqAtLeast "8.14") dune; + ocamlBuildInputs = [ + ocamlPackages.findlib + ]; ocamlPropagatedBuildInputs = [ ] ++ lib.optional (!coqAtLeast "8.10") ocamlPackages.camlp5 @@ -225,6 +229,7 @@ let buildInputs = [ ncurses ] + ++ ocamlBuildInputs ++ lib.optionals buildIde ( if coqAtLeast "8.10" then [ @@ -328,11 +333,18 @@ let platforms = lib.platforms.unix; mainProgram = if buildIde then "coqide" else "coqtop"; }; + + # Things required by the CI + strictDeps = true; + __structuredAttrs = true; }; in if coqAtLeast "8.21" then self.overrideAttrs (o: { # coq-core is now a shim for rocq + nativeBuildInputs = o.nativeBuildInputs ++ [ + rocqPackages.rocq-core + ]; propagatedBuildInputs = o.propagatedBuildInputs ++ [ rocqPackages.rocq-core ]; diff --git a/pkgs/applications/science/logic/rocq-core/default.nix b/pkgs/applications/science/logic/rocq-core/default.nix index a6501daaaa3f..68a2c3895e98 100644 --- a/pkgs/applications/science/logic/rocq-core/default.nix +++ b/pkgs/applications/science/logic/rocq-core/default.nix @@ -14,7 +14,7 @@ dune, customOCamlPackages ? null, ocamlPackages_4_14, - ocamlPackages_5_4, + ocamlPackages_5_5, ncurses, csdp ? null, version, @@ -29,6 +29,7 @@ let "9.1.0".sha256 = "sha256-+QL7I1/0BfT87n7lSaOmpHj2jJuDB4idWhAxwzvVQOE="; "9.1.1".sha256 = "sha256-aFsGsFzexyDnOVarHPKs35HjiV8uUCpeOKSl15wXZ4s="; "9.2.0".sha256 = "sha256-rVhv2GLImdVPgRwwTQ+wiWNtRUflMrES0ElIrdTIN1s="; + "9.3+rc1".sha256 = "sha256-vGJkRRzf8ur7i9IUpRA/sxVEQvZGnxfV/ex28Lt1kWw="; }; releaseRev = v: "V${v}"; fetched = @@ -66,12 +67,15 @@ let in lib.switch rocq-version [ (case (range "9.0" "9.1") ocamlPackages_4_14) - ] ocamlPackages_5_4; + ] ocamlPackages_5_5; ocamlNativeBuildInputs = [ ocamlPackages.ocaml ocamlPackages.findlib dune ]; + ocamlBuildInputs = [ + ocamlPackages.findlib + ]; ocamlPropagatedBuildInputs = [ ocamlPackages.zarith ]; self = stdenv.mkDerivation { pname = "rocq"; @@ -130,7 +134,7 @@ let }; nativeBuildInputs = [ pkg-config ] ++ ocamlNativeBuildInputs; - buildInputs = [ ncurses ]; + buildInputs = [ ncurses ] ++ ocamlBuildInputs; propagatedBuildInputs = ocamlPropagatedBuildInputs; @@ -196,6 +200,10 @@ let platforms = lib.platforms.unix; mainProgram = "rocq"; }; + + # Things required by the CI + strictDeps = true; + __structuredAttrs = true; }; in self diff --git a/pkgs/development/coq-modules/aac-tactics/default.nix b/pkgs/development/coq-modules/aac-tactics/default.nix index 65ee981171ae..4d27ac065a44 100644 --- a/pkgs/development/coq-modules/aac-tactics/default.nix +++ b/pkgs/development/coq-modules/aac-tactics/default.nix @@ -33,72 +33,27 @@ mkCoqDerivation { inherit version; defaultVersion = - + let + case = case: out: { inherit case out; }; + in + with lib.versions; lib.switch coq.coq-version [ - { - case = lib.versions.isGe "9.0"; - out = "9.0.0"; - } - { - case = "8.20"; - out = "8.20.0"; - } - { - case = "8.19"; - out = "8.19.1"; - } - { - case = "8.18"; - out = "8.18.0"; - } - { - case = "8.17"; - out = "8.17.0"; - } - { - case = "8.16"; - out = "8.16.0"; - } - { - case = "8.15"; - out = "8.15.1"; - } - { - case = "8.14"; - out = "8.14.1"; - } - { - case = "8.13"; - out = "8.13.2"; - } - { - case = "8.12"; - out = "8.12.0"; - } - { - case = "8.11"; - out = "8.11.0"; - } - { - case = "8.10"; - out = "8.10.0"; - } - { - case = "8.9"; - out = "8.9.0"; - } - { - case = "8.8"; - out = "8.8.0"; - } - { - case = "8.6"; - out = "8.6.1"; - } - { - case = "8.5"; - out = "8.5.0"; - } + (case (range "9.0" "9.2") "9.0.0") + (case "8.20" "8.20.0") + (case "8.19" "8.19.1") + (case "8.18" "8.18.0") + (case "8.17" "8.17.0") + (case "8.16" "8.16.0") + (case "8.15" "8.15.0") + (case "8.14" "8.14.1") + (case "8.13" "8.13.2") + (case "8.12" "8.12.0") + (case "8.11" "8.11.0") + (case "8.10" "8.10.0") + (case "8.9" "8.9.0") + (case "8.8" "8.8.0") + (case "8.6" "8.6.1") + (case "8.5" "8.5.0") ] null; mlPlugin = true; diff --git a/pkgs/development/coq-modules/unicoq/default.nix b/pkgs/development/coq-modules/unicoq/default.nix index 135f6515d397..8f8af5583689 100644 --- a/pkgs/development/coq-modules/unicoq/default.nix +++ b/pkgs/development/coq-modules/unicoq/default.nix @@ -10,20 +10,14 @@ mkCoqDerivation { owner = "unicoq"; inherit version; defaultVersion = + let + case = case: out: { inherit case out; }; + in with lib.versions; lib.switch coq.version [ - { - case = isGe "9.1"; - out = "1.6-9.1"; - } - { - case = range "8.20" "9.0"; - out = "1.6-8.20"; - } - { - case = range "8.19" "8.19"; - out = "1.6-8.19"; - } + (case (range "9.1" "9.1") "1.6-9.1") + (case (range "8.20" "9.0") "1.6-8.20") + (case (range "8.19" "8.19") "1.6-8.19") ] null; release."1.6-9.1".rev = "0cf37ef7e638bfaad6e804e17bd80e7bb0e1b717"; release."1.6-9.1".hash = "sha256-1EKDkj33pg3AsEpckZYqWppPUZV2OkxM2xLq2zvZGMQ="; diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index a552d5bc492e..c33b87cd6b67 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -10383,7 +10383,7 @@ with pkgs; (callPackage ./rocq-packages.nix { inherit (ocaml-ng) ocamlPackages_4_14 - ocamlPackages_5_4 + ocamlPackages_5_5 ; }) mkRocqPackages @@ -10393,6 +10393,8 @@ with pkgs; rocq-core_9_1 rocqPackages_9_2 rocq-core_9_2 + rocqPackages_9_3 + rocq-core_9_3 rocqPackages rocq-core ; @@ -10404,12 +10406,13 @@ with pkgs; ocamlPackages_4_10 ocamlPackages_4_12 ocamlPackages_4_14 - ocamlPackages_5_4 + ocamlPackages_5_5 ; inherit rocqPackages_9_0 rocqPackages_9_1 rocqPackages_9_2 + rocqPackages_9_3 rocqPackages ; }) @@ -10448,6 +10451,8 @@ with pkgs; coq_9_1 coqPackages_9_2 coq_9_2 + coqPackages_9_3 + coq_9_3 coqPackages coq ; diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix index ebe42498e38a..ec4a42f8b692 100644 --- a/pkgs/top-level/coq-packages.nix +++ b/pkgs/top-level/coq-packages.nix @@ -9,10 +9,11 @@ ocamlPackages_4_10, ocamlPackages_4_12, ocamlPackages_4_14, - ocamlPackages_5_4, + ocamlPackages_5_5, rocqPackages_9_0, rocqPackages_9_1, rocqPackages_9_2, + rocqPackages_9_3, rocqPackages, fetchpatch, makeWrapper, @@ -311,7 +312,7 @@ let ocamlPackages_4_10 ocamlPackages_4_12 ocamlPackages_4_14 - ocamlPackages_5_4 + ocamlPackages_5_5 ; rocqPackages = rp; }; @@ -351,6 +352,7 @@ rec { 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); + coqPackages_9_3 = mkCoqPackages (mkCoq "9.3" rocqPackages_9_3); coq_8_7 = coqPackages_8_7.coq; coq_8_8 = coqPackages_8_8.coq; @@ -369,6 +371,7 @@ rec { coq_9_0 = coqPackages_9_0.coq; coq_9_1 = coqPackages_9_1.coq; coq_9_2 = coqPackages_9_2.coq; + coq_9_3 = coqPackages_9_3.coq; coqPackages = lib.recurseIntoAttrs coqPackages_9_1; coq = coqPackages.coq; diff --git a/pkgs/top-level/rocq-packages.nix b/pkgs/top-level/rocq-packages.nix index 7b48e4d73079..d3adb57ae40e 100644 --- a/pkgs/top-level/rocq-packages.nix +++ b/pkgs/top-level/rocq-packages.nix @@ -6,7 +6,7 @@ callPackage, newScope, ocamlPackages_4_14, - ocamlPackages_5_4, + ocamlPackages_5_5, fetchpatch, makeWrapper, }@args: @@ -91,7 +91,7 @@ let inherit version ocamlPackages_4_14 - ocamlPackages_5_4 + ocamlPackages_5_5 ; }; in @@ -116,10 +116,12 @@ rec { rocq-core_9_0 = mkRocq "9.0"; rocq-core_9_1 = mkRocq "9.1"; rocq-core_9_2 = mkRocq "9.2"; + rocq-core_9_3 = mkRocq "9.3"; 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_9_3 = mkRocqPackages rocq-core_9_3; rocqPackages = lib.recurseIntoAttrs rocqPackages_9_1; rocq-core = rocqPackages.rocq-core;