tjh.dev
1{
2 coq,
3 mkCoqDerivation,
4 mathcomp,
5 mathcomp-real-closed,
6 lib,
7 version ? null,
8}:
9
10mkCoqDerivation {
11
12 namePrefix = [
13 "coq"
14 "mathcomp"
15 ];
16 pname = "abel";
17 owner = "math-comp";
18
19 inherit version;
20 defaultVersion =
21 let
22 case = coq: mc: out: {
23 cases = [
24 coq
25 mc
26 ];
27 inherit out;
28 };
29 in
30 with lib.versions;
31 lib.switch
32 [ coq.coq-version mathcomp.version ]
33 [
34 (case (range "8.10" "8.16") (range "1.12.0" "1.15.0") "1.2.1")
35 (case (range "8.10" "8.15") (range "1.12.0" "1.14.0") "1.2.0")
36 (case (range "8.10" "8.14") (range "1.11.0" "1.12.0") "1.1.2")
37 ]
38 null;
39
40 release."1.2.1".sha256 = "sha256-M1q6WIPBsayHde2hwlTxylH169hcTs3OuFsEkM0e3yc=";
41 release."1.2.0".sha256 = "1picd4m85ipj22j3b84cv8ab3330radzrhd6kp0gpxq14dhv02c2";
42 release."1.1.2".sha256 = "0565w713z1cwxvvdlqws2z5lgdys8lddf0vpwfdj7bpd7pq9hwxg";
43 release."1.0.0".sha256 = "190jd8hb8anqsvr9ysr514pm5sh8qhw4030ddykvwxx9d9q6rbp3";
44
45 propagatedBuildInputs = [
46 mathcomp.field
47 mathcomp-real-closed
48 ];
49
50 meta = with lib; {
51 description = "Abel - Galois and Abel - Ruffini Theorems";
52 license = licenses.cecill-b;
53 maintainers = [ maintainers.cohencyril ];
54 };
55}