nordic-dev.net/nixpkgs
nordic-dev.net/nixpkgs
2
0
Fork 0
mirror of https://github.com/NixOS/nixpkgs.git synced 2024-11-27 09:23:01 +00:00
Code Issues Packages Projects Releases Wiki Activity

coqPackages.addition-chains: init at 0.4

Browse Source
This commit is contained in:
Théo Zimmermann 2021-08-17 10:40:13 +02:00
parent ff96901dbd
commit 58c1ab9158
No known key found for this signature in database
GPG Key ID: F1744A0942F536C7
2 changed files with 34 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

33
pkgs/development/coq-modules/addition-chains/default.nix Normal file
View File

@ -0,0 +1,33 @@
{ lib, mkCoqDerivation, coq, mathcomp-ssreflect, mathcomp-algebra, paramcoq
, version ? null }:
with lib;
mkCoqDerivation {
pname = "addition-chains";
repo = "hydra-battles";
release."0.4".sha256 = "sha256:1f7pc4w3kir4c9p0fjx5l77401bx12y72nmqxrqs3qqd3iynvqlp";
releaseRev = (v: "v${v}");
inherit version;
defaultVersion = with versions; switch coq.coq-version [
{ case = isGe "8.11"; out = "0.4"; }
] null;
propagatedBuildInputs = [ mathcomp-ssreflect mathcomp-algebra paramcoq ];
useDune2 = true;
meta = {
description = "Exponentiation algorithms following addition chains";
longDescription = ''
Addition chains are algorithms for computations of the p-th
power of some x, with the least number of multiplication as
possible. We present a few implementations of addition chains,
with proofs of their correctness.
'';
maintainers = with maintainers; [ Zimmi48 ];
license = licenses.mit;
platforms = platforms.unix;
};
}

1
pkgs/top-level/coq-packages.nix
View File

@ -14,6 +14,7 @@ let
(callPackage ../development/coq-modules/contribs {});
aac-tactics = callPackage ../development/coq-modules/aac-tactics {};
addition-chains = callPackage ../development/coq-modules/addition-chains {};
autosubst = callPackage ../development/coq-modules/autosubst {};
bignums = if lib.versionAtLeast coq.coq-version "8.6"
then callPackage ../development/coq-modules/bignums {}