diff options
author | Théo Zimmermann <theo.zimmermann@inria.fr> | 2023-10-17 15:02:09 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2023-10-17 15:02:09 +0200 |
commit | 44374839383053f8fedb447974c5cf0f1aadcdc1 (patch) | |
tree | eadb5fceeff0152e644fcffc43fd20768c66420c /pkgs/development/coq-modules | |
parent | ea934cc857b853f363f22d9b68b19fd2ed5894cc (diff) | |
parent | c7634cf59a9d23569c5218435a2e72b8f32f3ddb (diff) |
Merge pull request #258096 from quinn-dougherty/init-coqPackages-vcfloat
coqPackages.vcfloat: init at 2.1.1
Diffstat (limited to 'pkgs/development/coq-modules')
-rw-r--r-- | pkgs/development/coq-modules/vcfloat/default.nix | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/pkgs/development/coq-modules/vcfloat/default.nix b/pkgs/development/coq-modules/vcfloat/default.nix new file mode 100644 index 0000000000000..d5837812ae88a --- /dev/null +++ b/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; + }; +} |