pkgs/development/coq-modules/vcfloat/default.nix

   1 {
   2   lib,
   3   mkCoqDerivation,
   4   coq,
   5   interval,
   6   compcert,
   7   flocq,
   8   bignums,
   9   version ? null,
  10 }:
  11
  12 let
  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.19";
  26           out = "2.2";
  27         }
  28         {
  29           case = range "8.16" "8.18";
  30           out = "2.1.1";
  31         }
  32       ] null;
  33     release."2.2".sha256 = "sha256-PyMm84ZYh+dOnl8Kk2wlYsQ+S/d1Hsp6uv2twTedEPg=";
  34     release."2.1.1".sha256 = "sha256-bd/XSQhyFUAnSm2bhZEZBWB6l4/Ptlm9JrWu6w9BOpw=";
  35     releaseRev = v: "v${v}";
  36
  37     propagatedBuildInputs = [
  38       interval
  39       compcert
  40       flocq
  41       bignums
  42     ];
  43
  44     meta = {
  45       description = "Tool for Coq proofs about floating-point round-off error";
  46       maintainers = with lib.maintainers; [ quinn-dougherty ];
  47       license = lib.licenses.lgpl3Plus;
  48     };
  49   };
  50 in
  51 self