tjh.dev
nixpkgs mirror (for testing)
github.com/NixOS/nixpkgs
nix
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 release."1.4.2".sha256 = "sha256-d5J8j8gi6siwCLevM6y8Hf2rTB/HEfh72LLk0Qlzr0c=";
23
24 inherit version;
25 defaultVersion =
26 let
27 case = coq: mc: out: {
28 cases = [
29 coq
30 mc
31 ];
32 inherit out;
33 };
34 in
35 with lib.versions;
36 lib.switch
37 [ coq.coq-version mathcomp.version ]
38 [
39 (case (isGe "8.20") (isGe "2.4") "1.4.2")
40 (case (isGe "8.16") (isGe "2.0") "1.4.1")
41 (case (isGe "8.16") "2.0.0" "1.3.0")
42 (case (isGe "8.11") (range "1.12" "1.19") "1.2.5")
43 (case (isGe "8.11") (range "1.11" "1.14") "1.2.4")
44 (case (isLe "8.13") (lib.pred.inter (isGe "1.11.0") (isLt "1.13")) "1.2.3")
45 ]
46 null;
47
48 propagatedBuildInputs = [
49 mathcomp.boot
50 mathcomp.fingroup
51 mathcomp.algebra
52 ];
53
54 meta = {
55 description = "Formal proof of the Four Color Theorem";
56 maintainers = with lib.maintainers; [ siraben ];
57 license = lib.licenses.cecill-b;
58 platforms = lib.platforms.unix;
59 };
60}