Merge PR #9748: [dune] Add shim for coqtop.byte

Reviewed-by: Zimmi48
Reviewed-by: gares

2 files changed, 15 insertions, 2 deletions

diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index a31ab1c511..b1bfac8cc9 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -126,9 +126,9 @@ script again] This will be fixed in the future.
 
 ## Dropping from coqtop:
 
-The following sequence is recommended:
+After doing `make -f Makefile.dune voboot`, the following commands should work:
 ```
-dune exec coqtop.byte
+dune exec dev/shim/coqbyte-prelude
 > Drop.
 # #directory "dev";;
 # #use "include_dune";;
diff --git a/dev/shim/dune b/dev/shim/dune
index 85a0d205da..39b4ef492c 100644
--- a/dev/shim/dune
+++ b/dev/shim/dune
@@ -11,6 +11,19 @@
     (run chmod +x %{targets})))))
 
 (rule
+ (targets coqbyte-prelude)
+ (deps
+  %{bin:coqtop.byte}
+  %{lib:coq.kernel:../../stublibs/dllbyterun_stubs.so}
+  %{project_root}/theories/Init/Prelude.vo)
+ (action
+  (with-outputs-to %{targets}
+   (progn
+    (echo "#!/usr/bin/env bash\n")
+    (bash "echo \"$(pwd)/%{bin:coqtop.byte} -coqlib $(pwd)/%{project_root}\" \"$@\"")
+    (run chmod +x %{targets})))))
+
+(rule
  (targets coqide-prelude)
  (deps
   %{bin:coqqueryworker.opt}