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

rocq-core_9_3: init at 9.3+rc1 (#544800)

Browse Source
This commit is contained in:
Vincent Laporte
2026-07-23 14:16:21 +00:00
committed by GitHub
parent 373f67b3b3 363e06dfb5
commit 82c76eb37c
7 changed files with 67 additions and 88 deletions
Download Patch File Download Diff File Expand all files Collapse all files
pkgs/applications/science/logic/coq/default.nix
+14 -2
View File
@@ -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
];
pkgs/applications/science/logic/rocq-core/default.nix
+11 -3
View File
@@ -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
pkgs/development/coq-modules/aac-tactics/default.nix
+20 -65
View File
@@ -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;
pkgs/development/coq-modules/unicoq/default.nix
+6 -12
View File
@@ -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=";
pkgs/top-level/all-packages.nix
+7 -2
View File
@@ -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
;
pkgs/top-level/coq-packages.nix
+5 -2
View File
@@ -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;
pkgs/top-level/rocq-packages.nix
+4 -2
View File
@@ -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;