tjh.dev
1{
2 lib,
3 mkCoqDerivation,
4 coq,
5 version ? null,
6 mathcomp-boot,
7 deriving,
8}:
9
10(mkCoqDerivation {
11 pname = "extructures";
12 owner = "arthuraa";
13
14 inherit version;
15 defaultVersion =
16 let
17 case = coq: mc: out: {
18 cases = [
19 coq
20 mc
21 ];
22 inherit out;
23 };
24 in
25 with lib.versions;
26 lib.switch
27 [ coq.coq-version mathcomp-boot.version ]
28 [
29 (case (range "8.17" "9.1") (range "2.0.0" "2.4.0") "0.5.0")
30 (case (range "8.17" "8.20") (range "2.0.0" "2.3.0") "0.4.0")
31 (case (range "8.11" "8.20") (range "1.12.0" "1.19.0") "0.3.1")
32 (case (range "8.11" "8.14") (isLe "1.12.0") "0.3.0")
33 (case (range "8.10" "8.12") (isLe "1.12.0") "0.2.2")
34 ]
35 null;
36
37 releaseRev = v: "v${v}";
38
39 release."0.5.0".sha256 = "sha256-Guu2+tmHym52DA6SB5Rq/rYWIQEl47Q7YvMaUkfOH2k=";
40 release."0.4.0".sha256 = "sha256-hItFO2XY2LTPSofPTKt3AfOEfiLliaYdzUXgDv4ea9Y=";
41 release."0.3.1".sha256 = "sha256-KcuG/11Yq5ACem4FyVnQqHKvy3tNK7hd0ir2SJzzMN0=";
42 release."0.3.0".sha256 = "sha256:14rm0726f1732ldds495qavg26gsn30w6dfdn36xb12g5kzavp38";
43 release."0.2.2".sha256 = "sha256:1clzza73gccy6p6l95n6gs0adkqd3h4wgl4qg5l0qm4q140grvm7";
44
45 propagatedBuildInputs = [ mathcomp-boot ];
46
47 meta = with lib; {
48 description = "Finite data structures with extensional reasoning";
49 license = licenses.mit;
50 maintainers = [ maintainers.vbgl ];
51 };
52
53}).overrideAttrs
54 (o: {
55 propagatedBuildInputs =
56 o.propagatedBuildInputs
57 ++ lib.optional (lib.versionAtLeast o.version "0.3.0" || o.version == "dev") deriving;
58 })