diff options
| author | Emilio Jesus Gallego Arias | 2019-11-20 00:12:12 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-11-20 00:12:12 +0100 |
| commit | 5d10145531b2920f5e7b9d47bc15b5de06783d97 (patch) | |
| tree | 559f9e29c74daceb530495ee01769490ff753114 | |
| parent | 69978e0a33d555392fd8a3d7802d28188dd6238b (diff) | |
| parent | 6930dd3533e7829184daa4cd8a84be62d9886c77 (diff) | |
Merge PR #11074: coqdep: only output vos when passed -vos
Reviewed-by: ejgallego
Reviewed-by: gares
| -rw-r--r-- | Makefile.build | 2 | ||||
| -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 |
5 files changed, 12 insertions, 5 deletions
diff --git a/Makefile.build b/Makefile.build index b63d582740..ff0e5dbaea 100644 --- a/Makefile.build +++ b/Makefile.build @@ -897,7 +897,7 @@ endif $(VDFILE).d: $(D_DEPEND_BEFORE_SRC) $(VFILES) $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(SHOW)'COQDEP VFILES' - $(HIDE)$(COQDEPBOOT) -boot $(DYNDEP) -Q user-contrib "" $(USERCONTRIBINCLUDES) $(VFILES) $(TOTARGET) + $(HIDE)$(COQDEPBOOT) -vos -boot $(DYNDEP) -Q user-contrib "" $(USERCONTRIBINCLUDES) $(VFILES) $(TOTARGET) ########################################################################### 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 |