Commit e976fa8f authored by Vincent Laporte's avatar Vincent Laporte Committed by Vincent Laporte
Browse files

coqPackages.vcfloat: enable for Coq 8.18 & 8.19

parent c02cbef6

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

+7 −5
Original line number Diff line number Diff line 
{ lib, mkCoqDerivation, coq, interval, compcert, flocq, bignums, version ? null }:



let self = with lib; mkCoqDerivation {

let self = mkCoqDerivation {

  pname = "vcfloat";

  owner = "VeriNum";

  inherit version;
@@ -8,9 +8,11 @@ let self = with lib; mkCoqDerivation { 
  postPatch = ''

    coq_makefile -o Makefile -f _CoqProject *.v

  '';

  defaultVersion = with versions; switch coq.coq-version [

    { case = range "8.16" "8.17"; out = "2.1.1"; }

  defaultVersion = with lib.versions; lib.switch coq.coq-version [

    { case = isEq "8.19"; out = "2.2"; }

    { case = range "8.16" "8.18"; out = "2.1.1"; }

  ] null;

  release."2.2".sha256 = "sha256-PyMm84ZYh+dOnl8Kk2wlYsQ+S/d1Hsp6uv2twTedEPg=";

  release."2.1.1".sha256 = "sha256-bd/XSQhyFUAnSm2bhZEZBWB6l4/Ptlm9JrWu6w9BOpw=";

  releaseRev = v: "v${v}";
@@ -18,8 +20,8 @@ let self = with lib; mkCoqDerivation { 


  meta = {

    description = "A tool for Coq proofs about floating-point round-off error";

    maintainers = with maintainers; [ quinn-dougherty ];

    license = licenses.lgpl3Plus;

    maintainers = with lib.maintainers; [ quinn-dougherty ];

    license = lib.licenses.lgpl3Plus;

  };

};

in self

pkgs/top-level/coq-packages.nix

+4 −3
Original line number Diff line number Diff line
@@ -122,9 +122,10 @@ 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 {

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

        (lib.versions.range "8.16" "8.18" self.coq.version) {

          interval = self.interval.override { version = "4.9.0"; };

      };

        });

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

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

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