rocq-core: 9.0+rc1 -> 9.0.0 (#389454)

Author: vbgl

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

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

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
       '';

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";

pkgs/top-level/all-packages.nix

@@ -5648,7 +5648,7 @@ with pkgs;
     ocamlPackages = ocaml-ng.ocamlPackages_4_14;
   };
 
-  inherit (coqPackages) compcert;
+  inherit (coqPackages_8_20) compcert;
 
   computecpp = wrapCCWith rec {
     cc = computecpp-unwrapped;
@@ -17058,7 +17058,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; };

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;
 }

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;