Commit e787c13c authored by Ralf Jung's avatar Ralf Jung

also test the output of error messages

parent 5dfd8acd
...@@ -7,11 +7,13 @@ TESTFILES=$(wildcard tests/*.v) ...@@ -7,11 +7,13 @@ TESTFILES=$(wildcard tests/*.v)
test: $(TESTFILES:.v=.vo) test: $(TESTFILES:.v=.vo)
.PHONY: test .PHONY: test
COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
$(TESTFILES:.v=.vo): %.vo: %.v $(VFILES:.v=.vo) $(TESTFILES:.v=.vo): %.vo: %.v $(VFILES:.v=.vo)
$(SHOW)COQC [test] $< $(SHOW)COQTOP [test] $<
$(HIDE)TEST="$$(basename -s .v $<)" && \ $(HIDE)TEST="$$(basename -s .v $<)" && \
TMPFILE="$$(mktemp)" && \ 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)) && \ (diff -u "tests/$$TEST.ref" "$$TMPFILE" || (rm "tests/$$TEST.vo" "$$TMPFILE" && exit 1)) && \
rm "$$TMPFILE" rm "$$TMPFILE"
...@@ -20,6 +22,6 @@ ref: $(TESTFILES:.v=.ref) ...@@ -20,6 +22,6 @@ ref: $(TESTFILES:.v=.ref)
.PHONY: ref .PHONY: ref
tests/%.ref: tests/%.v $(VFILES:.v=.vo) tests/%.ref: tests/%.v $(VFILES:.v=.vo)
$(SHOW)COQC [ref] $< $(SHOW)COQTOP [ref] $<
$(HIDE)TEST="$$(basename -s .v $<)" && \ $(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"
...@@ -31,6 +31,39 @@ ...@@ -31,6 +31,39 @@
--------------------------------------□ --------------------------------------□
<affine> (P ∗ Q) <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 1 subgoal
PROP : sbi PROP : sbi
...@@ -151,3 +184,22 @@ ...@@ -151,3 +184,22 @@
={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
={E1,E2}=∗ 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.
...@@ -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 ...@@ -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 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. - True.
Proof. Proof.
iIntros "HP". Show. iIntros "HP". Show. Undo. iIntros "?". 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.
Abort. Abort.
(* This is specifically crafted such that not having the printing box in (* 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) ...@@ -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 }} 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. - True.
Proof. Proof.
iIntros "HP". Show. iIntros "HP". Show. Undo. iIntros "?". 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.
Abort. Abort.
Lemma long_impl (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) : Lemma long_impl (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
...@@ -560,3 +547,28 @@ Abort. ...@@ -560,3 +547,28 @@ Abort.
End linebreaks. End linebreaks.
End printing_tests. 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.
...@@ -107,6 +107,24 @@ ...@@ -107,6 +107,24 @@
--------------------------------------∗ --------------------------------------∗
|={⊤}=> na_own t E1 ∗ na_own t E2 ∗ ▷ P |={⊤}=> 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 1 subgoal
Σ : gFunctors Σ : gFunctors
......
...@@ -57,3 +57,8 @@ ...@@ -57,3 +57,8 @@
--------------------------------------∗ --------------------------------------∗
∀ _ : (), ∃ _ : (), emp ∀ _ : (), ∃ _ : (), 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).
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment