tjh.dev
1{
2 lib,
3 mkCoqDerivation,
4 coq,
5 interval,
6 compcert,
7 flocq,
8 bignums,
9 version ? null,
10}:
11
12let
13 self = mkCoqDerivation {
14 pname = "vcfloat";
15 owner = "VeriNum";
16 inherit version;
17 sourceRoot = "${self.src.name}/vcfloat";
18 postPatch = ''
19 coq_makefile -o Makefile -f _CoqProject *.v
20 '';
21 defaultVersion =
22 with lib.versions;
23 lib.switch coq.coq-version [
24 {
25 case = isEq "8.20";
26 out = "2.3";
27 }
28 {
29 case = isEq "8.19";
30 out = "2.2";
31 }
32 {
33 case = range "8.16" "8.18";
34 out = "2.1.1";
35 }
36 ] null;
37 release."2.3".sha256 = "sha256-fV7w/kYTpcBxrHFzEvx+eydDHbGH05/seucrgSjKK3w=";
38 release."2.2".sha256 = "sha256-PyMm84ZYh+dOnl8Kk2wlYsQ+S/d1Hsp6uv2twTedEPg=";
39 release."2.1.1".sha256 = "sha256-bd/XSQhyFUAnSm2bhZEZBWB6l4/Ptlm9JrWu6w9BOpw=";
40 releaseRev = v: "v${v}";
41
42 propagatedBuildInputs = [
43 interval
44 compcert
45 flocq
46 bignums
47 ];
48
49 meta = {
50 description = "Tool for Coq proofs about floating-point round-off error";
51 maintainers = with lib.maintainers; [ quinn-dougherty ];
52 license = lib.licenses.lgpl3Plus;
53 };
54 };
55in
56self