diff --git a/test-suite/misc/coqdep-require-filter-categories.sh b/test-suite/misc/coqdep-require-filter-categories.sh index 4ca500b9fd3f..7d378af958b3 100755 --- a/test-suite/misc/coqdep-require-filter-categories.sh +++ b/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 diff --git a/test-suite/misc/external-deps.sh b/test-suite/misc/external-deps.sh index 6c3c6fff58be..211814827d3c 100755 --- a/test-suite/misc/external-deps.sh +++ b/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 diff --git a/test-suite/misc/external-deps/file1.notfound.error.deps b/test-suite/misc/external-deps/file1.notfound.error.deps new file mode 100644 index 000000000000..84a16e9b12bd --- /dev/null +++ b/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] diff --git a/test-suite/misc/external-deps/file1.notfound.deps b/test-suite/misc/external-deps/file1.notfound.warn.deps similarity index 100% rename from test-suite/misc/external-deps/file1.notfound.deps rename to test-suite/misc/external-deps/file1.notfound.warn.deps diff --git a/test-suite/misc/external-deps/file2.notfound.error.deps b/test-suite/misc/external-deps/file2.notfound.error.deps new file mode 100644 index 000000000000..5e5cea300c09 --- /dev/null +++ b/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] diff --git a/test-suite/misc/external-deps/file2.notfound.deps b/test-suite/misc/external-deps/file2.notfound.warn.deps similarity index 100% rename from test-suite/misc/external-deps/file2.notfound.deps rename to test-suite/misc/external-deps/file2.notfound.warn.deps diff --git a/tools/coqdep/lib/args.ml b/tools/coqdep/lib/args.ml index 31ebca9875cd..f687f4d5227b 100644 --- a/tools/coqdep/lib/args.ml +++ b/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 () = diff --git a/tools/coqdep/lib/common.ml b/tools/coqdep/lib/common.ml index dc57ea4faa4e..f7655cb2b1ea 100644 --- a/tools/coqdep/lib/common.ml +++ b/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 ->