pyrox.dev
1{
2 coq,
3 mkCoqDerivation,
4 mathcomp-analysis,
5 mathcomp-analysis-stdlib,
6 mathcomp-algebra-tactics,
7 interval,
8 lib,
9 version ? null,
10}:
11
12(mkCoqDerivation {
13 namePrefix = [
14 "coq"
15 "mathcomp"
16 ];
17 pname = "infotheo";
18 owner = "affeldt-aist";
19 inherit version;
20
21 defaultVersion =
22 let
23 case = coq: mc: out: {
24 cases = [
25 coq
26 mc
27 ];
28 inherit out;
29 };
30 in
31 with lib.versions;
32 lib.switch
33 [ coq.coq-version mathcomp-analysis.version ]
34 [
35 (case (range "8.20" "8.20") (isGe "1.12") "0.9.4")
36 (case (range "8.19" "8.20") (range "1.10" "1.11") "0.9.3")
37 (case (range "8.19" "8.20") (isGe "1.9") "0.9.1")
38 (case (range "8.19" "8.20") (isGe "1.7") "0.7.7")
39 (case (range "8.19" "8.20") (isGe "1.7") "0.7.5")
40 (case (range "8.18" "8.20") (isGe "1.5") "0.7.3")
41 (case (range "8.18" "8.19") (isGe "1.2") "0.7.2")
42 (case (range "8.17" "8.19") (isGe "1.0") "0.7.1")
43 (case (isGe "8.17") (range "0.6.6" "0.7.0") "0.6.1")
44 (case (range "8.17" "8.18") (range "0.6.0" "0.6.7") "0.5.2")
45 (case (range "8.15" "8.16") (range "0.5.4" "0.6.5") "0.5.1")
46 ]
47 null;
48 release."0.9.4".sha256 = "sha256-btHOBNMdXvlG2jxC04+4qmIjeyuaqtyugm2Ruj3lQr8=";
49 release."0.9.3".sha256 = "sha256-8+cnVKNAvZ3MVV3BpS8UmCIxJphsQRBv3swek1eEBjE=";
50 release."0.9.1".sha256 = "sha256-WI20HxMHr1ZUwOGPIUl+nRI8TxVUa2+F1xcGjRDHO9g=";
51 release."0.7.7".sha256 = "sha256-kEbpMl7U+I2kvqi1VrjhIVFkZFO6h0tTHEUZRbHYG7E=";
52 release."0.7.5".sha256 = "sha256-pzPo+Acjx3vlyqOkSZQ8uT2BDLSTfbAnRm39e+/CqE0=";
53 release."0.7.3".sha256 = "sha256-7+qPtE1KfDmo9ZsQtWMzoR2MYnFpTjFHK/yZYVm+GxA=";
54 release."0.7.2".sha256 = "sha256-dekrdVmuTcqXXmKhIb831EKtMhbPrXHJZhzmGb9rdRo=";
55 release."0.7.1".sha256 = "sha256-/4Elb35SmscG6EjEcHYDo+AmWrpBUlygZL0WhaD+fcY=";
56 release."0.6.1".sha256 = "sha256-tFB5lrwRPIlHkP+ebgcJwu03Cc9yVaOINOAo8Bf2LT4=";
57 release."0.5.1".sha256 = "sha256-yBBl5l+V+dggsg5KM59Yo9CULKog/xxE8vrW+ZRnX7Y=";
58 release."0.5.2".sha256 = "sha256-8WAnAV53c0pMTdwj8XcUDUkLZbpUgIQbEOgOb63uHQA=";
59
60 propagatedBuildInputs = [ mathcomp-analysis-stdlib ];
61
62 meta = with lib; {
63 description = "Coq formalization of information theory and linear error-correcting codes";
64 license = licenses.lgpl21Plus;
65 };
66}).overrideAttrs
67 (o: {
68 propagatedBuildInputs =
69 o.propagatedBuildInputs
70 ++ lib.optional (lib.versions.isGe "0.6.1" o.version || o.version == "dev") mathcomp-algebra-tactics
71 ++ lib.optional (lib.versions.isGe "0.7.2" o.version || o.version == "dev") interval;
72 })