From e7c74a75a2ae75a9e6061843fb57ea15868eecf1 Mon Sep 17 00:00:00 2001
From: definfo <hjsdbb1@gmail.com>
Date: Wed, 24 Jul 2024 21:10:01 +0800
Subject: [PATCH 1/2] maintainers: add definfo

---
 maintainers/maintainer-list.nix | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/maintainers/maintainer-list.nix b/maintainers/maintainer-list.nix
index ad714e25cc6d..a29c6a67128a 100644
--- a/maintainers/maintainer-list.nix
+++ b/maintainers/maintainer-list.nix
@@ -4762,6 +4762,12 @@
     githubId = 41747605;
     keys = [ { fingerprint = "6130 3BBA D7D1 BF74 EFA4  4E3B E7FE 2087 E438 0E64"; } ];
   };
+  definfo = {
+    name = "Adrien SUN";
+    email = "hjsdbb1@gmail.com";
+    github = "definfo";
+    githubId = 66514911;
+  };
   deifactor = {
     name = "Ash Zahlen";
     email = "ext0l@riseup.net";

From b1d0e56bc4132a2df2ccdecddf04815fbbbbfe0d Mon Sep 17 00:00:00 2001
From: definfo <hjsdbb1@gmail.com>
Date: Wed, 24 Jul 2024 23:57:23 +0800
Subject: [PATCH 2/2] coqPackages.high-school-geometry: init at 8.16

---
 .../high-school-geometry/default.nix          | 27 +++++++++++++++++++
 pkgs/top-level/coq-packages.nix               |  1 +
 2 files changed, 28 insertions(+)
 create mode 100644 pkgs/development/coq-modules/high-school-geometry/default.nix

diff --git a/pkgs/development/coq-modules/high-school-geometry/default.nix b/pkgs/development/coq-modules/high-school-geometry/default.nix
new file mode 100644
index 000000000000..2f478978bd58
--- /dev/null
+++ b/pkgs/development/coq-modules/high-school-geometry/default.nix
@@ -0,0 +1,27 @@
+{ lib, mkCoqDerivation, coq, version ? null }:
+
+mkCoqDerivation {
+  pname = "high-school-geometry";
+  inherit version;
+  repo = "HighSchoolGeometry";
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
+    { case = range "8.16" "8.20"; out = "8.16"; }
+    { case = range "8.12" "8.16"; out = "8.13"; }
+    { case = "8.12"; out = "8.12"; }
+    { case = "8.11"; out = "8.11"; }
+  ] null;
+
+  release = {
+    "8.16".sha256 = "sha256-HvUrZ6l7wCshuKUZs8rvfMkTEv+oXuogI5LICcD8Bn8=";
+    "8.13".sha256 = "sha256-5F/6155v0bWi5t7n4qU/GuR6jENngvWIIqJGPURzIeQ=";
+    "8.12".sha256 = "sha256-OF7sahU+5Ormkcrd8t6p2Kp/B2/Q/6zYTV3/XBvlGHc=";
+    "8.11".sha256 = "sha256-sVGeBBAJ7a7f+EJU1aSUvIVe9ip9PakY4379XWvvoqw=";
+  };
+  releaseRev = v: "v${v}";
+
+  meta = with lib; {
+    description = "Geometry in Coq for French high school";
+    maintainers = with maintainers; [ definfo ];
+    license = licenses.lgpl21Plus;
+  };
+}
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index 5998f4234eb6..711a00d2b1ae 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -68,6 +68,7 @@ let
       graph-theory = callPackage ../development/coq-modules/graph-theory {};
       heq = callPackage ../development/coq-modules/heq {};
       hierarchy-builder = callPackage ../development/coq-modules/hierarchy-builder {};
+      high-school-geometry = callPackage ../development/coq-modules/high-school-geometry {};
       HoTT = callPackage ../development/coq-modules/HoTT {};
       hydra-battles = callPackage ../development/coq-modules/hydra-battles {};
       interval = callPackage ../development/coq-modules/interval {};