pyrox.dev
1{ lib, mkCoqDerivation, coq, interval, compcert, flocq, bignums, version ? null }:
2
3with lib; mkCoqDerivation {
4 pname = "vcfloat";
5 owner = "VeriNum";
6 inherit version;
7 sourceRoot = "source/vcfloat";
8 postPatch = ''
9 coq_makefile -o Makefile -f _CoqProject *.v
10 '';
11 defaultVersion = with versions; switch coq.coq-version [
12 { case = range "8.16" "8.17"; out = "2.1.1"; }
13 ] null;
14 release."2.1.1".sha256 = "sha256-bd/XSQhyFUAnSm2bhZEZBWB6l4/Ptlm9JrWu6w9BOpw=";
15 releaseRev = v: "v${v}";
16
17 propagatedBuildInputs = [ interval compcert flocq bignums ];
18
19 meta = {
20 description = "A tool for Coq proofs about floating-point round-off error";
21 maintainers = with maintainers; [ quinn-dougherty ];
22 license = licenses.lgpl3Plus;
23 };
24}