mirror of
https://github.com/NixOS/nixpkgs.git
synced 2026-08-26 02:05:02 +00:00
60 lines
1.9 KiB
Nix
60 lines
1.9 KiB
Nix
{
|
|
lib,
|
|
coq,
|
|
mkRocqDerivation,
|
|
mathcomp-group-representation,
|
|
version ? null,
|
|
}:
|
|
|
|
mkRocqDerivation {
|
|
pname = "odd-order";
|
|
owner = "math-comp";
|
|
|
|
release."2.4.0".hash = "sha256-8U3xFKe/gBSapwNRix3i2+jbyTja5xXGnQwtiTiF+9w=";
|
|
release."2.3.0".hash = "sha256-53FG8I9O+tsIlmaa9qy6VYyJNwWfGmhavKhbZ0VqAGc=";
|
|
release."2.2.0".hash = "sha256-z0C7+wtY8NpoT8wYqHiy8mB2HPYAeJndzDmf7Bb0mg8=";
|
|
release."2.1.0".hash = "sha256-TPlaQbO0yXEpUgy3rlCx/w1MSLECJk5tdU26fAGe48Q=";
|
|
release."1.14.0".hash = "sha256:0iln70npkvixqyz469l6nry545a15jlaix532i1l7pzfkqqn6v68";
|
|
release."1.13.0".hash = "sha256-EzNKR/JzM8T17sMhPhgZNs14e50X4dY3OwFi133IsT0=";
|
|
release."1.12.0".hash = "sha256-omsfdc294CxKAHNMMeqJCcVimvyRCHgxcQ4NJOWSfNM=";
|
|
releaseRev = v: "mathcomp-odd-order.${v}";
|
|
|
|
inherit version;
|
|
defaultVersion =
|
|
let
|
|
case = coq: mc: out: {
|
|
cases = [
|
|
coq
|
|
mc
|
|
];
|
|
inherit out;
|
|
};
|
|
in
|
|
with lib.versions;
|
|
lib.switch
|
|
[ coq.coq-version mathcomp-group-representation.version ]
|
|
[
|
|
(case (range "9.1" "9.3") (range "2.5" "2.6") "2.4.0")
|
|
(case (range "9.0" "9.1") (range "2.5" "2.5") "2.3.0")
|
|
(case (range "8.16" "9.1") (range "2.2.0" "2.4.0") "2.2.0")
|
|
(case (range "8.16" "9.0") (range "2.1.0" "2.3.0") "2.1.0")
|
|
(case (range "8.11" "8.16") (range "1.13.0" "1.15.0") "1.14.0")
|
|
(case (range "8.10" "8.15") (range "1.12.0" "1.14.0") "1.13.0")
|
|
(case (range "8.10" "8.14") (range "1.10.0" "1.12.0") "1.12.0")
|
|
]
|
|
null;
|
|
|
|
useCoqifVersion = v: v != null && v != "dev" && lib.versions.isLe "2.4.0" v;
|
|
|
|
propagatedBuildInputs = [
|
|
mathcomp-group-representation
|
|
];
|
|
|
|
meta = {
|
|
description = "Formal proof of the Odd Order Theorem";
|
|
maintainers = with lib.maintainers; [ siraben ];
|
|
license = lib.licenses.cecill-b;
|
|
platforms = lib.platforms.unix;
|
|
};
|
|
}
|