pyrox.dev
1{
2 lib,
3 mkCoqDerivation,
4 coq,
5 mathcomp,
6 version ? null,
7}:
8
9mkCoqDerivation {
10 pname = "fourcolor";
11 owner = "math-comp";
12
13 releaseRev = v: "v${v}";
14
15 release."1.2.3".sha256 = "sha256-gwKfUa74fIP7j+2eQgnLD7AswjCtOFGHGaIWb4qI0n4=";
16 release."1.2.4".sha256 = "sha256-iSW2O1kuunvOqTolmGGXmsYTxo2MJYCdW3BnEhp6Ksg=";
17 release."1.2.5".sha256 = "sha256-3qOPNCRjGK2UdHGMSqElpIXhAPVCklpeQgZwf9AFals=";
18 release."1.3.0".sha256 = "sha256-h9pa6vaKT6jCEaIdEdcu0498Ou5kEXtZdb9P7WXK1DQ=";
19 release."1.3.1".sha256 = "sha256-wBizm1hJXPYBu0tHFNScQHd22FebsJYoggT5OlhY/zM=";
20 release."1.4.0".sha256 = "sha256-8TtNPEbp3uLAH+MjOKiTZHOjPb3vVYlabuqsdWxbg80=";
21 release."1.4.1".sha256 = "sha256-0UASpo9CdpvidRv33BDWrevo+NSOhxLQFPCJAWPXf+s=";
22
23 inherit version;
24 defaultVersion =
25 let
26 case = coq: mc: out: {
27 cases = [
28 coq
29 mc
30 ];
31 inherit out;
32 };
33 in
34 with lib.versions;
35 lib.switch
36 [ coq.coq-version mathcomp.version ]
37 [
38 (case (isGe "8.16") (isGe "2.0") "1.4.1")
39 (case (isGe "8.16") "2.0.0" "1.3.0")
40 (case (isGe "8.11") (range "1.12" "1.19") "1.2.5")
41 (case (isGe "8.11") (range "1.11" "1.14") "1.2.4")
42 (case (isLe "8.13") (lib.pred.inter (isGe "1.11.0") (isLt "1.13")) "1.2.3")
43 ]
44 null;
45
46 propagatedBuildInputs = [
47 mathcomp.boot
48 mathcomp.fingroup
49 mathcomp.algebra
50 ];
51
52 meta = with lib; {
53 description = "Formal proof of the Four Color Theorem";
54 maintainers = with maintainers; [ siraben ];
55 license = licenses.cecill-b;
56 platforms = platforms.unix;
57 };
58}