gador/nixpkgs
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

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

Browse Source
This commit is contained in:
Vincent Laporte
2025-03-17 11:28:25 +01:00
committed by GitHub
parent 79a38ed01e 92f87ee7ac
commit 6b776fde83
7 changed files with 23 additions and 38 deletions
Download Patch File Download Diff File Expand all files Collapse all files
pkgs/applications/science/logic/coq/default.nix
+1 -1
View File
@@ -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
+1 -1
View File
@@ -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
+10 -12
View File
@@ -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
+5 -19
View File
@@ -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
+3 -2
View File
@@ -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
+2 -2
View File
@@ -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
+1 -1
View File
@@ -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;