From c20f11c48a8ff9789c913d9c67ed87ee536ec76a Mon Sep 17 00:00:00 2001
From: 4ever2 <3417013+4ever2@users.noreply.github.com>
Date: Wed, 18 Mar 2026 21:59:38 +0100
Subject: [PATCH] coqPackages.CertiRocq: init at 0.9.1

---
 .../coq-modules/CertiRocq/default.nix         | 101 ++++++++++++++++++
 pkgs/top-level/coq-packages.nix               |   1 +
 2 files changed, 102 insertions(+)
 create mode 100644 pkgs/development/coq-modules/CertiRocq/default.nix

diff --git a/pkgs/development/coq-modules/CertiRocq/default.nix b/pkgs/development/coq-modules/CertiRocq/default.nix
new file mode 100644
index 000000000000..cb7f5accee56
--- /dev/null
+++ b/pkgs/development/coq-modules/CertiRocq/default.nix
@@ -0,0 +1,101 @@
+{
+  lib,
+  pkgs,
+  pkg-config,
+  mkCoqDerivation,
+  coq,
+  wasmcert,
+  compcert,
+  metarocq-erasure-plugin,
+  metarocq-safechecker-plugin,
+  ExtLib,
+  version ? null,
+}:
+
+with lib;
+mkCoqDerivation {
+  pname = "CertiRocq";
+  owner = "CertiRocq";
+  repo = "certirocq";
+  opam-name = "rocq-certirocq";
+  mlPlugin = true;
+
+  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" "0.9.1+9.1")
+      ]
+      null;
+  release = {
+    "0.9.1+9.1".sha256 = "sha256-YsweBaoq8+QG63e7Llp/4bHldAFnSQSyMumJkb+Bsp0=";
+  };
+  releaseRev = v: "v${v}";
+
+  buildInputs = [
+    pkgs.clang
+  ];
+
+  propagatedBuildInputs = [
+    wasmcert
+    compcert
+    ExtLib
+    metarocq-erasure-plugin
+    metarocq-safechecker-plugin
+  ];
+
+  patchPhase = ''
+    patchShebangs ./configure.sh
+    patchShebangs ./clean_extraction.sh
+    patchShebangs ./make_plugin.sh
+  '';
+
+  configurePhase = ''
+    ./configure.sh local
+  '';
+
+  buildPhase = ''
+    runHook preBuild
+
+    make all
+    make plugins
+
+    runHook postBuild
+  '';
+
+  installPhase = ''
+    runHook preInstall
+
+    OUTDIR=$out/lib/coq/${coq.coq-version}/user-contrib
+
+    DST=$OUTDIR/CertiRocq/Plugin/runtime make -C runtime install
+    COQLIBINSTALL=$OUTDIR make -C theories install
+    COQLIBINSTALL=$OUTDIR make -C libraries install
+    COQLIBINSTALL=$OUTDIR COQPLUGININSTALL=$OCAMLFIND_DESTDIR make -C plugin install
+    COQLIBINSTALL=$OUTDIR COQPLUGININSTALL=$OCAMLFIND_DESTDIR make -C cplugin install
+
+    runHook postInstall
+  '';
+
+  meta = {
+    description = "CertiRocq";
+    maintainers = with maintainers; [
+      womeier
+      _4ever2
+    ];
+    license = licenses.mit;
+  };
+}
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index 22ed5cc6f4b1..b2b98903066c 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -71,6 +71,7 @@ let
       category-theory = callPackage ../development/coq-modules/category-theory { };
       ceres = callPackage ../development/coq-modules/ceres { };
       ceres-bs = callPackage ../development/coq-modules/ceres-bs { };
+      CertiRocq = callPackage ../development/coq-modules/CertiRocq { };
       Cheerios = callPackage ../development/coq-modules/Cheerios { };
       coinduction = callPackage ../development/coq-modules/coinduction { };
       CoLoR = callPackage ../development/coq-modules/CoLoR (