coqPackages.*: 9.0 -> 9.1
This commit is contained in:
Pierre Roux
committed by
Vincent Laporte
Vincent Laporte
parent
b3cf32038f
commit
6bb4f60316
@@ -11,16 +11,13 @@ mkCoqDerivation {
|
||||
owner = "uwplse";
|
||||
inherit version;
|
||||
defaultVersion =
|
||||
let
|
||||
case = case: out: { inherit case out; };
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch coq.version [
|
||||
{
|
||||
case = range "8.14" "9.0";
|
||||
out = "20230107";
|
||||
}
|
||||
{
|
||||
case = range "8.6" "8.16";
|
||||
out = "20200201";
|
||||
}
|
||||
(case (range "8.14" "9.1") "20230107")
|
||||
(case (range "8.6" "8.16") "20200201")
|
||||
] null;
|
||||
release."20230107".rev = "bad8ad2476e14df6b5a819b7aaddc27a7c53fb69";
|
||||
release."20230107".sha256 = "sha256-G7a+6h4VDk7seKvFr6wy7vYqYmhUje78TYCj98wXrr8=";
|
||||
|
||||
@@ -11,28 +11,16 @@ mkCoqDerivation {
|
||||
owner = "fblanqui";
|
||||
inherit version;
|
||||
defaultVersion =
|
||||
let
|
||||
case = case: out: { inherit case out; };
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch coq.version [
|
||||
{
|
||||
case = range "8.14" "9.0";
|
||||
out = "1.8.5";
|
||||
}
|
||||
{
|
||||
case = range "8.12" "8.16";
|
||||
out = "1.8.2";
|
||||
}
|
||||
{
|
||||
case = range "8.10" "8.11";
|
||||
out = "1.7.0";
|
||||
}
|
||||
{
|
||||
case = range "8.8" "8.9";
|
||||
out = "1.6.0";
|
||||
}
|
||||
{
|
||||
case = range "8.6" "8.7";
|
||||
out = "1.4.0";
|
||||
}
|
||||
(case (range "8.14" "9.1") "1.8.5")
|
||||
(case (range "8.12" "8.16") "1.8.2")
|
||||
(case (range "8.10" "8.11") "1.7.0")
|
||||
(case (range "8.8" "8.9") "1.6.0")
|
||||
(case (range "8.6" "8.7") "1.4.0")
|
||||
] null;
|
||||
|
||||
release."1.8.5".sha256 = "sha256-zKAyj6rKAasDF+iKExmpVHMe2WwgAwv2j1mmiVAl7ys=";
|
||||
|
||||
@@ -16,6 +16,15 @@ mkCoqDerivation {
|
||||
|
||||
inherit version;
|
||||
defaultVersion =
|
||||
let
|
||||
case = coq: mc: out: {
|
||||
cases = [
|
||||
coq
|
||||
mc
|
||||
];
|
||||
inherit out;
|
||||
};
|
||||
in
|
||||
with versions;
|
||||
switch
|
||||
[
|
||||
@@ -23,13 +32,7 @@ mkCoqDerivation {
|
||||
metacoq.version
|
||||
]
|
||||
[
|
||||
{
|
||||
cases = [
|
||||
(range "8.17" "9.0")
|
||||
(range "1.3.1" "1.3.4")
|
||||
];
|
||||
out = "0.1.1";
|
||||
}
|
||||
(case (range "8.17" "9.1") (range "1.3.1" "1.3.4") "0.1.1")
|
||||
]
|
||||
null;
|
||||
|
||||
|
||||
@@ -10,40 +10,19 @@ mkCoqDerivation {
|
||||
pname = "coq-ext-lib";
|
||||
inherit version;
|
||||
defaultVersion =
|
||||
let
|
||||
case = case: out: { inherit case out; };
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch coq.coq-version [
|
||||
{
|
||||
case = range "8.14" "9.0";
|
||||
out = "0.13.0";
|
||||
}
|
||||
{
|
||||
case = range "8.11" "8.19";
|
||||
out = "0.12.0";
|
||||
}
|
||||
{
|
||||
case = range "8.8" "8.16";
|
||||
out = "0.11.6";
|
||||
}
|
||||
{
|
||||
case = range "8.8" "8.14";
|
||||
out = "0.11.4";
|
||||
}
|
||||
{
|
||||
case = range "8.8" "8.13";
|
||||
out = "0.11.3";
|
||||
}
|
||||
{
|
||||
case = "8.7";
|
||||
out = "0.9.7";
|
||||
}
|
||||
{
|
||||
case = "8.6";
|
||||
out = "0.9.5";
|
||||
}
|
||||
{
|
||||
case = "8.5";
|
||||
out = "0.9.4";
|
||||
}
|
||||
(case (range "8.14" "9.1") "0.13.0")
|
||||
(case (range "8.11" "8.19") "0.12.0")
|
||||
(case (range "8.8" "8.16") "0.11.6")
|
||||
(case (range "8.8" "8.14") "0.11.4")
|
||||
(case (range "8.8" "8.13") "0.11.3")
|
||||
(case ("8.7") "0.9.7")
|
||||
(case ("8.6") "0.9.5")
|
||||
(case ("8.5") "0.9.4")
|
||||
] null;
|
||||
release."0.13.0".sha256 = "sha256-vqVSu+nyGjRVXe2tnE6MPl0kcg4LHfgFwRCpTQAP/is=";
|
||||
release."0.12.2".sha256 = "sha256-lSTlbpkSuAY6B9cqofXSlDk2VchtqfZpRQ0+y/BAbEY=";
|
||||
|
||||
@@ -12,20 +12,14 @@ mkCoqDerivation {
|
||||
owner = "DeepSpec";
|
||||
inherit version;
|
||||
defaultVersion =
|
||||
let
|
||||
case = case: out: { inherit case out; };
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch coq.version [
|
||||
{
|
||||
case = range "8.14" "9.0";
|
||||
out = "5.2.1";
|
||||
}
|
||||
{
|
||||
case = isEq "8.13";
|
||||
out = "5.2.0+20241009";
|
||||
}
|
||||
{
|
||||
case = range "8.10" "8.16";
|
||||
out = "4.0.0";
|
||||
}
|
||||
(case (range "8.14" "9.1") "5.2.1")
|
||||
(case (isEq "8.13") "5.2.0+20241009")
|
||||
(case (range "8.10" "8.16") "4.0.0")
|
||||
] null;
|
||||
release."5.2.1".sha256 = "sha256-3ExKHXIA8EnzAPzSbdB9FTN2OcLCVS5WtmrHOiN9UiQ=";
|
||||
release."5.2.0+20241009".sha256 = "sha256-eg47YgnIonCq7XOUgh9uzoKsuFCvsOSTZhgFLNNcPD0=";
|
||||
|
||||
@@ -11,16 +11,13 @@ mkCoqDerivation {
|
||||
owner = "DistributedComponents";
|
||||
inherit version;
|
||||
defaultVersion =
|
||||
let
|
||||
case = case: out: { inherit case out; };
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch coq.version [
|
||||
{
|
||||
case = range "8.9" "9.0";
|
||||
out = "20230107";
|
||||
}
|
||||
{
|
||||
case = range "8.5" "8.16";
|
||||
out = "20200131";
|
||||
}
|
||||
(case (range "8.9" "9.1") "20230107")
|
||||
(case (range "8.5" "8.16") "20200131")
|
||||
] null;
|
||||
release."20230107".rev = "601e89ec019501c48c27fcfc14b9a3c70456e408";
|
||||
release."20230107".sha256 = "sha256-YMBzVIsLkIC+w2TeyHrKe29eWLIxrH3wIMZqhik8p9I=";
|
||||
|
||||
@@ -13,16 +13,13 @@ let
|
||||
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.12" "9.0";
|
||||
out = "20240715";
|
||||
}
|
||||
{
|
||||
case = range "8.7" "8.11";
|
||||
out = "20200624";
|
||||
}
|
||||
(case (range "8.12" "9.1") "20240715")
|
||||
(case (range "8.7" "8.11") "20200624")
|
||||
] null;
|
||||
release = {
|
||||
"20240715".sha256 = "sha256-9CSxAIm0aEXkwF+aj8u/bqLG30y5eDNz65EnohJPjzI="; # coq 8.9 - 8.20
|
||||
|
||||
@@ -16,87 +16,29 @@ in
|
||||
owner = "QuickChick";
|
||||
inherit version;
|
||||
defaultVersion =
|
||||
let
|
||||
case = coq: mc: out: {
|
||||
cases = [
|
||||
coq
|
||||
mc
|
||||
];
|
||||
inherit out;
|
||||
};
|
||||
in
|
||||
lib.switch
|
||||
[ coq.coq-version mathcomp-boot.version ]
|
||||
[
|
||||
{
|
||||
cases = [
|
||||
(lib.versions.range "8.15" "9.0")
|
||||
lib.pred.true
|
||||
];
|
||||
out = "2.0.4";
|
||||
}
|
||||
{
|
||||
cases = [
|
||||
(lib.versions.range "8.13" "8.17")
|
||||
lib.pred.true
|
||||
];
|
||||
out = "1.6.5";
|
||||
}
|
||||
{
|
||||
cases = [
|
||||
"8.13"
|
||||
lib.pred.true
|
||||
];
|
||||
out = "1.5.0";
|
||||
}
|
||||
{
|
||||
cases = [
|
||||
"8.12"
|
||||
lib.pred.true
|
||||
];
|
||||
out = "1.4.0";
|
||||
}
|
||||
{
|
||||
cases = [
|
||||
"8.11"
|
||||
lib.pred.true
|
||||
];
|
||||
out = "1.3.2";
|
||||
}
|
||||
{
|
||||
cases = [
|
||||
"8.10"
|
||||
lib.pred.true
|
||||
];
|
||||
out = "1.2.1";
|
||||
}
|
||||
{
|
||||
cases = [
|
||||
"8.9"
|
||||
lib.pred.true
|
||||
];
|
||||
out = "1.1.0";
|
||||
}
|
||||
{
|
||||
cases = [
|
||||
"8.8"
|
||||
lib.pred.true
|
||||
];
|
||||
out = "20190311";
|
||||
}
|
||||
{
|
||||
cases = [
|
||||
"8.7"
|
||||
lib.versions.isLe
|
||||
"1.8"
|
||||
];
|
||||
out = "1.0.0";
|
||||
}
|
||||
{
|
||||
cases = [
|
||||
"8.6"
|
||||
lib.pred.true
|
||||
];
|
||||
out = "20171102";
|
||||
}
|
||||
{
|
||||
cases = [
|
||||
"8.5"
|
||||
lib.pred.true
|
||||
];
|
||||
out = "20170512";
|
||||
}
|
||||
(case (lib.versions.range "8.15" "9.0") lib.pred.true "2.0.4")
|
||||
(case (lib.versions.range "8.13" "8.17") lib.pred.true "1.6.5")
|
||||
(case "8.13" lib.pred.true "1.5.0")
|
||||
(case "8.12" lib.pred.true "1.4.0")
|
||||
(case "8.11" lib.pred.true "1.3.2")
|
||||
(case "8.10" lib.pred.true "1.2.1")
|
||||
(case "8.9" lib.pred.true "1.1.0")
|
||||
(case "8.8" lib.pred.true "20190311")
|
||||
(case "8.7" (lib.versions.isLe "1.8") "1.0.0")
|
||||
(case "8.6" lib.pred.true "20171102")
|
||||
(case "8.5" lib.pred.true "20170512")
|
||||
]
|
||||
null;
|
||||
release."2.0.4".sha256 = "sha256-WD8B+n8gyGctHMO+M8201Ca3Uw8zCWYsOatSNGCf0/s=";
|
||||
|
||||
@@ -11,20 +11,14 @@ mkCoqDerivation {
|
||||
owner = "uwplse";
|
||||
inherit version;
|
||||
defaultVersion =
|
||||
let
|
||||
case = case: out: { inherit case out; };
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch coq.coq-version [
|
||||
{
|
||||
case = range "8.9" "9.0";
|
||||
out = "20230107";
|
||||
}
|
||||
{
|
||||
case = range "8.6" "8.16";
|
||||
out = "20210328";
|
||||
}
|
||||
{
|
||||
case = range "8.5" "8.13";
|
||||
out = "20181102";
|
||||
}
|
||||
(case (range "8.9" "9.1") "20230107")
|
||||
(case (range "8.6" "8.16") "20210328")
|
||||
(case (range "8.5" "8.13") "20181102")
|
||||
] null;
|
||||
release."20230107".rev = "2f2ff253be29bb09f36cab96d036419b18a95b00";
|
||||
release."20230107".sha256 = "sha256-4mWdnWD8m1ddgqWHqzjqclhinXJaB/YoLlmLeeL0yZA=";
|
||||
|
||||
@@ -18,20 +18,14 @@ mkCoqDerivation {
|
||||
|
||||
inherit version;
|
||||
defaultVersion =
|
||||
let
|
||||
case = case: out: { inherit case out; };
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch coq.coq-version [
|
||||
{
|
||||
case = range "8.14" "9.0";
|
||||
out = "1.9";
|
||||
}
|
||||
{
|
||||
case = range "8.14" "8.18";
|
||||
out = "1.8";
|
||||
}
|
||||
{
|
||||
case = range "8.10" "8.13";
|
||||
out = "1.7";
|
||||
}
|
||||
(case (range "8.14" "9.1") "1.9")
|
||||
(case (range "8.14" "8.18") "1.8")
|
||||
(case (range "8.10" "8.13") "1.7")
|
||||
] null;
|
||||
|
||||
propagatedBuildInputs = [
|
||||
|
||||
@@ -2,6 +2,8 @@
|
||||
lib,
|
||||
mkCoqDerivation,
|
||||
coq,
|
||||
rocqPackages_9_0,
|
||||
rocqPackages_9_1,
|
||||
rocqPackages,
|
||||
stdlib,
|
||||
version ? null,
|
||||
@@ -60,16 +62,25 @@
|
||||
# this is just a wrapper for rocPackages.bignums for Rocq >= 9.0
|
||||
lib.optionalAttrs
|
||||
(coq.version != null && (coq.version == "dev" || lib.versions.isGe "9.0" coq.version))
|
||||
{
|
||||
configurePhase = ''
|
||||
echo no configuration
|
||||
'';
|
||||
buildPhase = ''
|
||||
echo building nothing
|
||||
'';
|
||||
installPhase = ''
|
||||
echo installing nothing
|
||||
'';
|
||||
propagatedBuildInputs = o.propagatedBuildInputs ++ [ rocqPackages.bignums ];
|
||||
}
|
||||
(
|
||||
let
|
||||
case = case: out: { inherit case out; };
|
||||
rp = lib.switch coq.coq-version [
|
||||
(case (lib.versions.isEq "9.0") rocqPackages_9_0)
|
||||
(case (lib.versions.isEq "9.1") rocqPackages_9_1)
|
||||
] rocqPackages;
|
||||
in
|
||||
{
|
||||
configurePhase = ''
|
||||
echo no configuration
|
||||
'';
|
||||
buildPhase = ''
|
||||
echo building nothing
|
||||
'';
|
||||
installPhase = ''
|
||||
echo installing nothing
|
||||
'';
|
||||
propagatedBuildInputs = o.propagatedBuildInputs ++ [ rp.bignums ];
|
||||
}
|
||||
)
|
||||
)
|
||||
|
||||
@@ -14,16 +14,13 @@ mkCoqDerivation {
|
||||
|
||||
inherit version;
|
||||
defaultVersion =
|
||||
let
|
||||
case = case: out: { inherit case out; };
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch coq.version [
|
||||
{
|
||||
case = range "8.14" "9.0";
|
||||
out = "0.4.1";
|
||||
}
|
||||
{
|
||||
case = range "8.8" "8.16";
|
||||
out = "0.4.0";
|
||||
}
|
||||
(case (range "8.14" "9.1") "0.4.1")
|
||||
(case (range "8.8" "8.16") "0.4.0")
|
||||
] null;
|
||||
release."0.4.1".sha256 = "sha256-9vyk8/8IVsqNyhw3WPzl8w3L9Wu7gfaMVa3n2nWjFiA=";
|
||||
release."0.4.0".sha256 = "sha256:0zwp3pn6fdj0qdig734zdczrls886al06mxqhhabms0jvvqijmbi";
|
||||
|
||||
@@ -3,6 +3,8 @@
|
||||
mkCoqDerivation,
|
||||
which,
|
||||
coq,
|
||||
rocqPackages_9_0,
|
||||
rocqPackages_9_1,
|
||||
rocqPackages,
|
||||
stdlib,
|
||||
version ? null,
|
||||
@@ -16,17 +18,18 @@ let
|
||||
else
|
||||
(
|
||||
let
|
||||
|
||||
case = case: out: { inherit case out; };
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch coq.coq-version [
|
||||
(case "8.11" "1.11.4")
|
||||
(case "8.12" "1.12.0")
|
||||
(case (range "8.13" "8.14") "1.13.7")
|
||||
(case "8.15" "1.15.0")
|
||||
(case (range "8.16" "8.17") "1.17.0")
|
||||
(case (range "8.20" "9.1") "2.0.7")
|
||||
(case (range "8.18" "8.19") "1.18.1")
|
||||
(case (range "8.20" "9.0") "2.0.7")
|
||||
(case (range "8.16" "8.17") "1.17.0")
|
||||
(case "8.15" "1.15.0")
|
||||
(case (range "8.13" "8.14") "1.13.7")
|
||||
(case "8.12" "1.12.0")
|
||||
(case "8.11" "1.11.4")
|
||||
] { }
|
||||
);
|
||||
elpi = coq.ocamlPackages.elpi.override { version = default-elpi-version; };
|
||||
@@ -44,6 +47,7 @@ let
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch coq.coq-version [
|
||||
(case (range "8.20" "9.1") "2.6.0")
|
||||
(case (range "8.20" "9.0") "2.5.2")
|
||||
(case "8.19" "2.0.1")
|
||||
(case "8.18" "2.0.0")
|
||||
@@ -55,6 +59,7 @@ let
|
||||
(case "8.12" "1.8.3_8.12")
|
||||
(case "8.11" "1.6.3_8.11")
|
||||
] null;
|
||||
release."2.6.0".sha256 = "sha256-23BHq1NFUkI3ayXnGUwiGFySLyY3EuH4RyMgAhQqI4g=";
|
||||
release."2.5.2".sha256 = "sha256-lLzjPrbVB3rrqox528YiheUb0u89R84Xmrgkn0oplOs=";
|
||||
release."2.5.0".sha256 = "sha256-Z5xjO83X/ZoTQlWnVupGXPH3HuJefr57Kv128I0dltg=";
|
||||
release."2.4.0".sha256 = "sha256-W2+vVGExLLux8e0nSZESSoMVvrLxhL6dmXkb+JuKiqc=";
|
||||
@@ -138,6 +143,13 @@ let
|
||||
o:
|
||||
# this is just a wrapper for rocPackages.rocq-elpi for Rocq >= 9.0
|
||||
if coq.version != null && (coq.version == "dev" || lib.versions.isGe "9.0" coq.version) then
|
||||
let
|
||||
case = case: out: { inherit case out; };
|
||||
rp = lib.switch coq.coq-version [
|
||||
(case "9.0" rocqPackages_9_0)
|
||||
(case "9.1" rocqPackages_9_1)
|
||||
] rocqPackages;
|
||||
in
|
||||
{
|
||||
configurePhase = ''
|
||||
echo no configuration
|
||||
@@ -148,7 +160,7 @@ let
|
||||
installPhase = ''
|
||||
echo installing nothing
|
||||
'';
|
||||
propagatedBuildInputs = o.propagatedBuildInputs ++ [ rocqPackages.rocq-elpi ];
|
||||
propagatedBuildInputs = o.propagatedBuildInputs ++ [ rp.rocq-elpi ];
|
||||
}
|
||||
else
|
||||
lib.optionalAttrs (o.version != null && (o.version == "dev" || lib.versions.isGe "2.5.0" o.version))
|
||||
|
||||
@@ -10,12 +10,12 @@ mkCoqDerivation {
|
||||
owner = "tchajed";
|
||||
inherit version;
|
||||
defaultVersion =
|
||||
let
|
||||
case = case: out: { inherit case out; };
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch coq.coq-version [
|
||||
{
|
||||
case = range "8.10" "9.0";
|
||||
out = "0.3.4";
|
||||
}
|
||||
(case (range "8.10" "9.0") "0.3.4")
|
||||
] null;
|
||||
release."0.3.4".sha256 = "sha256-AhEcugUiVIsgbq884Lur/bQIuGw8prk+3AlNkP1omcw=";
|
||||
release."0.3.3".sha256 = "sha256-HDIPeFHiC9EwhiOH7yMGJ9d2zJMhboTpRGf9kWcB9Io=";
|
||||
|
||||
@@ -30,7 +30,7 @@ let
|
||||
lib.switch
|
||||
[ coq.coq-version mathcomp.version ]
|
||||
[
|
||||
(case (range "8.20" "9.0") (isGe "2.3.0") "2.1.0")
|
||||
(case (range "8.20" "9.1") (isGe "2.3.0") "2.1.0")
|
||||
(case (range "8.16" "8.20") (isGe "2.1.0") "2.0.3")
|
||||
(case (range "8.16" "8.20") (isGe "2.0.0") "2.0.1")
|
||||
(case (range "8.16" "8.17") (isGe "2.0.0") "2.0.0")
|
||||
|
||||
@@ -26,7 +26,7 @@ mkCoqDerivation {
|
||||
lib.switch
|
||||
[ coq.coq-version ssreflect.version ]
|
||||
[
|
||||
(case (range "8.17" "9.0") (range "2.0.0" "2.4.0") "0.2.2")
|
||||
(case (range "8.17" "9.1") (range "2.0.0" "2.4.0") "0.2.2")
|
||||
(case (range "8.17" "9.0") (range "2.0.0" "2.3.0") "0.2.1")
|
||||
(case (range "8.17" "8.20") (range "2.0.0" "2.2.0") "0.2.0")
|
||||
(case (range "8.11" "8.20") (isLe "2.0.0") "0.1.1")
|
||||
|
||||
@@ -26,7 +26,7 @@
|
||||
lib.switch
|
||||
[ coq.coq-version mathcomp-boot.version ]
|
||||
[
|
||||
(case (range "8.17" "9.0") (range "2.0.0" "2.4.0") "0.5.0")
|
||||
(case (range "8.17" "9.1") (range "2.0.0" "2.4.0") "0.5.0")
|
||||
(case (range "8.17" "8.20") (range "2.0.0" "2.3.0") "0.4.0")
|
||||
(case (range "8.11" "8.20") (range "1.12.0" "1.19.0") "0.3.1")
|
||||
(case (range "8.11" "8.14") (isLe "1.12.0") "0.3.0")
|
||||
|
||||
@@ -35,7 +35,7 @@ mkCoqDerivation {
|
||||
lib.switch
|
||||
[ coq.coq-version mathcomp.version ]
|
||||
[
|
||||
(case (range "8.16" "9.0") (range "2.0" "2.4") "2.3")
|
||||
(case (range "8.16" "9.1") (range "2.0" "2.4") "2.3")
|
||||
(case (range "8.16" "9.0") (range "2.0" "2.3") "2.2")
|
||||
(case (range "8.10" "8.18") (range "1.12.0" "1.18.0") "1.17")
|
||||
(case (range "8.10" "8.12") "1.11.0" "1.11")
|
||||
|
||||
@@ -2,6 +2,8 @@
|
||||
lib,
|
||||
mkCoqDerivation,
|
||||
coq,
|
||||
rocqPackages_9_0,
|
||||
rocqPackages_9_1,
|
||||
rocqPackages,
|
||||
stdlib,
|
||||
coq-elpi,
|
||||
@@ -19,7 +21,7 @@ let
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch coq.coq-version [
|
||||
(case (range "8.20" "9.0") "1.9.1")
|
||||
(case (range "8.20" "9.1") "1.9.1")
|
||||
(case (range "8.19" "8.20") "1.8.0")
|
||||
(case (range "8.18" "8.20") "1.7.1")
|
||||
(case (range "8.16" "8.18") "1.6.0")
|
||||
@@ -77,16 +79,25 @@ hb.overrideAttrs (
|
||||
//
|
||||
lib.optionalAttrs
|
||||
(coq.version != null && (coq.version == "dev" || lib.versions.isGe "9.0" coq.version))
|
||||
{
|
||||
configurePhase = ''
|
||||
echo no configuration
|
||||
'';
|
||||
buildPhase = ''
|
||||
echo building nothing
|
||||
'';
|
||||
installPhase = ''
|
||||
echo installing nothing
|
||||
'';
|
||||
propagatedBuildInputs = o.propagatedBuildInputs ++ [ rocqPackages.hierarchy-builder ];
|
||||
}
|
||||
(
|
||||
let
|
||||
case = case: out: { inherit case out; };
|
||||
rp = lib.switch coq.coq-version [
|
||||
(case "9.0" rocqPackages_9_0)
|
||||
(case "9.1" rocqPackages_9_1)
|
||||
] rocqPackages;
|
||||
in
|
||||
{
|
||||
configurePhase = ''
|
||||
echo no configuration
|
||||
'';
|
||||
buildPhase = ''
|
||||
echo building nothing
|
||||
'';
|
||||
installPhase = ''
|
||||
echo installing nothing
|
||||
'';
|
||||
propagatedBuildInputs = o.propagatedBuildInputs ++ [ rp.hierarchy-builder ];
|
||||
}
|
||||
)
|
||||
)
|
||||
|
||||
@@ -17,7 +17,7 @@ mkCoqDerivation {
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch coq.coq-version [
|
||||
(case (range "8.19" "9.0") "4.3.0")
|
||||
(case (range "8.19" "9.1") "4.3.0")
|
||||
(case (range "8.18" "8.19") "4.2.0")
|
||||
(case (range "8.16" "8.18") "4.1.0")
|
||||
(case (range "8.13" "8.17") "4.0.0")
|
||||
|
||||
@@ -19,7 +19,7 @@
|
||||
inherit (lib.versions) range;
|
||||
in
|
||||
lib.switch coq.coq-version [
|
||||
(case (range "8.14" "9.0") "0.2.0")
|
||||
(case (range "8.14" "9.1") "0.2.0")
|
||||
(case (range "8.14" "8.20") "0.1.3")
|
||||
] null;
|
||||
release = {
|
||||
|
||||
@@ -32,7 +32,7 @@ mkCoqDerivation {
|
||||
lib.switch
|
||||
[ coq.coq-version mathcomp-algebra.version ]
|
||||
[
|
||||
(case (range "8.20" "9.0") (isGe "2.4") "1.2.5")
|
||||
(case (range "8.20" "9.1") (isGe "2.4") "1.2.5")
|
||||
(case (range "8.16" "9.0") (isGe "2.0") "1.2.4")
|
||||
(case (range "8.16" "8.18") (isGe "2.0") "1.2.2")
|
||||
(case (range "8.16" "8.19") (isGe "1.15") "1.1.1")
|
||||
|
||||
@@ -58,7 +58,7 @@ let
|
||||
lib.switch
|
||||
[ coq.coq-version mathcomp.version ]
|
||||
[
|
||||
(case (range "8.20" "9.0") (range "2.1.0" "2.4.0") "1.12.0")
|
||||
(case (range "8.20" "9.1") (range "2.1.0" "2.4.0") "1.12.0")
|
||||
(case (range "8.19" "8.20") (range "2.1.0" "2.3.0") "1.9.0")
|
||||
(case (range "8.17" "8.20") (range "2.0.0" "2.2.0") "1.1.0")
|
||||
(case (range "8.17" "8.19") (range "1.17.0" "1.19.0") "0.7.0")
|
||||
|
||||
@@ -27,7 +27,7 @@ mkCoqDerivation {
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch coq.coq-version [
|
||||
(case (range "8.10" "9.0") "1.0.2")
|
||||
(case (range "8.10" "9.1") "1.0.2")
|
||||
(case (range "8.5" "8.14") "1.0.0")
|
||||
] null;
|
||||
|
||||
|
||||
@@ -29,7 +29,7 @@ mkCoqDerivation {
|
||||
lib.switch
|
||||
[ coq.coq-version mathcomp-boot.version ]
|
||||
[
|
||||
(case (range "8.20" "9.0") (range "2.3" "2.4") "2.2.0")
|
||||
(case (range "8.20" "9.1") (range "2.3" "2.4") "2.2.0")
|
||||
(case (range "8.16" "9.0") (range "2.0" "2.3") "2.1.0")
|
||||
(case (range "8.16" "8.18") (range "2.0" "2.1") "2.0.0")
|
||||
(case (range "8.13" "8.20") (range "1.12" "1.19") "1.5.2")
|
||||
|
||||
@@ -32,87 +32,30 @@ mkCoqDerivation {
|
||||
};
|
||||
|
||||
defaultVersion =
|
||||
let
|
||||
case = coq: mc: out: {
|
||||
cases = [
|
||||
coq
|
||||
mc
|
||||
];
|
||||
inherit out;
|
||||
};
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch
|
||||
[ coq.version mathcomp.version ]
|
||||
[
|
||||
{
|
||||
cases = [
|
||||
(range "8.18" "9.0")
|
||||
(isGe "2.2.0")
|
||||
];
|
||||
out = "2.0.3";
|
||||
}
|
||||
{
|
||||
cases = [
|
||||
(range "8.17" "9.0")
|
||||
(range "2.1.0" "2.3.0")
|
||||
];
|
||||
out = "2.0.2";
|
||||
}
|
||||
{
|
||||
cases = [
|
||||
(range "8.17" "8.20")
|
||||
(range "2.0.0" "2.2.0")
|
||||
];
|
||||
out = "2.0.1";
|
||||
}
|
||||
{
|
||||
cases = [
|
||||
(range "8.16" "8.19")
|
||||
(range "2.0.0" "2.2.0")
|
||||
];
|
||||
out = "2.0.0";
|
||||
}
|
||||
{
|
||||
cases = [
|
||||
(range "8.13" "8.19")
|
||||
(range "1.13.0" "1.19.0")
|
||||
];
|
||||
out = "1.1.4";
|
||||
}
|
||||
{
|
||||
cases = [
|
||||
(isGe "8.13")
|
||||
(range "1.12.0" "1.18.0")
|
||||
];
|
||||
out = "1.1.3";
|
||||
}
|
||||
{
|
||||
cases = [
|
||||
(isGe "8.10")
|
||||
(range "1.12.0" "1.18.0")
|
||||
];
|
||||
out = "1.1.2";
|
||||
}
|
||||
{
|
||||
cases = [
|
||||
(isGe "8.7")
|
||||
"1.11.0"
|
||||
];
|
||||
out = "1.1.1";
|
||||
}
|
||||
{
|
||||
cases = [
|
||||
(isGe "8.7")
|
||||
(range "1.9.0" "1.10.0")
|
||||
];
|
||||
out = "1.0.4";
|
||||
}
|
||||
{
|
||||
cases = [
|
||||
(isGe "8.7")
|
||||
"1.8.0"
|
||||
];
|
||||
out = "1.0.3";
|
||||
}
|
||||
{
|
||||
cases = [
|
||||
(isGe "8.7")
|
||||
"1.7.0"
|
||||
];
|
||||
out = "1.0.1";
|
||||
}
|
||||
(case (range "8.18" "9.1") (isGe "2.2.0") "2.0.3")
|
||||
(case (range "8.17" "9.0") (range "2.1.0" "2.3.0") "2.0.2")
|
||||
(case (range "8.17" "8.20") (range "2.0.0" "2.2.0") "2.0.1")
|
||||
(case (range "8.16" "8.19") (range "2.0.0" "2.2.0") "2.0.0")
|
||||
(case (range "8.13" "8.19") (range "1.13.0" "1.19.0") "1.1.4")
|
||||
(case (isGe "8.13") (range "1.12.0" "1.18.0") "1.1.3")
|
||||
(case (isGe "8.10") (range "1.12.0" "1.18.0") "1.1.2")
|
||||
(case (isGe "8.7") "1.11.0" "1.1.1")
|
||||
(case (isGe "8.7") (range "1.9.0" "1.10.0") "1.0.4")
|
||||
(case (isGe "8.7") "1.8.0" "1.0.3")
|
||||
(case (isGe "8.7") "1.7.0" "1.0.1")
|
||||
]
|
||||
null;
|
||||
|
||||
|
||||
@@ -31,7 +31,7 @@ mkCoqDerivation {
|
||||
lib.switch
|
||||
[ coq.coq-version mathcomp-ssreflect.version ]
|
||||
[
|
||||
(case (range "8.16" "9.0") (range "2.0.0" "2.4.0") "1.0.3")
|
||||
(case (range "8.16" "9.1") (range "2.0.0" "2.4.0") "1.0.3")
|
||||
(case (range "8.16" "9.0") (range "2.0.0" "2.3.0") "1.0.2")
|
||||
(case (range "8.12" "8.18") (range "1.12.0" "1.17.0") "1.0.1")
|
||||
(case (range "8.10" "8.16") (range "1.12.0" "1.17.0") "1.0.0")
|
||||
|
||||
@@ -69,7 +69,7 @@ mkCoqDerivation {
|
||||
lib.switch
|
||||
[ coq.coq-version mathcomp.version ]
|
||||
[
|
||||
(case (range "8.16" "9.0") (isGe "2.0") "3.2")
|
||||
(case (range "8.16" "9.1") (isGe "2.0") "3.2")
|
||||
(case (range "8.12" "8.20") (range "1.12" "1.19") "2.4")
|
||||
]
|
||||
null;
|
||||
|
||||
@@ -33,7 +33,7 @@ mkCoqDerivation {
|
||||
lib.switch
|
||||
[ coq.coq-version mathcomp-algebra.version ]
|
||||
[
|
||||
(case (range "8.16" "9.0") (isGe "2.0.0") "1.5.0+2.0+8.16")
|
||||
(case (range "8.16" "9.1") (isGe "2.0.0") "1.5.0+2.0+8.16")
|
||||
(case (range "8.13" "8.20") (range "1.12" "1.19.0") "1.3.0+1.12+8.13")
|
||||
(case (range "8.13" "8.16") (range "1.12" "1.17.0") "1.1.0+1.12+8.13")
|
||||
]
|
||||
|
||||
@@ -35,7 +35,7 @@ let
|
||||
inherit (lib.versions) range;
|
||||
in
|
||||
lib.switch coq.coq-version [
|
||||
(case (range "8.20" "9.0") "2.4.0")
|
||||
(case (range "8.20" "9.1") "2.4.0")
|
||||
(case (range "8.19" "9.0") "2.3.0")
|
||||
(case (range "8.17" "8.20") "2.2.0")
|
||||
(case (range "8.17" "8.18") "2.1.0")
|
||||
|
||||
@@ -33,7 +33,7 @@ mkCoqDerivation {
|
||||
lib.switch
|
||||
[ coq.coq-version mathcomp.version ]
|
||||
[
|
||||
(case (range "8.18" "9.0") (range "2.1.0" "2.4.0") "2.4.0")
|
||||
(case (range "8.18" "9.1") (range "2.1.0" "2.4.0") "2.4.0")
|
||||
(case (range "8.17" "9.0") (range "2.1.0" "2.3.0") "2.3.0")
|
||||
(case (range "8.17" "8.20") (isGe "2.1.0") "2.2.0")
|
||||
(case (range "8.16" "8.18") "2.1.0" "2.1.0")
|
||||
|
||||
@@ -11,32 +11,17 @@ mkCoqDerivation {
|
||||
owner = "snu-sf";
|
||||
inherit version;
|
||||
defaultVersion =
|
||||
let
|
||||
case = case: out: { inherit case out; };
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch coq.coq-version [
|
||||
{
|
||||
case = range "8.14" "9.0";
|
||||
out = "4.2.3";
|
||||
}
|
||||
{
|
||||
case = isEq "8.13";
|
||||
out = "4.2.2";
|
||||
}
|
||||
{
|
||||
case = range "8.12" "8.17";
|
||||
out = "4.1.2";
|
||||
}
|
||||
{
|
||||
case = range "8.9" "8.13";
|
||||
out = "4.1.1";
|
||||
}
|
||||
{
|
||||
case = range "8.6" "8.13";
|
||||
out = "4.0.2";
|
||||
}
|
||||
{
|
||||
case = isEq "8.5";
|
||||
out = "1.2.8";
|
||||
}
|
||||
(case (range "8.14" "9.1") "4.2.3")
|
||||
(case (isEq "8.13") "4.2.2")
|
||||
(case (range "8.12" "8.17") "4.1.2")
|
||||
(case (range "8.9" "8.13") "4.1.1")
|
||||
(case (range "8.6" "8.13") "4.0.2")
|
||||
(case (isEq "8.5") "1.2.8")
|
||||
] null;
|
||||
release."4.2.3".sha256 = "sha256-ldUjNd5daUu2B3v4tk20/iXFgyUuW4XHlbubTInpwcs=";
|
||||
release."4.2.2".sha256 = "sha256-qr6o45Q90FK+kkBUJ+W7QhiA0YQRb1RUwwXUpTTFt8A=";
|
||||
|
||||
@@ -21,24 +21,15 @@ mkCoqDerivation {
|
||||
|
||||
inherit version;
|
||||
defaultVersion =
|
||||
let
|
||||
case = case: out: { inherit case out; };
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch coq.version [
|
||||
{
|
||||
case = range "8.14" "9.0";
|
||||
out = "0.2.0";
|
||||
}
|
||||
{
|
||||
case = range "8.14" "8.20";
|
||||
out = "0.1.2";
|
||||
}
|
||||
{
|
||||
case = range "8.12" "8.16";
|
||||
out = "0.1.1";
|
||||
}
|
||||
{
|
||||
case = range "8.12" "8.13";
|
||||
out = "0.1.0";
|
||||
}
|
||||
(case (range "8.14" "9.1") "0.2.0")
|
||||
(case (range "8.14" "8.20") "0.1.2")
|
||||
(case (range "8.12" "8.16") "0.1.1")
|
||||
(case (range "8.12" "8.13") "0.1.0")
|
||||
] null;
|
||||
release."0.2.0".sha256 = "sha256-hM6LVFQ2VQ42QeHu8Ex+oz1VvJUr+g8/nZN+bYHEljQ=";
|
||||
release."0.1.2".sha256 = "sha256-QN0h1CsX86DQBDsluXLtNUvMh3r60/0iDSbYam67AhA=";
|
||||
|
||||
@@ -1,6 +1,8 @@
|
||||
{
|
||||
lib,
|
||||
mkCoqDerivation,
|
||||
rocqPackages_9_0,
|
||||
rocqPackages_9_1,
|
||||
rocqPackages,
|
||||
which,
|
||||
coq,
|
||||
@@ -41,16 +43,25 @@ with lib;
|
||||
# this is just a wrapper for rocPackages.parseque for Rocq >= 9.0
|
||||
lib.optionalAttrs
|
||||
(coq.version != null && (coq.version == "dev" || lib.versions.isGe "9.0" coq.version))
|
||||
{
|
||||
configurePhase = ''
|
||||
echo no configuration
|
||||
'';
|
||||
buildPhase = ''
|
||||
echo building nothing
|
||||
'';
|
||||
installPhase = ''
|
||||
echo installing nothing
|
||||
'';
|
||||
propagatedBuildInputs = [ rocqPackages.parseque ];
|
||||
}
|
||||
(
|
||||
let
|
||||
case = case: out: { inherit case out; };
|
||||
rp = lib.switch coq.coq-version [
|
||||
(case "9.0" rocqPackages_9_0)
|
||||
(case "9.1" rocqPackages_9_1)
|
||||
] rocqPackages;
|
||||
in
|
||||
{
|
||||
configurePhase = ''
|
||||
echo no configuration
|
||||
'';
|
||||
buildPhase = ''
|
||||
echo building nothing
|
||||
'';
|
||||
installPhase = ''
|
||||
echo installing nothing
|
||||
'';
|
||||
propagatedBuildInputs = [ rp.parseque ];
|
||||
}
|
||||
)
|
||||
)
|
||||
|
||||
@@ -33,7 +33,7 @@ mkCoqDerivation {
|
||||
lib.switch
|
||||
[ coq.coq-version mathcomp.version ]
|
||||
[
|
||||
(case (range "8.16" "9.0") (range "2.0.0" "2.4.0") "1.2.2")
|
||||
(case (range "8.16" "9.1") (range "2.0.0" "2.4.0") "1.2.2")
|
||||
(case (range "8.16" "9.0") (range "2.0.0" "2.3.0") "1.2.1")
|
||||
(case (range "8.16" "8.18") (range "2.0.0" "2.1.0") "1.2.0")
|
||||
(case (range "8.10" "8.20") (isLt "2.0.0") "1.1.3")
|
||||
|
||||
@@ -18,7 +18,7 @@
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch coq.coq-version [
|
||||
(case (range "8.17" "9.0") "1.10.0")
|
||||
(case (range "8.17" "9.1") "1.10.0")
|
||||
(case (range "8.11" "8.19") "1.8.0")
|
||||
(case (range "8.7" "8.13") "1.3.0")
|
||||
] null;
|
||||
|
||||
@@ -1,5 +1,7 @@
|
||||
{
|
||||
coq,
|
||||
rocqPackages_9_0,
|
||||
rocqPackages_9_1,
|
||||
rocqPackages,
|
||||
mkCoqDerivation,
|
||||
lib,
|
||||
@@ -52,5 +54,14 @@
|
||||
'';
|
||||
}
|
||||
else
|
||||
{ propagatedBuildInputs = [ rocqPackages.stdlib ]; }
|
||||
let
|
||||
case = case: out: { inherit case out; };
|
||||
rp = lib.switch coq.coq-version [
|
||||
(case "9.0" rocqPackages_9_0)
|
||||
(case "9.1" rocqPackages_9_1)
|
||||
] rocqPackages;
|
||||
in
|
||||
{
|
||||
propagatedBuildInputs = [ rp.stdlib ];
|
||||
}
|
||||
)
|
||||
|
||||
@@ -17,7 +17,7 @@ mkCoqDerivation {
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch coq.coq-version [
|
||||
(case (range "8.19" "9.0") "1.11.0")
|
||||
(case (range "8.19" "9.1") "1.11.0")
|
||||
(case (range "8.18" "8.19") "1.10.0")
|
||||
(case (range "8.16" "8.18") "1.9.0")
|
||||
(case (range "8.13" "8.17") "1.8.0")
|
||||
|
||||
@@ -17,7 +17,7 @@ let
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch rocq-core.rocq-version [
|
||||
(case (range "9.0" "9.0") "1.9.1")
|
||||
(case (range "9.0" "9.1") "1.9.1")
|
||||
] null;
|
||||
release."1.9.1".sha256 = "sha256-AiS0ezMyfIYlXnuNsVLz1GlKQZzJX+ilkrKkbo0GrF0=";
|
||||
releaseRev = v: "v${v}";
|
||||
|
||||
@@ -15,8 +15,9 @@ let
|
||||
let
|
||||
case = case: out: { inherit case out; };
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch rocq-core.rocq-version [
|
||||
(case ("9.0") "2.0.7")
|
||||
(case (range "9.0" "9.1") "2.0.7")
|
||||
] { };
|
||||
elpi = rocq-core.ocamlPackages.elpi.override { version = default-elpi-version; };
|
||||
propagatedBuildInputs_wo_elpi = [
|
||||
@@ -32,9 +33,12 @@ let
|
||||
let
|
||||
case = case: out: { inherit case out; };
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch rocq-core.rocq-version [
|
||||
(case (range "9.0" "9.1") "2.6.0")
|
||||
(case ("9.0") "2.5.2")
|
||||
] null;
|
||||
release."2.6.0".sha256 = "sha256-23BHq1NFUkI3ayXnGUwiGFySLyY3EuH4RyMgAhQqI4g=";
|
||||
release."2.5.2".sha256 = "sha256-lLzjPrbVB3rrqox528YiheUb0u89R84Xmrgkn0oplOs=";
|
||||
releaseRev = v: "v${v}";
|
||||
|
||||
|
||||
Reference in New Issue
Block a user