[coqdep] error on non-existent and unreadable files

Print an error message and return non-zero status for
non-existing or unreadable files. Unknown options produce a
warning and are otherwise ignored.
Fixes #14023

2 files changed, 24 insertions, 3 deletions

diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index f1dbac889b..199fc4225d 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -34,7 +34,8 @@ let usage () =
   eprintf "  -boot : For coq developers, prints dependencies over coq library files (omitted by default).\n";
   eprintf "  -sort : output the given file name ordered by dependencies\n";
   eprintf "  -noglob | -no-glob : \n";
-  eprintf "  -f file : read -I, -Q, -R and filenames from _CoqProject-formatted FILE.";
+  eprintf "  -noinit : currently no effect\n";
+  eprintf "  -f file : read -I, -Q, -R and filenames from _CoqProject-formatted FILE.\n";
   eprintf "  -I dir : add (non recursively) dir to ocaml path\n";
   eprintf "  -R dir logname : add and import dir recursively to coq load path under logical name logname\n";
   eprintf "  -Q dir logname : add (recursively) and open (non recursively) dir to coq load path under logical name logname\n";
@@ -64,6 +65,7 @@ let rec parse = function
   | "-sort" :: ll -> option_sort := true; parse ll
   | "-vos" :: ll -> write_vos := true; parse ll
   | ("-noglob" | "-no-glob") :: ll -> option_noglob := true; parse ll
+  | "-noinit" :: ll -> (* do nothing *) parse ll
   | "-f" :: f :: ll -> treat_coqproject f; parse ll
   | "-I" :: r :: ll -> add_caml_dir r; parse ll
   | "-I" :: [] -> usage ()
@@ -80,6 +82,8 @@ let rec parse = function
   | "-dyndep" :: "both" :: ll -> option_dynlink := Both; parse ll
   | "-dyndep" :: "var" :: ll -> option_dynlink := Variable; parse ll
   | ("-h"|"--help"|"-help") :: _ -> usage ()
+  | opt :: ll when String.length opt > 0 && opt.[0] = '-' ->
+     coqdep_warning "unknown option %s" opt; parse ll
   | f :: ll -> treat_file None f; parse ll
   | [] -> ()
 
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index dca9291da3..a6634586f3 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -157,6 +157,18 @@ let error_cannot_parse s (i,j) =
   Printf.eprintf "File \"%s\", characters %i-%i: Syntax error\n" s i j;
   exit 1
 
+let error_cannot_stat s unix_error =
+  (* Print an arbitrary line number, such that the message matches
+     common error message pattern. *)
+  Printf.eprintf "File \"%s\", line 1: %s\n" s (error_message unix_error);
+  exit 1
+
+let error_cannot_open s msg =
+  (* Print an arbitrary line number, such that the message matches
+     common error message pattern. *)
+  Printf.eprintf "File \"%s\", line 1: %s\n" s msg;
+  exit 1
+
 let warning_module_notfound f s =
   coqdep_warning "in file %s, library %s is required and has not been found in the loadpath!"
     f (String.concat "." s)
@@ -368,7 +380,7 @@ let rec find_dependencies basename =
     | Syntax_error (i,j) ->
         close_in chan;
         error_cannot_parse f (i,j)
-  with Sys_error _ -> [] (* TODO: report an error? *)
+  with Sys_error msg -> error_cannot_open (basename ^ ".v") msg
 
 
 let write_vos = ref false
@@ -472,7 +484,12 @@ let rec treat_file old_dirname old_name =
       | (Some d1,d2) -> Some (d1//d2)
   in
   let complete_name = file_name name dirname in
-  match try (stat complete_name).st_kind with _ -> S_BLK with
+  let stat_res =
+    try stat complete_name
+    with Unix_error(error, _, _) -> error_cannot_stat complete_name error
+  in
+  match stat_res.st_kind
+  with
     | S_DIR ->
         (if name.[0] <> '.' then
            let newdirname =