coqPackages.bbv: init at 1.5
This commit is contained in:
parent
59429f63d1
commit
1a638589b3
20
pkgs/development/coq-modules/bbv/default.nix
Normal file
20
pkgs/development/coq-modules/bbv/default.nix
Normal file
@ -0,0 +1,20 @@
|
|||||||
|
{ lib, mkCoqDerivation, coq, version ? null }:
|
||||||
|
|
||||||
|
mkCoqDerivation {
|
||||||
|
pname = "bbv";
|
||||||
|
owner = "mit-plv";
|
||||||
|
inherit version;
|
||||||
|
defaultVersion = let inherit (lib.versions) range; in
|
||||||
|
lib.switch coq.coq-version [
|
||||||
|
{ case = range "8.16" "8.19"; out = "1.5"; }
|
||||||
|
] null;
|
||||||
|
release = {
|
||||||
|
"1.5".sha256 = "sha256-8/VPsfhNpuYpLmLC/hWszDhgvS6n8m7BRxUlea8PSUw=";
|
||||||
|
};
|
||||||
|
releaseRev = v: "v${v}";
|
||||||
|
|
||||||
|
meta = {
|
||||||
|
description = "An implementation of bitvectors in Coq.";
|
||||||
|
license = lib.licenses.mit;
|
||||||
|
};
|
||||||
|
}
|
@ -22,6 +22,7 @@ let
|
|||||||
async-test = callPackage ../development/coq-modules/async-test {};
|
async-test = callPackage ../development/coq-modules/async-test {};
|
||||||
atbr = callPackage ../development/coq-modules/atbr {};
|
atbr = callPackage ../development/coq-modules/atbr {};
|
||||||
autosubst = callPackage ../development/coq-modules/autosubst {};
|
autosubst = callPackage ../development/coq-modules/autosubst {};
|
||||||
|
bbv = callPackage ../development/coq-modules/bbv {};
|
||||||
bignums = if lib.versionAtLeast coq.coq-version "8.6"
|
bignums = if lib.versionAtLeast coq.coq-version "8.6"
|
||||||
then callPackage ../development/coq-modules/bignums {}
|
then callPackage ../development/coq-modules/bignums {}
|
||||||
else null;
|
else null;
|
||||||
|
Loading…
Reference in New Issue
Block a user