From 6930dd3533e7829184daa4cd8a84be62d9886c77 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 8 Nov 2019 11:36:22 +0100
Subject: coqdep: only output vos when passed -vos

This fixes dune. TBH the problem is that dune is too strict, but we
can't go back in time to change it.
---
 tools/CoqMakefile.in    | 2 +-
 tools/coqdep.ml         | 1 +
 tools/coqdep_common.ml  | 9 ++++++---
 tools/coqdep_common.mli | 3 +++
 4 files changed, 11 insertions(+), 4 deletions(-)

(limited to 'tools')

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index abfbd66e28..ea93b369ee 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -753,7 +753,7 @@ VDFILE_FLAGS:=$(if @PROJECT_FILE@,-f @PROJECT_FILE@,) $(CMDLINE_COQLIBS) $(CMDLI
 
 $(VDFILE): $(VFILES)
 	$(SHOW)'COQDEP VFILES'
-	$(HIDE)$(COQDEP) -dyndep var $(VDFILE_FLAGS) $(redir_if_ok)
+	$(HIDE)$(COQDEP) -vos -dyndep var $(VDFILE_FLAGS) $(redir_if_ok)
 
 # Misc ########################################################################
 
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 6f81be475b..b9a8601d10 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -486,6 +486,7 @@ let rec parse = function
   | "-w" :: ll -> option_w := true; parse ll
   | "-boot" :: ll -> option_boot := true; parse ll
   | "-sort" :: ll -> option_sort := true; parse ll
+  | "-vos" :: ll -> write_vos := true; parse ll
   | ("-noglob" | "-no-glob") :: ll -> option_noglob := true; parse ll
   | "-f" :: f :: ll -> treat_coqproject f; parse ll
   | "-I" :: r :: ll -> add_caml_dir r; parse ll
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index ddedec12f8..c5f38e716e 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -517,6 +517,8 @@ let mL_dependencies () =
        printf "%!")
     (List.rev !mlpackAccu)
 
+let write_vos = ref false
+
 let coq_dependencies () =
   List.iter
     (fun (name,_) ->
@@ -526,9 +528,10 @@ let coq_dependencies () =
        printf "%s%s%s %s.v.beautified %s.required_vo: %s.v %s\n" ename !suffixe glob ename ename ename
         (string_of_dependency_list !suffixe deps);
        printf "%s.vio: %s.v %s\n" ename ename
-        (string_of_dependency_list ".vio" deps);
-       printf "%s.vos %s.vok %s.required_vos: %s.v %s\n" ename ename ename ename
-        (string_of_dependency_list ".vos" deps);
+         (string_of_dependency_list ".vio" deps);
+       if !write_vos then
+         printf "%s.vos %s.vok %s.required_vos: %s.v %s\n" ename ename ename ename
+           (string_of_dependency_list ".vos" deps);
        printf "%!")
     (List.rev !vAccu)
 
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index e450d0e36f..6d49f7e06c 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -24,6 +24,9 @@ val option_c : bool ref
 val option_noglob : bool ref
 val option_boot : bool ref
 
+val write_vos : bool ref
+(** output vos and vok dependencies *)
+
 type dynlink = Opt | Byte | Both | No | Variable
 
 val option_dynlink : dynlink ref
-- 
cgit v1.2.3