diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/dune | 8 | ||||
| -rwxr-xr-x | test-suite/misc/printers.sh | 16 |
2 files changed, 22 insertions, 2 deletions
diff --git a/test-suite/dune b/test-suite/dune index 041c181d66..6ab2988331 100644 --- a/test-suite/dune +++ b/test-suite/dune @@ -20,6 +20,14 @@ ../dev/header.ml ../dev/tools/update-compat.py ../doc/stdlib/index-list.html.template + ; For the misc/printers.sh test + ../dev/incdir_dune + ../dev/base_include + ../dev/inc_ltac_dune + ../dev/include_printers + ../dev/include_dune + ../dev/top_printers.ml + ../dev/vm_printers.ml ; For the changelog test ../config/coq_config.py (source_tree doc/changelog) diff --git a/test-suite/misc/printers.sh b/test-suite/misc/printers.sh index f659fce680..f2bf6b8681 100755 --- a/test-suite/misc/printers.sh +++ b/test-suite/misc/printers.sh @@ -3,6 +3,18 @@ command -v "${BIN}coqtop.byte" || { echo "Missing coqtop.byte"; exit 1; } f=$(mktemp) -printf 'Drop. #use"include";; #quit;;\n' | "${BIN}coqtop.byte" -q 2>&1 | tee "$f" +{ + if [ -n "$INSIDE_DUNE" ]; then + printf 'Drop.\n#directory "../dev";;\n#use "include_dune";;\n#quit;;\n' | coqtop.byte -q + else + # -I ../dev is not needed when compiled with -local (usual dev + # setup), but is needed for CI testing. + printf 'Drop. #use "include";; #quit;;\n' | "${BIN}coqtop.byte" -I ../dev -q + fi +} 2>&1 | tee "$f" -if grep -q -E "Error|Unbound" "$f"; then exit 1; fi +# if there's an issue in base_include 'go' won't be defined +# if there's an issue in include_printers it will be an undefined printer +if ! grep -q -F 'val go : unit -> unit = <fun>' "$f" || + grep -q -E "Error|Unbound" "$f"; +then exit 1; fi |