From 582a03331265dea5501db0e047e4fd58cbd4f53e Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 13 Mar 2025 08:59:01 +0100 Subject: [PATCH 1/2] coq: 9.0+rc1 -> 9.0.0 --- pkgs/applications/science/logic/coq/default.nix | 2 +- pkgs/applications/science/logic/rocq-core/default.nix | 2 +- pkgs/top-level/all-packages.nix | 5 +++-- pkgs/top-level/coq-packages.nix | 4 ++-- pkgs/top-level/rocq-packages.nix | 2 +- 5 files changed, 8 insertions(+), 7 deletions(-) diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix index fe8e77b1f1c3..4b8e9eab7abb 100644 --- a/pkgs/applications/science/logic/coq/default.nix +++ b/pkgs/applications/science/logic/coq/default.nix @@ -61,7 +61,7 @@ let "8.19.2".sha256 = "sha256-q+i07JsMZp83Gqav6v1jxsgPLN7sPvp5/oszVnavmz0="; "8.20.0".sha256 = "sha256-WFpZlA6CzFVAruPhWcHQI7VOBVhrGLdFzWrHW0DTSl0="; "8.20.1".sha256 = "sha256-nRaLODPG4E3gUDzGrCK40vhl4+VhPyd+/fXFK/HC3Ig="; - "9.0+rc1".sha256 = "sha256-TLq925HFdizxyHjKRMeHBH9rLRpLNUiVIfA1JSMgYXA="; + "9.0.0".sha256 = "sha256-GRwYSvrJGiPD+I82gLOgotb+8Ra5xHZUJGcNwxWqZkU="; }; releaseRev = v: "V${v}"; fetched = import ../../../../build-support/coq/meta-fetch/default.nix diff --git a/pkgs/applications/science/logic/rocq-core/default.nix b/pkgs/applications/science/logic/rocq-core/default.nix index 88d8dcf26616..ec6a132f340f 100644 --- a/pkgs/applications/science/logic/rocq-core/default.nix +++ b/pkgs/applications/science/logic/rocq-core/default.nix @@ -15,7 +15,7 @@ let lib = import ../../../../build-support/coq/extra-lib.nix { inherit (args) lib; }; release = { - "9.0+rc1".sha256 = "sha256-TLq925HFdizxyHjKRMeHBH9rLRpLNUiVIfA1JSMgYXA="; + "9.0.0".sha256 = "sha256-GRwYSvrJGiPD+I82gLOgotb+8Ra5xHZUJGcNwxWqZkU="; }; releaseRev = v: "V${v}"; fetched = import ../../../../build-support/coq/meta-fetch/default.nix diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index ac7fd2d9f463..33daf1235411 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -5668,7 +5668,7 @@ with pkgs; ocamlPackages = ocaml-ng.ocamlPackages_4_14; }; - inherit (coqPackages) compcert; + inherit (coqPackages_8_20) compcert; computecpp = wrapCCWith rec { cc = computecpp-unwrapped; @@ -17078,7 +17078,8 @@ with pkgs; stdenv = gccStdenv; }; - why3 = callPackage ../applications/science/logic/why3 { }; + why3 = callPackage ../applications/science/logic/why3 + { coqPackages = coqPackages_8_20; }; yices = callPackage ../applications/science/logic/yices { gmp-static = gmp.override { withStatic = true; }; diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix index c79ab2016ce8..ad96a655d439 100644 --- a/pkgs/top-level/coq-packages.nix +++ b/pkgs/top-level/coq-packages.nix @@ -237,7 +237,7 @@ in rec { coq_8_18 = mkCoq "8.18"; coq_8_19 = mkCoq "8.19"; coq_8_20 = mkCoq "8.20"; - coq_9_0 = mkCoq "9.0+rc1"; + coq_9_0 = mkCoq "9.0"; coqPackages_8_5 = mkCoqPackages coq_8_5; coqPackages_8_6 = mkCoqPackages coq_8_6; @@ -257,6 +257,6 @@ in rec { coqPackages_8_20 = mkCoqPackages coq_8_20; coqPackages_9_0 = mkCoqPackages coq_9_0; - coqPackages = recurseIntoAttrs coqPackages_8_20; + coqPackages = recurseIntoAttrs coqPackages_9_0; coq = coqPackages.coq; } diff --git a/pkgs/top-level/rocq-packages.nix b/pkgs/top-level/rocq-packages.nix index a6478bda519f..1253ebd1f4f8 100644 --- a/pkgs/top-level/rocq-packages.nix +++ b/pkgs/top-level/rocq-packages.nix @@ -49,7 +49,7 @@ in rec { let self = lib.makeScope newScope (lib.flip mkRocqPackages' rocq-core); in self.filterPackages (! rocq-core.dontFilter or false); - rocq-core_9_0 = mkRocq "9.0+rc1"; + rocq-core_9_0 = mkRocq "9.0"; rocqPackages_9_0 = mkRocqPackages rocq-core_9_0; From 92f87ee7ac9fbb4e20e29d4e9c66e2f5bc7c8f55 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 13 Mar 2025 09:19:48 +0100 Subject: [PATCH 2/2] rocqPackages.stdlib: 9.0+rc1 -> 9.0.0 --- .../coq-modules/stdlib/default.nix | 22 ++++++++--------- .../rocq-modules/stdlib/default.nix | 24 ++++--------------- 2 files changed, 15 insertions(+), 31 deletions(-) diff --git a/pkgs/development/coq-modules/stdlib/default.nix b/pkgs/development/coq-modules/stdlib/default.nix index 033fc30330f2..8b3563253c55 100644 --- a/pkgs/development/coq-modules/stdlib/default.nix +++ b/pkgs/development/coq-modules/stdlib/default.nix @@ -16,16 +16,20 @@ defaultVersion = with lib.versions; lib.switch coq.version [ - { case = isEq "9.0"; out = "9.0+rc1"; } - { case = isLt "8.21"; out = "8.20"; } + { case = isEq "9.0"; out = "9.0.0"; } + # the one below is artificial as stdlib was included in Coq before + { case = isLt "9.0"; out = "9.0.0"; } ] null; releaseRev = v: "V${v}"; - release."9.0+rc1".sha256 = "sha256-raHwniQdpAX1HGlMofM8zVeXcmlUs+VJZZg5VF43k/M="; - release."8.20".sha256 = "sha256-AcoS4edUYCfJME1wx8UbuSQRF3jmxhArcZyPIoXcfu0="; - - useDune = true; + release."9.0.0".sha256 = "sha256-2l7ak5Q/NbiNvUzIVXOniEneDXouBMNSSVFbD1Pf8cQ="; + configurePhase = '' + echo no configuration + ''; + buildPhase = '' + echo building nothing + ''; installPhase = '' echo installing nothing ''; @@ -40,12 +44,6 @@ o: # stdlib is already included in Coq <= 8.20 if coq.version != null && coq.version != "dev" && lib.versions.isLt "8.21" coq.version then { - configurePhase = '' - echo no configuration - ''; - buildPhase = '' - echo building nothing - ''; installPhase = '' touch $out ''; diff --git a/pkgs/development/rocq-modules/stdlib/default.nix b/pkgs/development/rocq-modules/stdlib/default.nix index 6bfce6dacf24..2686c0f8ca7c 100644 --- a/pkgs/development/rocq-modules/stdlib/default.nix +++ b/pkgs/development/rocq-modules/stdlib/default.nix @@ -15,29 +15,15 @@ mkRocqDerivation { defaultVersion = with lib.versions; lib.switch rocq-core.version [ - { case = isEq "9.0"; out = "9.0+rc1"; } - { case = isLt "8.21"; out = "8.20"; } + { case = isEq "9.0"; out = "9.0.0"; } + # the one below is artificial as stdlib was included in Coq before + { case = isLt "9.0"; out = "9.0.0"; } ] null; releaseRev = v: "V${v}"; - release."9.0+rc1".sha256 = "sha256-raHwniQdpAX1HGlMofM8zVeXcmlUs+VJZZg5VF43k/M="; - release."8.20".sha256 = "sha256-AcoS4edUYCfJME1wx8UbuSQRF3jmxhArcZyPIoXcfu0="; + release."9.0.0".sha256 = "sha256-2l7ak5Q/NbiNvUzIVXOniEneDXouBMNSSVFbD1Pf8cQ="; - useDune = true; - - configurePhase = '' - patchShebangs dev/with-rocq-wrap.sh - ''; - - buildPhase = '' - dev/with-rocq-wrap.sh dune build -p rocq-stdlib @install ''${enableParallelBuilding:+-j $NIX_BUILD_CORES} - ''; - - installPhase = '' - dev/with-rocq-wrap.sh dune install --root . rocq-stdlib --prefix=$out --libdir $OCAMLFIND_DESTDIR - mkdir $out/lib/coq/ - mv $OCAMLFIND_DESTDIR/coq $out/lib/coq/${rocq-core.rocq-version} - ''; + mlPlugin = true; meta = { description = "The Rocq Proof Assistant -- Standard Library";