tjh.dev
1{
2 fetchurl,
3 coq,
4 mkCoqDerivation,
5 mathcomp,
6 stdlib,
7 lib,
8 version ? null,
9}:
10
11let
12 namePrefix = [
13 "coq"
14 "mathcomp"
15 ];
16 pname = "word";
17 fetcher =
18 {
19 domain,
20 owner,
21 repo,
22 rev,
23 sha256 ? null,
24 ...
25 }:
26 let
27 prefix = "https://${domain}/${owner}/${repo}/";
28 in
29 if sha256 == null then
30 fetchTarball { url = "${prefix}archive/refs/heads/${rev}.tar.gz"; }
31 else
32 fetchurl {
33 url = "${prefix}releases/download/${rev}/${
34 lib.concatStringsSep "-" (namePrefix ++ [ pname ])
35 }-${rev}.tbz";
36 inherit sha256;
37 };
38in
39
40mkCoqDerivation {
41 inherit namePrefix pname fetcher;
42 owner = "jasmin-lang";
43 repo = "coqword";
44 useDune = true;
45
46 releaseRev = v: "v${v}";
47
48 release."3.2".sha256 = "sha256-4HOFFQzKbHIq+ktjJaS5b2Qr8WL1eQ26YxF4vt1FdWM=";
49 release."3.1".sha256 = "sha256-qQHis6554sG7NpCpWhT2wvelnxsrbEPVNv3fpxwxHMU=";
50 release."3.0".sha256 = "sha256-xEgx5HHDOimOJbNMtIVf/KG3XBemOS9XwoCoW6btyJ4=";
51 release."2.4".sha256 = "sha256-OG99PfjhtKikxM9aBKRsej1gTo1O/llAdXdiiyjZf2Q=";
52 release."2.3".sha256 = "sha256-whU1yvFFuxpwQutW41B/WBg5DrVZJW/Do/GuHtzuI3U=";
53 release."2.2".sha256 = "sha256-8BB6SToCrMZTtU78t2K+aExuxk9O1lCqVQaa8wabSm8=";
54 release."2.1".sha256 = "sha256-895gZzwwX8hN9UUQRhcgRlphHANka9R0PRotfmSEelA=";
55 release."2.0".sha256 = "sha256-ySg3AviGGY5jXqqn1cP6lTw3aS5DhawXEwNUgj7pIjA=";
56
57 inherit version;
58 defaultVersion =
59 let
60 case = coq: mc: out: {
61 cases = [
62 coq
63 mc
64 ];
65 inherit out;
66 };
67 in
68 with lib.versions;
69 lib.switch
70 [ coq.coq-version mathcomp.version ]
71 [
72 (case (range "8.16" "9.1") (isGe "2.0") "3.2")
73 (case (range "8.12" "8.20") (range "1.12" "1.19") "2.4")
74 ]
75 null;
76
77 propagatedBuildInputs = [
78 mathcomp.algebra
79 mathcomp.ssreflect
80 mathcomp.fingroup
81 stdlib
82 ];
83
84 meta = with lib; {
85 description = "Yet Another Coq Library on Machine Words";
86 maintainers = [ maintainers.vbgl ];
87 license = licenses.mit;
88 };
89}