coqPackages.verified-extraction: init at 1.0.0 (#503111)

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
+    ];
+  };
+}

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 { };