From 430851db6db8ba30280f024ccbca5f6124287ab7 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 12 Mar 2019 12:07:56 +0100
Subject: [dune] Add shim for coqtop.byte

We add a shim for running the byte version of coqtop. This fixes the
Coq part of #9727 , the Dune part is still open at
https://github.com/ocaml/dune/issues/108 but this PR includes a
workaround.

Unfortunately we have to introduce a small inefficiency in the build
process as we build both byte and native versions of plugins for this
work reliable.

As this is a choice done during bootstrap it won't be easy to fix
until we have our own `dune coqtop` command and we can control the
rules depending on the final target.

This should affect the `check` target so still fast builds should be
possible, but if this is a problem we could add a `byteboot` target to
help.
---
 dev/doc/build-system.dune.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev/doc')

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";;
-- 
cgit v1.2.3