b12f/nixpkgs
1
0
Fork 0
Code Issues Pull requests Packages Projects Releases Wiki Activity

Add coqPackages.mathcomp-apery

Browse source
This commit is contained in:
Pierre Roux 2023-03-29 14:29:05 +02:00 committed by Vincent Laporte
parent 29743d181a
commit 25c631cc0e
2 changed files with 24 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
pkgs/development/coq-modules/mathcomp-apery/default.nix Normal file
View file

@ -0,0 +1,23 @@
{ coq, mkCoqDerivation, mathcomp, coqeal, mathcomp-real-closed,
mathcomp-bigenough, mathcomp-zify, mathcomp-algebra-tactics,
lib, version ? null }:
mkCoqDerivation {
pname = "apery";
inherit version;
defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ] [
{ cases = [ (range "8.13" "8.16") (isGe "1.12.0") ]; out = "1.0.2"; }
] null;
release."1.0.2".sha256 = "sha256-llxyMKYvWUA7fyroG1S/jtpioAoArmarR1edi3cikcY=";
propagatedBuildInputs = [ mathcomp.field coqeal mathcomp-real-closed
mathcomp-bigenough mathcomp-zify mathcomp-algebra-tactics ];
meta = {
description = "A formally verified proof in Coq, by computer algebra, that ζ(3) is irrational";
license = lib.licenses.cecill-c;
};
}

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

@ -77,6 +77,7 @@ let
mathcomp-character = self.mathcomp.character;
mathcomp-abel = callPackage ../development/coq-modules/mathcomp-abel {};
mathcomp-analysis = callPackage ../development/coq-modules/mathcomp-analysis {};
mathcomp-apery = callPackage ../development/coq-modules/mathcomp-apery {};
mathcomp-classical = self.mathcomp-analysis.classical;
mathcomp-finmap = callPackage ../development/coq-modules/mathcomp-finmap {};
mathcomp-bigenough = callPackage ../development/coq-modules/mathcomp-bigenough {};