diff options
| author | Gaëtan Gilbert | 2019-11-08 11:36:22 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-11-08 11:36:22 +0100 |
| commit | 6930dd3533e7829184daa4cd8a84be62d9886c77 (patch) | |
| tree | 78600ee4e921af2ebaf67dd42e9cb6594f52745c /tools | |
| parent | 4658804c1f5d9c89f23e2c31a44643ed4569f9fe (diff) | |
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.
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 2 | ||||
| -rw-r--r-- | tools/coqdep.ml | 1 | ||||
| -rw-r--r-- | tools/coqdep_common.ml | 9 | ||||
| -rw-r--r-- | tools/coqdep_common.mli | 3 |
4 files changed, 11 insertions, 4 deletions
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 |