[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

4 files changed, 47 insertions, 3 deletions

diff --git a/doc/changelog/08-cli-tools/14024-coqdep-errors.rst b/doc/changelog/08-cli-tools/14024-coqdep-errors.rst
new file mode 100644
index 0000000000..355c0bd7b7
--- /dev/null
+++ b/doc/changelog/08-cli-tools/14024-coqdep-errors.rst
@@ -0,0 +1,8 @@
+- **Changed:**
+  ``coqdep`` now reports an error if files specified on the
+  command line don't exist or if it encounters unreadable files.
+  Unknown options now generate a warning. Previously these
+  conditions were ignored.
+  (`#14024 <https://github.com/coq/coq/pull/14024>`_,
+  fixes `#14023 <https://github.com/coq/coq/issues/14023>`_,
+  by Hendrik Tews).
diff --git a/man/coqdep.1 b/man/coqdep.1
index bb6b20c0bb..5ca558b7c5 100644
--- a/man/coqdep.1
+++ b/man/coqdep.1
@@ -70,6 +70,21 @@ Output dependencies for .vos files (this is not the default as it breaks dune's
 .B \-boot
 For coq developers, prints dependencies over coq library files
 (omitted by default).
+.TP
+.B \-noinit
+Currently no effect.
+
+
+.SH EXIT STATUS
+.IP "1"
+A file given on the command line cannot be found or some file
+cannot be opened.
+.IP "0"
+In all other cases. In particular, when a dependency cannot be
+found or an invalid option is encountered,
+.B coqdep
+prints a warning and exits with status
+.B 0\fR.
 
 
 .SH SEE ALSO
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 =