diff options
author | Théo Zimmermann <theo.zimmermann@inria.fr> | 2021-08-17 10:25:41 +0200 |
---|---|---|
committer | Théo Zimmermann <theo.zimmermann@inria.fr> | 2021-08-17 14:44:10 +0200 |
commit | ff96901dbd04d4f70f3e5ef52b24a8f0c9227529 (patch) | |
tree | c9b9868be50fad62cd6caa83f8609d003a7436a3 /pkgs/development/coq-modules | |
parent | 98e23395453a69115a27fda26baa41f24d3c0c63 (diff) | |
download | nixpkgs-ff96901dbd04d4f70f3e5ef52b24a8f0c9227529.tar nixpkgs-ff96901dbd04d4f70f3e5ef52b24a8f0c9227529.tar.gz nixpkgs-ff96901dbd04d4f70f3e5ef52b24a8f0c9227529.tar.bz2 nixpkgs-ff96901dbd04d4f70f3e5ef52b24a8f0c9227529.tar.lz nixpkgs-ff96901dbd04d4f70f3e5ef52b24a8f0c9227529.tar.xz nixpkgs-ff96901dbd04d4f70f3e5ef52b24a8f0c9227529.tar.zst nixpkgs-ff96901dbd04d4f70f3e5ef52b24a8f0c9227529.zip |
coqPackages.hydra-battles: 0.3 -> 0.4
Diffstat (limited to 'pkgs/development/coq-modules')
-rw-r--r-- | pkgs/development/coq-modules/hydra-battles/default.nix | 24 |
1 files changed, 14 insertions, 10 deletions
diff --git a/pkgs/development/coq-modules/hydra-battles/default.nix b/pkgs/development/coq-modules/hydra-battles/default.nix index a74eec4b64f..6c3c9d88e0c 100644 --- a/pkgs/development/coq-modules/hydra-battles/default.nix +++ b/pkgs/development/coq-modules/hydra-battles/default.nix @@ -1,28 +1,32 @@ -{ lib, mkCoqDerivation, coq, mathcomp, equations, paramcoq, version ? null }: +{ lib, mkCoqDerivation, coq, equations, version ? null }: with lib; mkCoqDerivation { pname = "hydra-battles"; owner = "coq-community"; - release."0.3".rev = "v0.3"; - release."0.3".sha256 = "sha256-rXP/vJqVEg2tN/I9LWV13YQ1+C7M6lzGu3oI+7pSZzg="; + 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.3"; } + { case = isGe "8.11"; out = "0.4"; } ] null; - propagatedBuildInputs = [ mathcomp equations paramcoq ]; + propagatedBuildInputs = [ equations ]; + + useDune2 = true; meta = { - description = "Variations on Kirby & Paris' hydra battles and other entertaining math in Coq"; + description = "Exploration of some properties of Kirby and Paris' hydra battles, with the help of Coq"; longDescription = '' - Variations on Kirby & Paris' hydra battles and other - entertaining math in Coq (collaborative, documented, includes - exercises) + An exploration of some properties of Kirby and Paris' hydra + battles, with the help of the Coq Proof assistant. This + development includes the study of several representations of + ordinal numbers, and a part of the so-called Ketonen and Solovay + machinery (combinatorial properties of epsilon0). ''; - maintainers = with maintainers; [ siraben ]; + maintainers = with maintainers; [ siraben Zimmi48 ]; license = licenses.mit; platforms = platforms.unix; }; |