diff options
| author | coqbot-app[bot] | 2021-04-13 14:10:33 +0000 |
|---|---|---|
| committer | GitHub | 2021-04-13 14:10:33 +0000 |
| commit | ea62d1e19f2ba565ea3a18ba3709a06af5c845ac (patch) | |
| tree | 3193f7dafa0fc93c1c9b3fc8d47fcc1c2c075f6e /tools/coqdep_common.ml | |
| parent | b78e6cfcb412d1c4e5902fb895c5ecaa0cb177ac (diff) | |
| parent | e1793962bebf1401026ed961ecc15b7eb60d57f5 (diff) | |
Merge PR #14024: [coqdep] error on non-existent and unreadable files
Reviewed-by: gares
Ack-by: jfehrle
Ack-by: ejgallego
Diffstat (limited to 'tools/coqdep_common.ml')
| -rw-r--r-- | tools/coqdep_common.ml | 21 |
1 files changed, 19 insertions, 2 deletions
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 = |