tjh.dev
1{
2 lib,
3 mkCoqDerivation,
4 coq,
5 stdlib,
6 version ? null,
7}:
8
9mkCoqDerivation {
10 pname = "aac-tactics";
11
12 releaseRev = v: "v${v}";
13
14 release."8.20.0".sha256 = "sha256-VQzeINIZAfP3Qyh29uPqcNVlNJfIzzRLtN0Cm4EuGCk=";
15 release."8.19.1".sha256 = "sha256-W/V57h+rjb3m0ktCG83PquMHfXiv6H1Nhvw9sVEPLqM=";
16 release."8.19.0".sha256 = "sha256-IeCBd8gcu4bAXH5I/XIT7neQIILi+EWR6qqAA4GzQD0=";
17 release."8.18.0".sha256 = "sha256-Vpe79qCyFLOdOtFFvLKR0N+MMpGD661Q01yx4gxRhZo=";
18 release."8.17.0".sha256 = "sha256-c8DtD21QFDZEVyCQc7ScPZEMTmolxlT3+Db3gStofF8=";
19 release."8.16.0".sha256 = "sha256-sE1w8q/60adNF9yMJQO70CEk3D8QUopvgiszdHt5Wsw=";
20 release."8.15.1".sha256 = "sha256:0k2sl3ns897a5ll11bazgpv4ppgi1vmx4n89v2dnxabm5dglyglp";
21 release."8.14.1".sha256 = "sha256:1w99jgm7mxwdxnalxhralmhmpwwbd52pbbifq0mx13ixkv6iqm1a";
22 release."8.14.0".sha256 = "04x47ngb95m1h4jw2gl0v79s5im7qimcw7pafc34gkkf51pyhakp";
23 release."8.13.2".sha256 = "sha256-MAnMc4KzC551JInrRcfKED4nz04FO0GyyyuDVRmnYTa=";
24 release."8.13.0".sha256 = "sha256-MAnMc4KzC551JInrRcfKED4nz04FO0GyyyuDVRmnYTY=";
25 release."8.12.0".sha256 = "sha256-dPNA19kZo/2t3rbyX/R5yfGcaEfMhbm9bo71Uo4ZwoM=";
26 release."8.11.0".sha256 = "sha256-CKKMiJLltIb38u+ZKwfQh/NlxYawkafp+okY34cGCYU=";
27 release."8.10.0".sha256 = "sha256-Ny3AgfLAzrz3FnoUqejXLApW+krlkHBmYlo3gAG0JsM=";
28 release."8.9.0".sha256 = "sha256-6Pp0dgYEnVaSnkJR/2Cawt5qaxWDpBI4m0WAbQboeWY=";
29 release."8.8.0".sha256 = "sha256-mwIKp3kf/6i9IN3cyIWjoRtW8Yf8cc3MV744zzFM3u4=";
30 release."8.6.1".sha256 = "sha256-PfovQ9xJnzr0eh/tO66yJ3Yp7A5E1SQG46jLIrrbZFg=";
31 release."8.5.0".sha256 = "sha256-7yNxJn6CH5xS5w/zsXfcZYORa6e5/qS9v8PUq2o02h4=";
32
33 inherit version;
34 defaultVersion =
35 with lib.versions;
36 lib.switch coq.coq-version [
37 {
38 case = "8.20";
39 out = "8.20.0";
40 }
41 {
42 case = "8.19";
43 out = "8.19.1";
44 }
45 {
46 case = "8.18";
47 out = "8.18.0";
48 }
49 {
50 case = "8.17";
51 out = "8.17.0";
52 }
53 {
54 case = "8.16";
55 out = "8.16.0";
56 }
57 {
58 case = "8.15";
59 out = "8.15.1";
60 }
61 {
62 case = "8.14";
63 out = "8.14.1";
64 }
65 {
66 case = "8.13";
67 out = "8.13.2";
68 }
69 {
70 case = "8.12";
71 out = "8.12.0";
72 }
73 {
74 case = "8.11";
75 out = "8.11.0";
76 }
77 {
78 case = "8.10";
79 out = "8.10.0";
80 }
81 {
82 case = "8.9";
83 out = "8.9.0";
84 }
85 {
86 case = "8.8";
87 out = "8.8.0";
88 }
89 {
90 case = "8.6";
91 out = "8.6.1";
92 }
93 {
94 case = "8.5";
95 out = "8.5.0";
96 }
97 ] null;
98
99 mlPlugin = true;
100
101 propagatedBuildInputs = [ stdlib ];
102
103 meta = with lib; {
104 description = "Coq plugin providing tactics for rewriting universally quantified equations";
105 longDescription = ''
106 This Coq plugin provides tactics for rewriting universally quantified
107 equations, modulo associativity and commutativity of some operator.
108 The tactics can be applied for custom operators by registering the
109 operators and their properties as type class instances. Many common
110 operator instances, such as for Z binary arithmetic and booleans, are
111 provided with the plugin.
112 '';
113 maintainers = with maintainers; [ siraben ];
114 license = licenses.gpl3Plus;
115 platforms = platforms.unix;
116 };
117}