diff --git a/stdlib/dune b/stdlib/dune
new file mode 100644
index 000000000000..c2419136528d
--- /dev/null
+++ b/stdlib/dune
@@ -0,0 +1,6 @@
+; NB rocq dep will declare the dependency on the worker
+(env
+ (_
+  (binaries
+   (tools/rocqc.exe as coqc)
+   (tools/rocqdep.exe as coqdep))))
diff --git a/stdlib/tools/dune b/stdlib/tools/dune
new file mode 100644
index 000000000000..d3364f582cf1
--- /dev/null
+++ b/stdlib/tools/dune
@@ -0,0 +1,22 @@
+(library
+ (name rocq_info)
+ (modules rocq_info))
+
+(executable
+ (name rocqc)
+ (modules rocqc)
+ (libraries rocq_info unix))
+
+(executable
+ (name rocqdep)
+ (modules rocqdep)
+ (libraries rocq_info unix))
+
+(executable
+ (name mkinfo)
+ (modules mkinfo))
+
+(rule
+ (targets rocq_info.ml)
+ (deps %{bin:rocq})
+ (action (with-stdout-to %{targets} (run ./mkinfo.exe %{deps}))))
diff --git a/stdlib/tools/mkinfo.ml b/stdlib/tools/mkinfo.ml
new file mode 100644
index 000000000000..b55275f443a6
--- /dev/null
+++ b/stdlib/tools/mkinfo.ml
@@ -0,0 +1,4 @@
+let () =
+  let hash = Digest.file Sys.argv.(1) in
+  Printf.printf "let path = %S\n" Sys.argv.(1);
+  Printf.printf "let hash = %S\n%!" (Digest.to_hex hash)
diff --git a/stdlib/tools/rocq_info.mli b/stdlib/tools/rocq_info.mli
new file mode 100644
index 000000000000..7b32e449db1f
--- /dev/null
+++ b/stdlib/tools/rocq_info.mli
@@ -0,0 +1,2 @@
+val path : string
+val hash : string
diff --git a/stdlib/tools/rocqc.ml b/stdlib/tools/rocqc.ml
new file mode 100644
index 000000000000..bfb01a28bb41
--- /dev/null
+++ b/stdlib/tools/rocqc.ml
@@ -0,0 +1,27 @@
+let () =
+  match Sys.argv.(1) with
+  | exception Invalid_argument _ -> ()
+  | "-debug-shim" ->
+    Printf.eprintf "expected rocq hash = %s\n%!" Rocq_info.hash
+  | _ -> ()
+
+let exec_or_create_process prog argv =
+  if Sys.os_type <> "Win32" then
+    Unix.execv prog argv
+  else
+    let pid = Unix.create_process prog argv Unix.stdin Unix.stdout Unix.stderr in
+    if pid = 0 then begin
+      Printf.eprintf "coqc shim: create_process failed\n%!";
+      exit 127
+    end;
+    let _, status = Unix.waitpid [] pid in
+    match status with
+    | WEXITED n | WSIGNALED n -> exit n
+    | WSTOPPED _ ->
+      (* is there anything sensible to do with WSTOPPED? can it even happen on windows? *)
+      assert false
+
+let () =
+  exec_or_create_process Rocq_info.path
+    (Array.append [|Rocq_info.path;"compile"|]
+       (Array.sub Sys.argv 1 (Array.length Sys.argv - 1)))
diff --git a/stdlib/tools/rocqdep.ml b/stdlib/tools/rocqdep.ml
new file mode 100644
index 000000000000..624fe28a334f
--- /dev/null
+++ b/stdlib/tools/rocqdep.ml
@@ -0,0 +1,27 @@
+let () =
+  match Sys.argv.(1) with
+  | exception Invalid_argument _ -> ()
+  | "-debug-shim" ->
+    Printf.eprintf "expected rocq hash = %s\n%!" Rocq_info.hash
+  | _ -> ()
+
+let exec_or_create_process prog argv =
+  if Sys.os_type <> "Win32" then
+    Unix.execv prog argv
+  else
+    let pid = Unix.create_process prog argv Unix.stdin Unix.stdout Unix.stderr in
+    if pid = 0 then begin
+      Printf.eprintf "coqc shim: create_process failed\n%!";
+      exit 127
+    end;
+    let _, status = Unix.waitpid [] pid in
+    match status with
+    | WEXITED n | WSIGNALED n -> exit n
+    | WSTOPPED _ ->
+      (* is there anything sensible to do with WSTOPPED? can it even happen on windows? *)
+      assert false
+
+let () =
+  exec_or_create_process Rocq_info.path
+    (Array.append [|Rocq_info.path;"dep"|]
+       (Array.sub Sys.argv 1 (Array.length Sys.argv - 1)))