From e787c13c088ec955eaeb3d804831fbf106454989 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 10 Jun 2018 22:05:59 +0200
Subject: [PATCH] also test the output of error messages
---
Makefile.coq.local | 10 ++++---
tests/proofmode.ref | 52 +++++++++++++++++++++++++++++++++++++
tests/proofmode.v | 42 +++++++++++++++++++-----------
tests/proofmode_iris.ref | 18 +++++++++++++
tests/proofmode_monpred.ref | 5 ++++
5 files changed, 108 insertions(+), 19 deletions(-)
diff --git a/Makefile.coq.local b/Makefile.coq.local
index 196539e92..d8617a604 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -7,11 +7,13 @@ TESTFILES=$(wildcard tests/*.v)
test: $(TESTFILES:.v=.vo)
.PHONY: test
+COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
+
$(TESTFILES:.v=.vo): %.vo: %.v $(VFILES:.v=.vo)
- $(SHOW)COQC [test] $<
+ $(SHOW)COQTOP [test] $<
$(HIDE)TEST="$$(basename -s .v $<)" && \
TMPFILE="$$(mktemp)" && \
- $(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $< $(TIMING_EXTRA) > "$$TMPFILE" && \
+ $(TIMER) $(COQ_TEST) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< $(TIMING_EXTRA) > "$$TMPFILE" && \
(diff -u "tests/$$TEST.ref" "$$TMPFILE" || (rm "tests/$$TEST.vo" "$$TMPFILE" && exit 1)) && \
rm "$$TMPFILE"
@@ -20,6 +22,6 @@ ref: $(TESTFILES:.v=.ref)
.PHONY: ref
tests/%.ref: tests/%.v $(VFILES:.v=.vo)
- $(SHOW)COQC [ref] $<
+ $(SHOW)COQTOP [ref] $<
$(HIDE)TEST="$$(basename -s .v $<)" && \
- $(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $< $(TIMING_EXTRA) > "tests/$$TEST.ref"
+ $(TIMER) $(COQ_TEST) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< $(TIMING_EXTRA) > "tests/$$TEST.ref"
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 558ea48ba..3460e251b 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -31,6 +31,39 @@
--------------------------------------â–¡
<affine> (P ∗ Q)
+The command has indeed failed with message:
+Ltac call to "done" failed.
+No applicable tactic.
+The command has indeed failed with message:
+In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and
+"iElaborateSelPat_go", last call failed.
+Tactic failure: iElaborateSelPat: (INamed "HQ") not found.
+The command has indeed failed with message:
+In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and
+"iElaborateSelPat_go", last call failed.
+Tactic failure: iElaborateSelPat: (INamed "HQ") not found.
+The command has indeed failed with message:
+In nested Ltac calls to "iSpecialize (open_constr)",
+"iSpecializeCore (open_constr) as (constr)",
+"iSpecializeCore (open_constr) as (constr)",
+"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
+"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
+failed.
+Tactic failure: iSpecialize: cannot instantiate (∀ _ : φ, P -∗ False)%I with
+P.
+The command has indeed failed with message:
+In nested Ltac calls to "iSpecialize (open_constr)",
+"iSpecializeCore (open_constr) as (constr)",
+"iSpecializeCore (open_constr) as (constr)",
+"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
+"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
+failed.
+Tactic failure: iSpecialize: cannot instantiate (⌜φ⌠→ P -∗ False)%I with P.
+The command has indeed failed with message:
+In nested Ltac calls to "iFrame (constr)",
+"<iris.proofmode.ltac_tactics.iFrame_go>" and
+"<iris.proofmode.ltac_tactics.iFrameHyp>", last call failed.
+Tactic failure: iFrame: cannot frame Q.
1 subgoal
PROP : sbi
@@ -151,3 +184,22 @@
={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
+The command has indeed failed with message:
+In nested Ltac calls to "iAlways", "iModIntro" and
+"iModIntro (uconstr)", last call failed.
+Tactic failure: iModIntro: spatial context is non-empty.
+The command has indeed failed with message:
+In nested Ltac calls to "iDestruct (open_constr) as (constr)",
+"iDestructCore (open_constr) as (constr) (tactic)" and
+"iDestructCore (open_constr) as (constr) (tactic)", last call failed.
+Tactic failure: iDestruct: (INamed "HQ") not found.
+The command has indeed failed with message:
+In nested Ltac calls to "iIntros ( (intropattern) )",
+"iIntro ( (intropattern) )" and "intros x", last call failed.
+x is already used.
+The command has indeed failed with message:
+Ltac call to "iSplitL (constr)" failed.
+Tactic failure: iSplitL: hypotheses ["HPx"] not found.
+The command has indeed failed with message:
+Ltac call to "iSplitL (constr)" failed.
+Tactic failure: iSplitL: hypotheses ["HPx"] not found.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 2c340bc11..2359d047a 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -499,14 +499,7 @@ Lemma print_long_line (P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PRO
P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
-∗ True.
Proof.
- iIntros "HP". Show.
-Abort.
-Lemma print_long_line_anon (P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP) :
- P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P ∗
- P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
- -∗ True.
-Proof.
- iIntros "?". Show.
+ iIntros "HP". Show. Undo. iIntros "?". Show.
Abort.
(* This is specifically crafted such that not having the printing box in
@@ -517,13 +510,7 @@ Lemma print_long_line (P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP)
TESTNOTATION {{ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P | P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P }}
-∗ True.
Proof.
- iIntros "HP". Show.
-Abort.
-Lemma print_long_line_anon (P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP) :
- TESTNOTATION {{ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P | P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P }}
- -∗ True.
-Proof.
- iIntros "?". Show.
+ iIntros "HP". Show. Undo. iIntros "?". Show.
Abort.
Lemma long_impl (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
@@ -560,3 +547,28 @@ Abort.
End linebreaks.
End printing_tests.
+
+(** Test error messages *)
+Section error_tests.
+Context {PROP : sbi}.
+Implicit Types P Q R : PROP.
+
+Lemma iAlways_spatial_non_empty P :
+ P -∗ □ emp.
+Proof. iIntros "HP". Fail iAlways. Abort.
+
+Lemma iDestruct_bad_name P :
+ P -∗ P.
+Proof. iIntros "HP". Fail iDestruct "HQ" as "HP". Abort.
+
+Lemma iIntros_dup_name P :
+ P -∗ ∀ x y : (), P.
+Proof. iIntros "HP" (x). Fail iIntros (x). Abort.
+
+Lemma iSplit_one_of_many P :
+ P -∗ P -∗ P ∗ P.
+Proof.
+ iIntros "HP1 HP2". Fail iSplitL "HP1 HPx". Fail iSplitL "HPx HP1".
+Abort.
+
+End error_tests.
diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
index 735cba70f..eaaf26845 100644
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -107,6 +107,24 @@
--------------------------------------∗
|={⊤}=> na_own t E1 ∗ na_own t E2 ∗ ▷ P
+The command has indeed failed with message:
+In nested Ltac calls to "iInv (constr) as (constr)",
+"iInvCore (constr) in (tactic)" and
+"iInvCore (constr) with (constr) as (open_constr) in (tactic)", last call
+failed.
+Tactic failure: iInv: selector 34 is not of the right type .
+The command has indeed failed with message:
+In nested Ltac calls to "iInv (constr) as (constr)",
+"iInvCore (constr) in (tactic)" and
+"iInvCore (constr) with (constr) as (open_constr) in (tactic)", last call
+failed.
+Tactic failure: iInv: invariant nroot not found.
+The command has indeed failed with message:
+In nested Ltac calls to "iInv (constr) as (constr)",
+"iInvCore (constr) in (tactic)" and
+"iInvCore (constr) with (constr) as (open_constr) in (tactic)", last call
+failed.
+Tactic failure: iInv: invariant "H2" not found.
1 subgoal
Σ : gFunctors
diff --git a/tests/proofmode_monpred.ref b/tests/proofmode_monpred.ref
index 39b3fb6e4..459ec829a 100644
--- a/tests/proofmode_monpred.ref
+++ b/tests/proofmode_monpred.ref
@@ -57,3 +57,8 @@
--------------------------------------∗
∀ _ : (), ∃ _ : (), emp
+The command has indeed failed with message:
+In nested Ltac calls to "iFrame (constr)",
+"<iris.proofmode.ltac_tactics.iFrame_go>" and
+"<iris.proofmode.ltac_tactics.iFrameHyp>", last call failed.
+Tactic failure: iFrame: cannot frame (P i).
--
GitLab