coqPackages: New expressions: StructTact, InfSeqExt, Cheerios, Verdi
This commit is contained in:
parent
461c9d783c
commit
a370bd1fed
52
pkgs/development/coq-modules/Cheerios/default.nix
Normal file
52
pkgs/development/coq-modules/Cheerios/default.nix
Normal file
@ -0,0 +1,52 @@
|
|||||||
|
{ stdenv, fetchFromGitHub, coq, StructTact }:
|
||||||
|
|
||||||
|
let params =
|
||||||
|
{
|
||||||
|
"8.6" = {
|
||||||
|
version = "20181102";
|
||||||
|
rev = "04da309304bdd28a1f7dacca9fdf8696204a4ff2";
|
||||||
|
sha256 = "1xfa78p70c90favds1mv1vj5sr9bv0ad3dsgg05v3v72006g2f1q";
|
||||||
|
};
|
||||||
|
|
||||||
|
"8.7" = {
|
||||||
|
version = "20181102";
|
||||||
|
rev = "04da309304bdd28a1f7dacca9fdf8696204a4ff2";
|
||||||
|
sha256 = "1xfa78p70c90favds1mv1vj5sr9bv0ad3dsgg05v3v72006g2f1q";
|
||||||
|
};
|
||||||
|
|
||||||
|
"8.8" = {
|
||||||
|
version = "20181102";
|
||||||
|
rev = "04da309304bdd28a1f7dacca9fdf8696204a4ff2";
|
||||||
|
sha256 = "1xfa78p70c90favds1mv1vj5sr9bv0ad3dsgg05v3v72006g2f1q";
|
||||||
|
};
|
||||||
|
|
||||||
|
"8.9" = {
|
||||||
|
version = "20181102";
|
||||||
|
rev = "04da309304bdd28a1f7dacca9fdf8696204a4ff2";
|
||||||
|
sha256 = "1xfa78p70c90favds1mv1vj5sr9bv0ad3dsgg05v3v72006g2f1q";
|
||||||
|
};
|
||||||
|
};
|
||||||
|
param = params."${coq.coq-version}";
|
||||||
|
in
|
||||||
|
|
||||||
|
stdenv.mkDerivation rec {
|
||||||
|
name = "coq${coq.coq-version}-Cheerios-${param.version}";
|
||||||
|
|
||||||
|
src = fetchFromGitHub {
|
||||||
|
owner = "uwplse";
|
||||||
|
repo = "cheerios";
|
||||||
|
inherit (param) rev sha256;
|
||||||
|
};
|
||||||
|
|
||||||
|
buildInputs = [
|
||||||
|
coq coq.ocaml coq.camlp5 coq.findlib StructTact
|
||||||
|
];
|
||||||
|
enableParallelBuilding = true;
|
||||||
|
|
||||||
|
buildPhase = "make -j$NIX_BUILD_CORES";
|
||||||
|
installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
|
||||||
|
|
||||||
|
passthru = {
|
||||||
|
compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" "8.9" ];
|
||||||
|
};
|
||||||
|
}
|
58
pkgs/development/coq-modules/InfSeqExt/default.nix
Normal file
58
pkgs/development/coq-modules/InfSeqExt/default.nix
Normal file
@ -0,0 +1,58 @@
|
|||||||
|
{ stdenv, fetchFromGitHub, coq, mathcomp }:
|
||||||
|
|
||||||
|
let params =
|
||||||
|
{
|
||||||
|
"8.5" = {
|
||||||
|
version = "20180918";
|
||||||
|
rev = "243d6be45666da73a9da6c37d451327165275798";
|
||||||
|
sha256 = "1nh2psb4pcppy1akk24ilb4p08m35cba357i4xyymmarmbwqpxmn";
|
||||||
|
};
|
||||||
|
|
||||||
|
"8.6" = {
|
||||||
|
version = "20180918";
|
||||||
|
rev = "243d6be45666da73a9da6c37d451327165275798";
|
||||||
|
sha256 = "1nh2psb4pcppy1akk24ilb4p08m35cba357i4xyymmarmbwqpxmn";
|
||||||
|
};
|
||||||
|
|
||||||
|
"8.7" = {
|
||||||
|
version = "20180918";
|
||||||
|
rev = "243d6be45666da73a9da6c37d451327165275798";
|
||||||
|
sha256 = "1nh2psb4pcppy1akk24ilb4p08m35cba357i4xyymmarmbwqpxmn";
|
||||||
|
};
|
||||||
|
|
||||||
|
"8.8" = {
|
||||||
|
version = "20180918";
|
||||||
|
rev = "243d6be45666da73a9da6c37d451327165275798";
|
||||||
|
sha256 = "1nh2psb4pcppy1akk24ilb4p08m35cba357i4xyymmarmbwqpxmn";
|
||||||
|
};
|
||||||
|
|
||||||
|
"8.9" = {
|
||||||
|
version = "20180918";
|
||||||
|
rev = "243d6be45666da73a9da6c37d451327165275798";
|
||||||
|
sha256 = "1nh2psb4pcppy1akk24ilb4p08m35cba357i4xyymmarmbwqpxmn";
|
||||||
|
};
|
||||||
|
};
|
||||||
|
param = params."${coq.coq-version}";
|
||||||
|
in
|
||||||
|
|
||||||
|
stdenv.mkDerivation rec {
|
||||||
|
name = "coq${coq.coq-version}-InfSeqExt-${param.version}";
|
||||||
|
|
||||||
|
src = fetchFromGitHub {
|
||||||
|
owner = "DistributedComponents";
|
||||||
|
repo = "InfSeqExt";
|
||||||
|
inherit (param) rev sha256;
|
||||||
|
};
|
||||||
|
|
||||||
|
buildInputs = [
|
||||||
|
coq coq.ocaml coq.camlp5 coq.findlib mathcomp
|
||||||
|
];
|
||||||
|
enableParallelBuilding = true;
|
||||||
|
|
||||||
|
buildPhase = "make -j$NIX_BUILD_CORES";
|
||||||
|
installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
|
||||||
|
|
||||||
|
passthru = {
|
||||||
|
compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" "8.8" "8.9" ];
|
||||||
|
};
|
||||||
|
}
|
58
pkgs/development/coq-modules/StructTact/default.nix
Normal file
58
pkgs/development/coq-modules/StructTact/default.nix
Normal file
@ -0,0 +1,58 @@
|
|||||||
|
{ stdenv, fetchFromGitHub, coq, mathcomp }:
|
||||||
|
|
||||||
|
let params =
|
||||||
|
{
|
||||||
|
"8.5" = {
|
||||||
|
version = "20181102";
|
||||||
|
rev = "82a85b7ec07e71fa6b30cfc05f6a7bfb09ef2510";
|
||||||
|
sha256 = "08zry20flgj7qq37xk32kzmg4fg6d4wi9m7pf9aph8fd3j2a0b5v";
|
||||||
|
};
|
||||||
|
|
||||||
|
"8.6" = {
|
||||||
|
version = "20181102";
|
||||||
|
rev = "82a85b7ec07e71fa6b30cfc05f6a7bfb09ef2510";
|
||||||
|
sha256 = "08zry20flgj7qq37xk32kzmg4fg6d4wi9m7pf9aph8fd3j2a0b5v";
|
||||||
|
};
|
||||||
|
|
||||||
|
"8.7" = {
|
||||||
|
version = "20181102";
|
||||||
|
rev = "82a85b7ec07e71fa6b30cfc05f6a7bfb09ef2510";
|
||||||
|
sha256 = "08zry20flgj7qq37xk32kzmg4fg6d4wi9m7pf9aph8fd3j2a0b5v";
|
||||||
|
};
|
||||||
|
|
||||||
|
"8.8" = {
|
||||||
|
version = "20181102";
|
||||||
|
rev = "82a85b7ec07e71fa6b30cfc05f6a7bfb09ef2510";
|
||||||
|
sha256 = "08zry20flgj7qq37xk32kzmg4fg6d4wi9m7pf9aph8fd3j2a0b5v";
|
||||||
|
};
|
||||||
|
|
||||||
|
"8.9" = {
|
||||||
|
version = "20181102";
|
||||||
|
rev = "82a85b7ec07e71fa6b30cfc05f6a7bfb09ef2510";
|
||||||
|
sha256 = "08zry20flgj7qq37xk32kzmg4fg6d4wi9m7pf9aph8fd3j2a0b5v";
|
||||||
|
};
|
||||||
|
};
|
||||||
|
param = params."${coq.coq-version}";
|
||||||
|
in
|
||||||
|
|
||||||
|
stdenv.mkDerivation rec {
|
||||||
|
name = "coq${coq.coq-version}-StructTact-${param.version}";
|
||||||
|
|
||||||
|
src = fetchFromGitHub {
|
||||||
|
owner = "uwplse";
|
||||||
|
repo = "StructTact";
|
||||||
|
inherit (param) rev sha256;
|
||||||
|
};
|
||||||
|
|
||||||
|
buildInputs = [
|
||||||
|
coq coq.ocaml coq.camlp5 coq.findlib
|
||||||
|
];
|
||||||
|
enableParallelBuilding = true;
|
||||||
|
|
||||||
|
buildPhase = "make -j$NIX_BUILD_CORES";
|
||||||
|
installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
|
||||||
|
|
||||||
|
passthru = {
|
||||||
|
compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" "8.8" "8.9" ];
|
||||||
|
};
|
||||||
|
}
|
52
pkgs/development/coq-modules/Verdi/default.nix
Normal file
52
pkgs/development/coq-modules/Verdi/default.nix
Normal file
@ -0,0 +1,52 @@
|
|||||||
|
{ stdenv, fetchFromGitHub, coq, mathcomp, StructTact, InfSeqExt, Cheerios }:
|
||||||
|
|
||||||
|
let params =
|
||||||
|
{
|
||||||
|
"8.6" = {
|
||||||
|
version = "20181102";
|
||||||
|
rev = "25b79cf1be5527ab8dc1b8314fcee93e76a2e564";
|
||||||
|
sha256 = "1vw47c37k5vaa8vbr6ryqy8riagngwcrfmb3rai37yi9xhdqg55z";
|
||||||
|
};
|
||||||
|
|
||||||
|
"8.7" = {
|
||||||
|
version = "20181102";
|
||||||
|
rev = "25b79cf1be5527ab8dc1b8314fcee93e76a2e564";
|
||||||
|
sha256 = "1vw47c37k5vaa8vbr6ryqy8riagngwcrfmb3rai37yi9xhdqg55z";
|
||||||
|
};
|
||||||
|
|
||||||
|
"8.8" = {
|
||||||
|
version = "20181102";
|
||||||
|
rev = "25b79cf1be5527ab8dc1b8314fcee93e76a2e564";
|
||||||
|
sha256 = "1vw47c37k5vaa8vbr6ryqy8riagngwcrfmb3rai37yi9xhdqg55z";
|
||||||
|
};
|
||||||
|
|
||||||
|
"8.9" = {
|
||||||
|
version = "20181102";
|
||||||
|
rev = "25b79cf1be5527ab8dc1b8314fcee93e76a2e564";
|
||||||
|
sha256 = "1vw47c37k5vaa8vbr6ryqy8riagngwcrfmb3rai37yi9xhdqg55z";
|
||||||
|
};
|
||||||
|
};
|
||||||
|
param = params."${coq.coq-version}";
|
||||||
|
in
|
||||||
|
|
||||||
|
stdenv.mkDerivation rec {
|
||||||
|
name = "coq${coq.coq-version}-verdi-${param.version}";
|
||||||
|
|
||||||
|
src = fetchFromGitHub {
|
||||||
|
owner = "uwplse";
|
||||||
|
repo = "verdi";
|
||||||
|
inherit (param) rev sha256;
|
||||||
|
};
|
||||||
|
|
||||||
|
buildInputs = [
|
||||||
|
coq coq.ocaml coq.camlp5 coq.findlib mathcomp StructTact InfSeqExt Cheerios
|
||||||
|
];
|
||||||
|
enableParallelBuilding = true;
|
||||||
|
|
||||||
|
buildPhase = "make -j$NIX_BUILD_CORES";
|
||||||
|
installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
|
||||||
|
|
||||||
|
passthru = {
|
||||||
|
compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" "8.9" ];
|
||||||
|
};
|
||||||
|
}
|
@ -14,6 +14,7 @@ let
|
|||||||
then callPackage ../development/coq-modules/bignums {}
|
then callPackage ../development/coq-modules/bignums {}
|
||||||
else null;
|
else null;
|
||||||
category-theory = callPackage ../development/coq-modules/category-theory { };
|
category-theory = callPackage ../development/coq-modules/category-theory { };
|
||||||
|
Cheerios = callPackage ../development/coq-modules/Cheerios {};
|
||||||
CoLoR = callPackage ../development/coq-modules/CoLoR {};
|
CoLoR = callPackage ../development/coq-modules/CoLoR {};
|
||||||
coq-ext-lib = callPackage ../development/coq-modules/coq-ext-lib {};
|
coq-ext-lib = callPackage ../development/coq-modules/coq-ext-lib {};
|
||||||
coq-haskell = callPackage ../development/coq-modules/coq-haskell { };
|
coq-haskell = callPackage ../development/coq-modules/coq-haskell { };
|
||||||
@ -26,6 +27,7 @@ let
|
|||||||
heq = callPackage ../development/coq-modules/heq {};
|
heq = callPackage ../development/coq-modules/heq {};
|
||||||
HoTT = callPackage ../development/coq-modules/HoTT {};
|
HoTT = callPackage ../development/coq-modules/HoTT {};
|
||||||
interval = callPackage ../development/coq-modules/interval {};
|
interval = callPackage ../development/coq-modules/interval {};
|
||||||
|
InfSeqExt = callPackage ../development/coq-modules/InfSeqExt {};
|
||||||
iris = callPackage ../development/coq-modules/iris {};
|
iris = callPackage ../development/coq-modules/iris {};
|
||||||
math-classes = callPackage ../development/coq-modules/math-classes { };
|
math-classes = callPackage ../development/coq-modules/math-classes { };
|
||||||
mathcomp = callPackage ../development/coq-modules/mathcomp { };
|
mathcomp = callPackage ../development/coq-modules/mathcomp { };
|
||||||
@ -35,8 +37,10 @@ let
|
|||||||
QuickChick = callPackage ../development/coq-modules/QuickChick {};
|
QuickChick = callPackage ../development/coq-modules/QuickChick {};
|
||||||
ssreflect = callPackage ../development/coq-modules/ssreflect { };
|
ssreflect = callPackage ../development/coq-modules/ssreflect { };
|
||||||
stdpp = callPackage ../development/coq-modules/stdpp { };
|
stdpp = callPackage ../development/coq-modules/stdpp { };
|
||||||
|
StructTact = callPackage ../development/coq-modules/StructTact {};
|
||||||
tlc = callPackage ../development/coq-modules/tlc {};
|
tlc = callPackage ../development/coq-modules/tlc {};
|
||||||
Velisarios = callPackage ../development/coq-modules/Velisarios {};
|
Velisarios = callPackage ../development/coq-modules/Velisarios {};
|
||||||
|
Verdi = callPackage ../development/coq-modules/Verdi {};
|
||||||
};
|
};
|
||||||
|
|
||||||
filterCoqPackages = coq:
|
filterCoqPackages = coq:
|
||||||
|
Loading…
Reference in New Issue
Block a user