tjh.dev
nixpkgs mirror (for testing)
github.com/NixOS/nixpkgs
nix
1{
2 lib,
3 mkCoqDerivation,
4 coq,
5 mathcomp-ssreflect,
6 mathcomp-algebra,
7 mathcomp-fingroup,
8 paramcoq,
9 version ? null,
10}:
11
12mkCoqDerivation {
13 pname = "addition-chains";
14 repo = "hydra-battles";
15
16 release."0.4".sha256 = "1f7pc4w3kir4c9p0fjx5l77401bx12y72nmqxrqs3qqd3iynvqlp";
17 release."0.5".sha256 = "121pcbn6v59l0c165ha9n00whbddpy11npx2y9cn7g879sfk2nqk";
18 release."0.6".sha256 = "1dri4sisa7mhclf8w4kw7ixs5zxm8xyjr034r1377p96rdk3jj0j";
19 releaseRev = (v: "v${v}");
20
21 inherit version;
22 defaultVersion =
23 with lib.versions;
24 lib.switch coq.coq-version [
25 {
26 case = range "8.13" "8.18";
27 out = "0.6";
28 }
29 {
30 case = range "8.11" "8.12";
31 out = "0.4";
32 }
33 ] null;
34
35 propagatedBuildInputs = [
36 mathcomp-ssreflect
37 mathcomp-algebra
38 mathcomp-fingroup
39 paramcoq
40 ];
41
42 useDune = true;
43
44 meta = with lib; {
45 description = "Exponentiation algorithms following addition chains";
46 longDescription = ''
47 Addition chains are algorithms for computations of the p-th
48 power of some x, with the least number of multiplication as
49 possible. We present a few implementations of addition chains,
50 with proofs of their correctness.
51 '';
52 maintainers = with maintainers; [ Zimmi48 ];
53 license = licenses.mit;
54 platforms = platforms.unix;
55 };
56}