From 4e9bc09df64cd15e85c19ecabbc9580c00771176 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 6 Nov 2018 11:33:09 +0100
Subject: [CoqProject] Abstract warning function for CoqProject readers.

`CoqProject_file` uses the feedback system, however this is not very
convenient in some scenarios such as `coqdep` that has to be run very
early in the build process [and thus in "boot" mode].

We thus make the warning function a paramater.

Should fix #8913.
---
 tools/coq_makefile.ml | 5 +++--
 tools/coqdep.ml       | 3 ++-
 2 files changed, 5 insertions(+), 3 deletions(-)

(limited to 'tools')

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index ca5a232edb..8560bac786 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -396,8 +396,9 @@ let _ =
     | "-destination-of" :: tgt :: rest -> Some tgt, rest
     | _ -> None, args in
 
-  let project = 
-    try cmdline_args_to_project ~curdir:Filename.current_dir_name args
+  let project =
+    let warning_fn x = Format.eprintf "%s@\n%!" x in
+    try cmdline_args_to_project ~warning_fn ~curdir:Filename.current_dir_name args
     with Parsing_error s -> prerr_endline s; usage_coq_makefile () in
 
   if only_destination <> None then begin
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index ba88069be9..226a19678f 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -473,7 +473,8 @@ let add_r_include path l = add_rec_dir_import add_known path (split_period l)
 let treat_coqproject f =
   let open CoqProject_file in
   let iter_sourced f = List.iter (fun {thing} -> f thing) in
-  let project = read_project_file f in
+  let warning_fn x = coqdep_warning "%s" x in
+  let project = read_project_file ~warning_fn f in
   iter_sourced (fun { path } -> add_caml_dir path) project.ml_includes;
   iter_sourced (fun ({ path }, l) -> add_q_include path l) project.q_includes;
   iter_sourced (fun ({ path }, l) -> add_r_include path l) project.r_includes;
-- 
cgit v1.2.3