Unverified Commit 44374839 authored by Théo Zimmermann's avatar Théo Zimmermann Committed by GitHub
Browse files

Merge pull request #258096 from quinn-dougherty/init-coqPackages-vcfloat 

coqPackages.vcfloat: init at 2.1.1
parents ea934cc8 c7634cf5

maintainers/maintainer-list.nix

+6 −0
Original line number Diff line number Diff line
@@ -14432,6 +14432,12 @@ 
    githubId = 1332289;

    name = "Quentin Machu";

  };

  quinn-dougherty = {

    email = "quinnd@riseup.net";

    github = "quinn-dougherty";

    githubId = 39039420;

    name = "Quinn Dougherty";

  };

  qyliss = {

    email = "hi@alyssa.is";

    github = "alyssais";

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

0 → 100644
+20 −0
Original line number Diff line number Diff line 
{ 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;

  };

}

pkgs/top-level/coq-packages.nix

+1 −0
Original line number Diff line number Diff line
@@ -120,6 +120,7 @@ let 
      tlc = callPackage ../development/coq-modules/tlc {};

      topology = callPackage ../development/coq-modules/topology {};

      trakt = callPackage ../development/coq-modules/trakt {};

      vcfloat = callPackage ../development/coq-modules/vcfloat {};

      Velisarios = callPackage ../development/coq-modules/Velisarios {};

      Verdi = callPackage ../development/coq-modules/Verdi {};

      VST = callPackage ../development/coq-modules/VST ((lib.optionalAttrs