From 370fd8006ca8882362a50b05bd78b142799356f8 Mon Sep 17 00:00:00 2001
From: 4ever2 <3417013+4ever2@users.noreply.github.com>
Date: Tue, 24 Mar 2026 18:57:46 +0100
Subject: [PATCH] coqPackages.verified-extraction: init at 1.0.0

---
 .../verified-extraction/default.nix           | 66 +++++++++++++++++++
 pkgs/top-level/coq-packages.nix               |  1 +
 2 files changed, 67 insertions(+)
 create mode 100644 pkgs/development/coq-modules/verified-extraction/default.nix

diff --git a/pkgs/development/coq-modules/verified-extraction/default.nix b/pkgs/development/coq-modules/verified-extraction/default.nix
new file mode 100644
index 000000000000..c8ce1f8bf02f
--- /dev/null
+++ b/pkgs/development/coq-modules/verified-extraction/default.nix
@@ -0,0 +1,66 @@
+{
+  lib,
+  mkCoqDerivation,
+  coq,
+  dune,
+  ceres-bs,
+  equations,
+  metarocq-erasure-plugin,
+  version ? null,
+}:
+
+mkCoqDerivation {
+  pname = "verified-extraction";
+  owner = "MetaRocq";
+  repo = "rocq-verified-extraction";
+  opam-name = "rocq-verified-extraction";
+
+  inherit version;
+  defaultVersion =
+    let
+      case = coq: mr: out: {
+        cases = [
+          coq
+          mr
+        ];
+        inherit out;
+      };
+    in
+    lib.switch
+      [
+        coq.coq-version
+        metarocq-erasure-plugin.version
+      ]
+      [
+        (case "9.1" "1.5.1-9.1" "1.0.0-9.1")
+      ]
+      null;
+  release = {
+    "1.0.0-9.1".hash = "sha256-0eKpchQtnPI12rcsb9+qN1pdNX9KY8VryZP0oqHuYeU=";
+  };
+  releaseRev = v: "v${v}";
+
+  mlPlugin = true;
+
+  buildInputs = [ dune ];
+  propagatedBuildInputs = [
+    coq.ocamlPackages.findlib
+    coq.ocamlPackages.malfunction
+    equations
+    metarocq-erasure-plugin
+    ceres-bs
+  ];
+
+  prePatch = ''
+    patchShebangs plugin/plugin/clean_extraction.sh
+  '';
+
+  meta = with lib; {
+    homepage = "https://metarocq.github.io/";
+    description = "Verified Extraction from Rocq to OCaml. Including a bootstrapped extraction plugin";
+    maintainers = with maintainers; [
+      mattam82
+      _4ever2
+    ];
+  };
+}
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index b0204719a753..eff8239c40b2 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -241,6 +241,7 @@ let
       );
       Velisarios = callPackage ../development/coq-modules/Velisarios { };
       Verdi = callPackage ../development/coq-modules/Verdi { };
+      verified-extraction = callPackage ../development/coq-modules/verified-extraction { };
       Vpl = callPackage ../development/coq-modules/Vpl { };
       VplTactic = callPackage ../development/coq-modules/VplTactic { };
       vscoq-language-server = callPackage ../development/coq-modules/vscoq-language-server { };