tjh.dev
nixpkgs mirror (for testing)
github.com/NixOS/nixpkgs
nix
1{
2 lib,
3 mkCoqDerivation,
4 coq,
5 equations,
6 LibHyps,
7 version ? null,
8}:
9
10(mkCoqDerivation {
11 pname = "hydra-battles";
12 owner = "coq-community";
13
14 release."0.4".sha256 = "1f7pc4w3kir4c9p0fjx5l77401bx12y72nmqxrqs3qqd3iynvqlp";
15 release."0.5".sha256 = "121pcbn6v59l0c165ha9n00whbddpy11npx2y9cn7g879sfk2nqk";
16 release."0.6".sha256 = "1dri4sisa7mhclf8w4kw7ixs5zxm8xyjr034r1377p96rdk3jj0j";
17 release."0.9".sha256 = "sha256-wlK+154owQD/03FB669KCjyQlL2YOXLCi0KLSo0DOwc=";
18 releaseRev = (v: "v${v}");
19
20 inherit version;
21 defaultVersion =
22 let
23 case = case: out: { inherit case out; };
24 in
25 with lib.versions;
26 lib.switch coq.coq-version [
27 (case (range "8.13" "8.16") "0.9")
28 (case (range "8.11" "8.12") "0.4")
29 ] null;
30
31 useDune = true;
32
33 meta = {
34 description = "Exploration of some properties of Kirby and Paris' hydra battles, with the help of Coq";
35 longDescription = ''
36 An exploration of some properties of Kirby and Paris' hydra
37 battles, with the help of the Coq Proof assistant. This
38 development includes the study of several representations of
39 ordinal numbers, and a part of the so-called Ketonen and Solovay
40 machinery (combinatorial properties of epsilon0).
41 '';
42 maintainers = with lib.maintainers; [
43 siraben
44 Zimmi48
45 ];
46 license = lib.licenses.mit;
47 platforms = lib.platforms.unix;
48 };
49}).overrideAttrs
50 (
51 o:
52 let
53 inherit (o) version;
54 in
55 {
56 propagatedBuildInputs = [
57 equations
58 ]
59 ++ lib.optional (lib.versions.isGe "0.6" version || version == "dev") LibHyps;
60 }
61 )