diff options
Diffstat (limited to 'nixpkgs/pkgs/development/coq-modules/vcfloat/default.nix')
-rw-r--r-- | nixpkgs/pkgs/development/coq-modules/vcfloat/default.nix | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/nixpkgs/pkgs/development/coq-modules/vcfloat/default.nix b/nixpkgs/pkgs/development/coq-modules/vcfloat/default.nix new file mode 100644 index 000000000000..d5837812ae88 --- /dev/null +++ b/nixpkgs/pkgs/development/coq-modules/vcfloat/default.nix @@ -0,0 +1,20 @@ +{ lib, mkCoqDerivation, coq, interval, compcert, flocq, bignums, version ? null }: + +with lib; mkCoqDerivation { + pname = "vcfloat"; + owner = "VeriNum"; + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = range "8.16" "8.17"; out = "2.1.1"; } + ] null; + release."2.1.1".sha256 = "sha256-bd/XSQhyFUAnSm2bhZEZBWB6l4/Ptlm9JrWu6w9BOpw="; + releaseRev = v: "v${v}"; + + propagatedBuildInputs = [ interval compcert flocq bignums ]; + + meta = { + description = "A tool for Coq proofs about floating-point round-off error"; + maintainers = with maintainers; [ quinn-dougherty ]; + license = licenses.lgpl3Plus; + }; +} |