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