Try to get stdlib to not depend on coqc using (env (binaries))

Doesn't work properly.

NB: if there's a coqc in PATH it appears to work, but if there's not
it will say
~~~
Couldn't find Coq standard library, and theory is not using (stdlib no)
~~~

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))))

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}))))

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)

stdlib/tools/rocq_info.mli

@@ -0,0 +1,2 @@
+val path : string
+val hash : string

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)))

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)))