diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/dune | 8 | ||||
| -rw-r--r-- | test-suite/ltac2/compat.v | 13 | ||||
| -rwxr-xr-x | test-suite/misc/printers.sh | 16 |
3 files changed, 35 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/ltac2/compat.v b/test-suite/ltac2/compat.v index 489fa638e4..9c11d19c27 100644 --- a/test-suite/ltac2/compat.v +++ b/test-suite/ltac2/compat.v @@ -27,6 +27,19 @@ Fail Ltac2 bar nay := ltac1:(discriminate nay). Fail Ltac2 pose1 (v : constr) := ltac1:(pose $v). +(** Variables explicitly crossing the boundary must satisfy typing properties *) +Goal True. +Proof. +(* Wrong type *) +Fail ltac1:(x |- idtac) 0. +(* OK, and runtime has access to variable *) +ltac1:(x |- idtac x) (Ltac1.of_constr constr:(Type)). + +(* Same for ltac1val *) +Fail Ltac1.run (ltac1val:(x |- idtac) 0). +Ltac1.run (ltac1val:(x |- idtac x) (Ltac1.of_constr constr:(Type))). +Abort. + (** Test calls to Ltac2 from Ltac1 *) Set Default Proof Mode "Classic". 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 |