tjh.dev
1{
2 lib,
3 mkCoqDerivation,
4 coq,
5 mathcomp-ssreflect,
6 version ? null,
7}:
8
9mkCoqDerivation {
10 pname = "lemma-overloading";
11 inherit version;
12
13 defaultVersion =
14 with lib.versions;
15 lib.switch
16 [ coq.coq-version mathcomp-ssreflect.version ]
17 [
18 {
19 cases = [
20 (range "8.10" "8.12")
21 (range "1.7" "1.11")
22 ];
23 out = "8.12.0";
24 }
25 {
26 cases = [
27 (range "8.10" "8.11")
28 (range "1.7" "1.11")
29 ];
30 out = "8.11.0";
31 }
32 {
33 cases = [
34 (range "8.8" "8.11")
35 (range "1.7" "1.10")
36 ];
37 out = "8.10.0";
38 }
39 {
40 cases = [
41 (range "8.8" "8.9")
42 (range "1.7" "1.8")
43 ];
44 out = "8.9.0";
45 }
46 {
47 cases = [
48 (isEq "8.8")
49 (range "1.6.2" "1.7")
50 ];
51 out = "8.8.0";
52 }
53 ]
54 null;
55
56 release = {
57 "8.12.0".sha256 = "sha256-ul1IhxFwhLTy3+rmo3gvjHI3Z8A8avN0Rzq0YDy2bjs=";
58 "8.11.0".sha256 = "sha256-RI3KdSEYxUbjfZWKO7atGdEqDU8WmLJSFeF6TLlgUFc=";
59 "8.10.0".sha256 = "sha256-qpHh/iz2fFtGwUedjJ6fuOh8uq1mlL4ETxc9zDJ6800=";
60 "8.9.0".sha256 = "sha256-dE9O94DvcF93TUTU7ky9pvGZgTtPZWz6826b6Js/nHc=";
61 "8.8.0".sha256 = "sha256-Iq3KfESMnZF8hhGKuvZHx+hAMEaoCP7MhhQEI6xfoO8=";
62 };
63 releaseRev = v: "v${v}";
64
65 propagatedBuildInputs = [ mathcomp-ssreflect ];
66
67 meta = with lib; {
68 description = "Libraries demonstrating design patterns for programming and proving with canonical structures in Coq";
69 maintainers = with lib.maintainers; [ cohencyril ];
70 license = licenses.gpl3Plus;
71 };
72}