From fe543c7576ec04e4512f1d8ef8babfd72808f573 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Mon, 23 Feb 2026 09:38:44 +0100 Subject: [PATCH 1/2] coqPackages.compcert: fix fmt --- .../coq-modules/compcert/default.nix | 28 ++++++------------- 1 file changed, 8 insertions(+), 20 deletions(-) diff --git a/pkgs/development/coq-modules/compcert/default.nix b/pkgs/development/coq-modules/compcert/default.nix index fe4f294e81d0..42e51aad93d5 100644 --- a/pkgs/development/coq-modules/compcert/default.nix +++ b/pkgs/development/coq-modules/compcert/default.nix @@ -38,28 +38,16 @@ let releaseRev = v: "v${v}"; defaultVersion = + let + case = case: out: { inherit case out; }; + in with lib.versions; lib.switch coq.version [ - { - case = range "8.15" "9.1"; - out = "3.17"; - } - { - case = range "8.14" "8.20"; - out = "3.15"; - } - { - case = isEq "8.13"; - out = "3.10"; - } - { - case = isEq "8.12"; - out = "3.9"; - } - { - case = range "8.8" "8.11"; - out = "3.8"; - } + (case (range "8.15" "9.1") "3.17") + (case (range "8.14" "8.20") "3.15") + (case (isEq "8.13") "3.10") + (case (isEq "8.12") "3.9") + (case (range "8.8" "8.11") "3.8") ] null; release = { From 3db198457b0e56a4edd1315d66e1b7c0c139e2c7 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Mon, 23 Feb 2026 09:33:41 +0100 Subject: [PATCH 2/2] coqPackages.flocq: 4.2.1 -> 4.2.2 --- .../development/coq-modules/flocq/default.nix | 96 +++++++++++-------- 1 file changed, 54 insertions(+), 42 deletions(-) diff --git a/pkgs/development/coq-modules/flocq/default.nix b/pkgs/development/coq-modules/flocq/default.nix index c4b604358ca2..ceb1879e5165 100644 --- a/pkgs/development/coq-modules/flocq/default.nix +++ b/pkgs/development/coq-modules/flocq/default.nix @@ -8,49 +8,61 @@ version ? null, }: -mkCoqDerivation { - pname = "flocq"; - owner = "flocq"; - domain = "gitlab.inria.fr"; - inherit version; - defaultVersion = - let - case = case: out: { inherit case out; }; - in - with lib.versions; - lib.switch coq.coq-version [ - (case (range "8.15" "9.1") "4.2.1") - (case (range "8.14" "8.20") "4.2.0") - (case (range "8.14" "8.18") "4.1.3") - (case (range "8.14" "8.17") "4.1.1") - (case (range "8.14" "8.16") "4.1.0") - (case (range "8.7" "8.15") "3.4.3") - (case (range "8.5" "8.8") "2.6.1") - ] null; - release."4.2.1".sha256 = "sha256-W5hcAm0GGmNsvre79/iGNcoBwFzStC4G177hZ3ds/4E="; - release."4.2.0".sha256 = "sha256-uTeo4GCs6wTLN3sLKsj0xLlt1fUDYfozXtq6iooLUgM="; - release."4.1.4".sha256 = "sha256-Use6Mlx79yef1CkCPyGoOItsD69B9KR+mQArCtmre4s="; - release."4.1.3".sha256 = "sha256-os3cI885xNpxI+1p5rb8fSNnxKr7SFxqh83+3AM3t4I="; - release."4.1.1".sha256 = "sha256-FbClxlV0ZaxITe7s9SlNbpeMNDJli+Dfh2TMrjaMtHo="; - release."4.1.0".sha256 = "sha256:09rak9cha7q11yfqracbcq75mhmir84331h1218xcawza48rbjik"; - release."3.4.3".sha256 = "sha256-YTdWlEmFJjCcHkl47jSOgrGqdXoApJY4u618ofCaCZE="; - release."3.4.2".sha256 = "1s37hvxyffx8ccc8mg5aba7ivfc39p216iibvd7f2cb9lniqk1pw"; - release."3.3.1".sha256 = "1mk8adhi5hrllsr0hamzk91vf2405sjr4lh5brg9201mcw11abkz"; - release."2.6.1".sha256 = "0q5a038ww5dn72yvwn5298d3ridkcngb1dik8hdyr3xh7gr5qibj"; - releaseRev = v: "flocq-${v}"; +let + derivation = mkCoqDerivation { + pname = "flocq"; + owner = "flocq"; + domain = "gitlab.inria.fr"; + inherit version; + defaultVersion = + let + case = case: out: { inherit case out; }; + in + with lib.versions; + lib.switch coq.coq-version [ + (case (range "8.15" "9.2") "4.2.2") + (case (range "8.15" "9.1") "4.2.1") + (case (range "8.14" "8.20") "4.2.0") + (case (range "8.14" "8.18") "4.1.3") + (case (range "8.14" "8.17") "4.1.1") + (case (range "8.14" "8.16") "4.1.0") + (case (range "8.7" "8.15") "3.4.3") + (case (range "8.5" "8.8") "2.6.1") + ] null; + release."4.2.2".sha256 = "sha256-1q4V6KyRb0tEeqBcBTUKmAxCJktqe/MN2C9zdbyv7hk="; + release."4.2.1".sha256 = "sha256-W5hcAm0GGmNsvre79/iGNcoBwFzStC4G177hZ3ds/4E="; + release."4.2.0".sha256 = "sha256-uTeo4GCs6wTLN3sLKsj0xLlt1fUDYfozXtq6iooLUgM="; + release."4.1.4".sha256 = "sha256-Use6Mlx79yef1CkCPyGoOItsD69B9KR+mQArCtmre4s="; + release."4.1.3".sha256 = "sha256-os3cI885xNpxI+1p5rb8fSNnxKr7SFxqh83+3AM3t4I="; + release."4.1.1".sha256 = "sha256-FbClxlV0ZaxITe7s9SlNbpeMNDJli+Dfh2TMrjaMtHo="; + release."4.1.0".sha256 = "sha256:09rak9cha7q11yfqracbcq75mhmir84331h1218xcawza48rbjik"; + release."3.4.3".sha256 = "sha256-YTdWlEmFJjCcHkl47jSOgrGqdXoApJY4u618ofCaCZE="; + release."3.4.2".sha256 = "1s37hvxyffx8ccc8mg5aba7ivfc39p216iibvd7f2cb9lniqk1pw"; + release."3.3.1".sha256 = "1mk8adhi5hrllsr0hamzk91vf2405sjr4lh5brg9201mcw11abkz"; + release."2.6.1".sha256 = "0q5a038ww5dn72yvwn5298d3ridkcngb1dik8hdyr3xh7gr5qibj"; + releaseRev = v: "flocq-${v}"; - nativeBuildInputs = [ - bash - autoconf - ]; - mlPlugin = true; - useMelquiondRemake.logpath = "Flocq"; + nativeBuildInputs = [ + bash + autoconf + ]; + mlPlugin = true; + useMelquiondRemake.logpath = "Flocq"; - propagatedBuildInputs = [ stdlib ]; + propagatedBuildInputs = [ stdlib ]; - meta = { - description = "Floating-point formalization for the Coq system"; - license = lib.licenses.lgpl3; - maintainers = with lib.maintainers; [ jwiegley ]; + meta = { + description = "Floating-point formalization for the Coq system"; + license = lib.licenses.lgpl3; + maintainers = with lib.maintainers; [ jwiegley ]; + }; }; -} + patched-derivation = derivation.overrideAttrs ( + o: + lib.optionalAttrs (o.version != null && (o.version == "dev" || lib.versions.isGe "4.2.2" o.version)) + { + nativeBuildInputs = o.nativeBuildInputs ++ [ coq.ocamlPackages.ocaml ]; + } + ); +in +patched-derivation