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 ++--
 dev/shim/dune                | 13 +++++++++++++
 dune                         |  2 +-
 tools/coq_dune.ml            |  7 +++++++
 4 files changed, 23 insertions(+), 3 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
@@ -10,6 +10,19 @@
     (bash "echo \"$(pwd)/%{bin:coqtop} -coqlib $(pwd)/%{project_root}\" \"$@\"")
     (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
diff --git a/dune b/dune
index 32dbc736f3..f1f966b7fd 100644
--- a/dune
+++ b/dune
@@ -19,7 +19,7 @@
  (deps
   (source_tree theories)
   (source_tree plugins))
- (action (with-stdout-to .vfiles.d (bash "%{bin:coqdep} -dyndep opt -noglob -boot `find theories plugins -type f -name *.v`"))))
+ (action (with-stdout-to .vfiles.d (bash "%{bin:coqdep} -dyndep both -noglob -boot `find theories plugins -type f -name *.v`"))))
 
 (alias
  (name vodeps)
diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml
index 62a871aa0e..98368d76ca 100644
--- a/tools/coq_dune.ml
+++ b/tools/coq_dune.ml
@@ -235,6 +235,12 @@ let scan_plugins m =
   let dirs = Sys.(List.filter (fun f -> is_plugin_directory @@ bpath ["plugins";f]) Array.(to_list @@ readdir "plugins")) in
   List.fold_left scan_mlg m dirs
 
+(* This will be removed when we drop support for Make *)
+let fix_cmo_cma file =
+  if String.equal Filename.(extension file) ".cmo"
+  then replace_ext ~file ~newext:".cma"
+  else file
+
 (* Process .vfiles.d and generate a skeleton for the dune file *)
 let parse_coqdep_line l =
   match Str.(split (regexp ":") l) with
@@ -249,6 +255,7 @@ let parse_coqdep_line l =
          the platform. Anyways, I hope we can link to coqdep instead
          of having to parse its output soon, that should solve this
          kind of issues *)
+      let deps = List.map fix_cmo_cma deps in
       Some (String.split_on_char '/' dir, VO { target; deps; })
     (* Otherwise a vio file, we ignore *)
     | _ -> None
-- 
cgit v1.2.3