From 67a843262fd6b475c588f0aa840f4e65859c23bb Mon Sep 17 00:00:00 2001
From: 4ever2 <3417013+4ever2@users.noreply.github.com>
Date: Wed, 25 Feb 2026 20:50:32 +0100
Subject: [PATCH] coqPackages.TypedExtraction: init at 0.2.0

---
 .../coq-modules/TypedExtraction/default.nix   | 127 ++++++++++++++++++
 pkgs/top-level/coq-packages.nix               |   5 +
 2 files changed, 132 insertions(+)
 create mode 100644 pkgs/development/coq-modules/TypedExtraction/default.nix

diff --git a/pkgs/development/coq-modules/TypedExtraction/default.nix b/pkgs/development/coq-modules/TypedExtraction/default.nix
new file mode 100644
index 000000000000..ab5c95a7c01f
--- /dev/null
+++ b/pkgs/development/coq-modules/TypedExtraction/default.nix
@@ -0,0 +1,127 @@
+{
+  lib,
+  mkCoqDerivation,
+  which,
+  coq,
+  stdlib,
+  metarocq,
+  version ? null,
+  single ? false,
+}:
+
+let
+  pname = "TypedExtraction";
+  repo = "rocq-typed-extraction";
+  owner = "peregrine-project";
+  domain = "github.com";
+
+  inherit version;
+  defaultVersion =
+    let
+      case = coq: mr: out: {
+        cases = [
+          coq
+          mr
+        ];
+        inherit out;
+      };
+    in
+    lib.switch
+      [
+        coq.coq-version
+        metarocq.version
+      ]
+      [
+        (case "9.1" (lib.versions.range "1.4" "1.4.1") "0.2.0")
+      ]
+      null;
+  release = {
+    "0.2.0".sha256 = "sha256-rgg39X45IXjcnejBhh8N7wMiH+gHQrfO8pBbFEWOGVI=";
+  };
+  releaseRev = v: "v${v}";
+
+  packages = {
+    "common" = [ ];
+    "elm" = [
+      "common"
+    ];
+    "rust" = [
+      "common"
+    ];
+    "plugin" = [
+      "elm"
+      "rust"
+    ];
+    "all" = [
+      "plugin"
+    ];
+  };
+
+  typedextraction_ =
+    package:
+    let
+      typedextraction-deps = lib.optionals (package != "single") (
+        map typedextraction_ packages.${package}
+      );
+      pkgpath = if package == "single" then "./" else "./${package}";
+      pname = if package == "all" then "TypedExtraction" else "TypedExtraction-${package}";
+      pkgallMake = ''
+        mkdir all
+        echo "all:" > all/Makefile
+        echo "install:" >> all/Makefile
+      '';
+      derivation = (
+        mkCoqDerivation (
+          {
+            inherit
+              version
+              pname
+              defaultVersion
+              release
+              releaseRev
+              repo
+              owner
+              ;
+
+            mlPlugin = true;
+            propagatedBuildInputs = [
+              stdlib
+              coq.ocamlPackages.findlib
+              metarocq
+            ]
+            ++ typedextraction-deps;
+
+            patchPhase = ''
+              patchShebangs ./configure.sh
+              patchShebangs ./plugin/process_extraction.sh
+            '';
+
+            configurePhase =
+              lib.optionalString (package == "all") pkgallMake
+              + ''
+                touch ${pkgpath}/_config
+              ''
+              + lib.optionalString (package == "single") ''
+                ./configure.sh local
+              '';
+
+            preBuild = ''
+              cd ${pkgpath}
+            '';
+
+            meta = {
+              homepage = "https://peregrine-project.github.io/";
+              description = "A framework for extracting Rocq programs to Rust and Elm";
+              maintainers = with lib.maintainers; [ _4ever2 ];
+              license = lib.licenses.mit;
+            };
+          }
+          // lib.optionalAttrs (package != "single") {
+            passthru = lib.mapAttrs (package: deps: typedextraction_ package) packages;
+          }
+        )
+      );
+    in
+    derivation;
+in
+typedextraction_ (if single then "single" else "all")
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index b24ab749b997..18f608a57c20 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -223,6 +223,11 @@ let
       tlc = callPackage ../development/coq-modules/tlc { };
       topology = callPackage ../development/coq-modules/topology { };
       trakt = callPackage ../development/coq-modules/trakt { };
+      TypedExtraction = callPackage ../development/coq-modules/TypedExtraction { };
+      TypedExtraction-common = self.TypedExtraction.common;
+      TypedExtraction-elm = self.TypedExtraction.elm;
+      TypedExtraction-rust = self.TypedExtraction.rust;
+      TypedExtraction-plugin = self.TypedExtraction.plugin;
       unicoq = callPackage ../development/coq-modules/unicoq { };
       validsdp = callPackage ../development/coq-modules/validsdp { };
       vcfloat = callPackage ../development/coq-modules/vcfloat (