From aff253f5dc70f76661bf0743fd41cbec1cbb8aff Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Wed, 26 Aug 2026 15:52:36 +0200
Subject: [PATCH] Cleanup no longer needed rocq-wrap.sh

Since dune build requires dune >= 3.21 and uses rocq lang 0.11,
it is able to compile without the coq* compat binaries
that the rocq-wrap.sh script was faking.
---
 .nix/rocq-overlays/stdlib-html/default.nix    |  3 +-
 .../stdlib-refman-html/default.nix            |  3 +-
 Makefile                                      |  2 +-
 dev/with-rocq-wrap.sh                         | 53 -------------------
 4 files changed, 3 insertions(+), 58 deletions(-)
 delete mode 100755 dev/with-rocq-wrap.sh

diff --git a/.nix/rocq-overlays/stdlib-html/default.nix b/.nix/rocq-overlays/stdlib-html/default.nix
index dc5c67804d..4553cd2c0f 100644
--- a/.nix/rocq-overlays/stdlib-html/default.nix
+++ b/.nix/rocq-overlays/stdlib-html/default.nix
@@ -8,8 +8,7 @@ rocqPackages.lib.overrideRocqDerivation {
   useDune = true;
 
   buildPhase = ''
-    patchShebangs dev/with-rocq-wrap.sh
-    dev/with-rocq-wrap.sh dune build @stdlib-html ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}
+    dune build @stdlib-html ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}
   '';
 
   installPhase = ''
diff --git a/.nix/rocq-overlays/stdlib-refman-html/default.nix b/.nix/rocq-overlays/stdlib-refman-html/default.nix
index bdf9ed39ac..0e53133a3e 100644
--- a/.nix/rocq-overlays/stdlib-refman-html/default.nix
+++ b/.nix/rocq-overlays/stdlib-refman-html/default.nix
@@ -16,8 +16,7 @@ rocqPackages.lib.overrideRocqDerivation {
   useDune = true;
 
   buildPhase = ''
-    patchShebangs dev/with-rocq-wrap.sh
-    dev/with-rocq-wrap.sh dune build --root . --no-buffer @refman-html ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}
+    dune build --root . --no-buffer @refman-html ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}
   '';
 
   installPhase = ''
diff --git a/Makefile b/Makefile
index e1b7b3e8b7..5d873dd23d 100644
--- a/Makefile
+++ b/Makefile
@@ -1,4 +1,4 @@
-DUNE=dev/with-rocq-wrap.sh dune
+DUNE=dune
 
 .PHONY: clean all install dune dune-install test-suite
 
diff --git a/dev/with-rocq-wrap.sh b/dev/with-rocq-wrap.sh
deleted file mode 100755
index 6f6bea17ab..0000000000
--- a/dev/with-rocq-wrap.sh
+++ /dev/null
@@ -1,53 +0,0 @@
-#!/usr/bin/env bash
-
-set -ex
-
-rocq=$(command -v rocq)
-# NB on cygwin "$rocq" is a cygwin path (/foo/bar)
-# but reading files from hash.exe needs windows paths (C:/cygwin/foo/bar)
-# we avoid the problem by going through stdin
-rocqhash=$(dune exec --root "$(dirname "$0")"/.. -- dev/tools/hash.exe < "$rocq")
-
-rm -rf .wrappers
-mkdir .wrappers
-
-cat > .wrappers/coqc <<EOF
-#!/bin/sh
-# hash = $rocqhash
-exec rocq c "\$@"
-EOF
-
-cat > .wrappers/coqdep <<EOF
-#!/bin/sh
-# hash = $rocqhash
-exec rocq dep "\$@"
-EOF
-
-cat > .wrappers/coqdoc <<EOF
-#!/bin/sh
-# hash = $rocqhash
-exec rocq doc "\$@"
-EOF
-
-chmod +x .wrappers/coqc .wrappers/coqdep .wrappers/coqdoc
-
-ln -s "$(ocamlfind query rocq-runtime.kernel)" .wrappers/kernel
-
-# fake coq-core.kernel for dune (mode native)
-cat > .wrappers/META.coq-core <<EOF
-package "kernel" (
-  directory = "kernel"
-  version = "dev"
-  description = "The Rocq Kernel"
-  requires = "dynlink rocq-runtime.boot rocq-runtime.lib rocq-runtime.vm"
-  archive(byte) = "kernel.cma"
-  archive(native) = "kernel.cmxa"
-  plugin(byte) = "kernel.cma"
-  plugin(native) = "kernel.cmxs"
-)
-EOF
-
-export PATH="$PWD/.wrappers:$PATH"
-export OCAMLPATH="$PWD/.wrappers:$OCAMLPATH"
-
-"$@"