coqdep warnings default AsError

test-suite/misc/coqdep-require-filter-categories.sh

@@ -5,7 +5,7 @@ set -e
 cd misc/coqdep-require-filter-categories
 
 code=0
-$coqdep -worker @ROCQWORKER@ -R . 'Bla' ./*.v > stdout 2> stderr || code=$?
+$coqdep -worker @ROCQWORKER@ -R . 'Bla' ./*.v -w module-not-found > stdout 2> stderr || code=$?
 
 diff -u stdout.ref stdout
 diff -u stderr.ref stderr

test-suite/misc/external-deps.sh

@@ -4,26 +4,58 @@ set -e
 
 # Set Extra Dependency syntax
 output=misc/external-deps/file1.found.real
-$coqdep -worker @ROCQWORKER@ -Q misc/external-deps/deps foo.bar misc/external-deps/file1.v > $output 2>&1
+if ! $coqdep -worker @ROCQWORKER@ -Q misc/external-deps/deps foo.bar misc/external-deps/file1.v > $output 2>&1; then
+  >&2 echo file1.found failed
+  exit 1
+fi
 diff -u --strip-trailing-cr misc/external-deps/file1.found.deps $output
 
 output=misc/external-deps/file1.ambiguous.real
-$coqdep -worker @ROCQWORKER@ -Q misc/external-deps/deps foo.bar -Q misc/external-deps/more foo.bar misc/external-deps/file1.v > $output 2>&1
+if ! $coqdep -worker @ROCQWORKER@ -Q misc/external-deps/deps foo.bar -Q misc/external-deps/more foo.bar misc/external-deps/file1.v > $output 2>&1; then
+  >&2 echo file1.ambiguous failed
+  exit 1
+fi
 diff -u --strip-trailing-cr misc/external-deps/file1.ambiguous.deps $output
 
-output=misc/external-deps/file1.notfound.real
-$coqdep -worker @ROCQWORKER@ misc/external-deps/file1.v > $output 2>&1
-diff -u --strip-trailing-cr misc/external-deps/file1.notfound.deps $output
+output=misc/external-deps/file1.notfound.error.real
+if $coqdep -worker @ROCQWORKER@ misc/external-deps/file1.v > $output 2>&1; then
+  >&2 echo file1.notfound.error did not fail
+  exit 1
+fi
+diff -u --strip-trailing-cr misc/external-deps/file1.notfound.error.deps $output
+
+output=misc/external-deps/file1.notfound.warn.real
+if ! $coqdep -worker @ROCQWORKER@ misc/external-deps/file1.v -w module-not-found > $output 2>&1; then
+  >&2 echo file1.warn failed
+  exit 1
+fi
+diff -u --strip-trailing-cr misc/external-deps/file1.notfound.warn.deps $output
 
 # From bla Extra Dependency syntax
 output=misc/external-deps/file2.found.real
-$coqdep -worker @ROCQWORKER@ -Q misc/external-deps/deps foo.bar misc/external-deps/file2.v > $output 2>&1
+if ! $coqdep -worker @ROCQWORKER@ -Q misc/external-deps/deps foo.bar misc/external-deps/file2.v > $output 2>&1; then
+  >&2 echo file1.found failed
+  exit 1
+fi
 diff -u --strip-trailing-cr misc/external-deps/file2.found.deps $output
 
 output=misc/external-deps/file2.ambiguous.real
-$coqdep -worker @ROCQWORKER@ -Q misc/external-deps/deps foo.bar -Q misc/external-deps/more foo.bar misc/external-deps/file2.v > $output 2>&1
+if ! $coqdep -worker @ROCQWORKER@ -Q misc/external-deps/deps foo.bar -Q misc/external-deps/more foo.bar misc/external-deps/file2.v > $output 2>&1; then
+  >&2 echo file1.ambiguous failed
+  exit 1
+fi
 diff -u --strip-trailing-cr misc/external-deps/file2.ambiguous.deps $output
 
-output=misc/external-deps/file2.notfound.real
-$coqdep -worker @ROCQWORKER@ misc/external-deps/file2.v > $output 2>&1
-diff -u --strip-trailing-cr misc/external-deps/file2.notfound.deps $output
+output=misc/external-deps/file2.notfound.error.real
+if $coqdep -worker @ROCQWORKER@ misc/external-deps/file2.v > $output 2>&1; then
+  >&2 echo file2.notfound.error did not fail
+  exit 1
+fi
+diff -u --strip-trailing-cr misc/external-deps/file2.notfound.error.deps $output
+
+output=misc/external-deps/file2.notfound.warn.real
+if ! $coqdep -worker @ROCQWORKER@ misc/external-deps/file2.v -w module-not-found > $output 2>&1; then
+  >&2 echo file2.notfound.warn failed
+  exit 1
+fi
+diff -u --strip-trailing-cr misc/external-deps/file2.notfound.warn.deps $output

test-suite/misc/external-deps/file1.notfound.error.deps

@@ -0,0 +1,4 @@
+File "misc/external-deps/file1.v", line 2, characters 51-55:
+Error: external file d1 is required
+from root foo.bar and has not been found in the loadpath!
+[module-not-found,filesystem,default]

test-suite/misc/external-deps/file2.notfound.error.deps

@@ -0,0 +1,4 @@
+File "misc/external-deps/file2.v", line 1, characters 30-34:
+Error: external file d1 is required
+from root foo.bar and has not been found in the loadpath!
+[module-not-found,filesystem,default]

tools/coqdep/lib/args.ml

@@ -38,7 +38,7 @@ let make () =
 
 
 let warn_unknown_option =
-  CWarnings.create ~name:"unknown-option"
+  CWarnings.create ~name:"unknown-option" ~default:AsError
     Pp.(fun opt -> str "Unknown option \"" ++ str opt ++ str "\".")
 
 let usage () =

tools/coqdep/lib/common.ml

@@ -66,14 +66,13 @@ type what = Library | External
 let str_of_what = function Library -> "library" | External -> "external file"
 
 let warning_module_notfound =
-  let warn (what, from, s) =
-    let open Pp in
-    str (str_of_what what) ++ spc () ++ str (String.concat "." s) ++ str " is required" ++
-    pr_opt (fun pth -> str "from root " ++ str (String.concat "." pth)) from ++
-    str " and has not been found in the loadpath!"
-  in
   CWarnings.create ~name:"module-not-found"
-    ~category:CWarnings.CoreCategories.filesystem warn
+    ~category:CWarnings.CoreCategories.filesystem
+    ~default:AsError
+    Pp.(fun (what, from, s) ->
+        str (str_of_what what) ++ spc () ++ str (String.concat "." s) ++ str " is required" ++
+        pr_opt (fun pth -> str "from root " ++ str (String.concat "." pth)) from ++
+        str " and has not been found in the loadpath!")
 
 let warn_if_clash ?(what=Library) exact file dir f1 = function
   | f2::fl ->