From 25c631cc0e529066726ddbfbfc5e1ccfe7218dee Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Wed, 29 Mar 2023 14:29:05 +0200
Subject: [PATCH] Add coqPackages.mathcomp-apery

---
 .../coq-modules/mathcomp-apery/default.nix    | 23 +++++++++++++++++++
 pkgs/top-level/coq-packages.nix               |  1 +
 2 files changed, 24 insertions(+)
 create mode 100644 pkgs/development/coq-modules/mathcomp-apery/default.nix

diff --git a/pkgs/development/coq-modules/mathcomp-apery/default.nix b/pkgs/development/coq-modules/mathcomp-apery/default.nix
new file mode 100644
index 000000000000..695116938768
--- /dev/null
+++ b/pkgs/development/coq-modules/mathcomp-apery/default.nix
@@ -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;
+  };
+}
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index 87291ca8f3df..3aa08807f798 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -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 {};