Commit 859871ab authored by Ralf Jung's avatar Ralf Jung

move test suite out of theories/ so it does not get installed; also check...

move test suite out of theories/ so it does not get installed; also check output of test suite so that we can test printing
parent 032ee4a5
......@@ -33,7 +33,7 @@ build-dep: build-dep/opam phony
@# dependencies, but does not actually install anything.
@# Reinstalling is needed with opam 1 in case the pin already exists, but the builddep
@# package changed.
@BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')"; \
@BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
echo "# Pinning build-dep package." && \
opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
((! opam --version | grep "^1\." > /dev/null) || ( \
......
# run tests after real-all
post-all:: test
# the test suite
TESTFILES=$(wildcard tests/*.v)
test: $(TESTFILES:.v=.vo)
.PHONY: test
$(TESTFILES:.v=.vo): %.vo: %.v $(VFILES:.v=.vo)
$(SHOW)COQC [test] $<
$(HIDE)TEST="$$(basename -s .v $<)" && \
TMPFILE="$$(tempfile -p test- -s "-$$TEST")" && \
$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $< $(TIMING_EXTRA) > "$$TMPFILE" && \
diff --color=auto -u "tests/$$TEST.ref" "$$TMPFILE"
# a target, for convenience sake, to create the .ref file with the current output
ref: $(TESTFILES:.v=.ref)
.PHONY: ref
tests/%.ref: tests/%.v $(VFILES:.v=.vo)
$(SHOW)COQC [ref] $<
$(HIDE)TEST="$$(basename -s .v $<)" && \
$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $< $(TIMING_EXTRA) > "tests/$$TEST.ref"
......@@ -109,12 +109,3 @@ theories/proofmode/frame_instances.v
theories/proofmode/monpred.v
theories/proofmode/modalities.v
theories/proofmode/modality_instances.v
theories/tests/heap_lang.v
theories/tests/one_shot.v
theories/tests/proofmode.v
theories/tests/proofmode_iris.v
theories/tests/proofmode_monpred.v
theories/tests/list_reverse.v
theories/tests/tree_sum.v
theories/tests/ipm_paper.v
theories/tests/algebra.v
1 subgoal
Σ : gFunctors
H : heapG Σ
E : coPset
============================
--------------------------------------∗
WP let: "x" := ref #1 in "x" <- ! "x" + #1;; ! "x" @ E {{ v, ⌜v = #2⌝ }}
1 subgoal
Σ : gFunctors
H : heapG Σ
E : coPset
l : loc
============================
_ : l ↦ #1
--------------------------------------∗
WP #l <- #1 + #1;; ! #l @ E {{ v, ⌜v = #2⌝ }}
......@@ -25,8 +25,9 @@ Section LiftingTests.
Lemma heap_e_spec E : WP heap_e @ E {{ v, v = #2 }}%I.
Proof.
iIntros "". rewrite /heap_e.
wp_alloc l. wp_let. wp_load. wp_op. wp_store. by wp_load.
iIntros "". rewrite /heap_e. Show.
wp_alloc l. wp_let. wp_load. Show.
wp_op. wp_store. by wp_load.
Qed.
Definition heap_e2 : expr :=
......
1 subgoal
PROP : sbi
P, Q : PROP
============================
"H2" : ∀ x : nat, ⌜x = 0⌝ ∨ ⌜x = 1⌝
--------------------------------------□
"H" : □ (P ∨ Q)
--------------------------------------∗
Q ∨ P
1 subgoal
PROP : sbi
P, Q : PROP
============================
"H2" : ∀ x : nat, ⌜x = 0⌝ ∨ ⌜x = 1⌝
_ : P
--------------------------------------□
Q ∨ P
......@@ -8,9 +8,9 @@ Implicit Types P Q R : PROP.
Lemma demo_0 P Q : (P Q) - ( x, x = 0 x = 1) (Q P).
Proof.
iIntros "H #H2". iDestruct "H" as "###H".
iIntros "H #H2". Show. iDestruct "H" as "###H".
(* should remove the disjunction "H" *)
iDestruct "H" as "[#?|#?]"; last by iLeft.
iDestruct "H" as "[#?|#?]"; last by iLeft. Show.
(* should keep the disjunction "H" because it is instantiated *)
iDestruct ("H2" $! 10) as "[%|%]". done. done.
Qed.
......
1 subgoal
Σ : gFunctors
H : invG Σ
H0 : cinvG Σ
H1 : na_invG Σ
N : namespace
P : uPredI (iResUR Σ)
============================
"H" : inv N (<pers> P)%I
"H2" : ▷ <pers> P
--------------------------------------□
|={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> ▷ P)
1 subgoal
Σ : gFunctors
H : invG Σ
H0 : cinvG Σ
H1 : na_invG Σ
N : namespace
P : uPredI (iResUR Σ)
============================
"H" : inv N (<pers> P)%I
"H2" : ▷ <pers> P
--------------------------------------□
"Hclose" : ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp
--------------------------------------∗
|={⊤ ∖ ↑N,⊤}=> ▷ P
1 subgoal
Σ : gFunctors
H : invG Σ
H0 : cinvG Σ
H1 : na_invG Σ
γ : gname
p : Qp
N : namespace
P : uPredI (iResUR Σ)
============================
_ : cinv N γ (<pers> P)%I
"HP" : ▷ <pers> P
--------------------------------------□
"Hown" : cinv_own γ p
--------------------------------------∗
|={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> cinv_own γ p ∗ ▷ P)
1 subgoal
Σ : gFunctors
H : invG Σ
H0 : cinvG Σ
H1 : na_invG Σ
γ : gname
p : Qp
N : namespace
P : uPredI (iResUR Σ)
============================
_ : cinv N γ (<pers> P)%I
"HP" : ▷ <pers> P
--------------------------------------□
"Hown" : cinv_own γ p
"Hclose" : ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp
--------------------------------------∗
|={⊤ ∖ ↑N,⊤}=> cinv_own γ p ∗ ▷ P
1 subgoal
Σ : gFunctors
H : invG Σ
H0 : cinvG Σ
H1 : na_invG Σ
t : na_inv_pool_name
N : namespace
E1, E2 : coPset
P : uPredI (iResUR Σ)
H2 : ↑N ⊆ E2
============================
_ : na_inv t N (<pers> P)%I
"HP" : ▷ <pers> P
--------------------------------------□
"Hown1" : na_own t E1
"Hown2" : na_own t (E2 ∖ ↑N)
--------------------------------------∗
|={⊤}=> (▷ <pers> P ∗ na_own t (E2 ∖ ↑N))
∗ (na_own t E2 ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P)
1 subgoal
Σ : gFunctors
H : invG Σ
H0 : cinvG Σ
H1 : na_invG Σ
t : na_inv_pool_name
N : namespace
E1, E2 : coPset
P : uPredI (iResUR Σ)
H2 : ↑N ⊆ E2
============================
_ : na_inv t N (<pers> P)%I
"HP" : ▷ <pers> P
--------------------------------------□
"Hown1" : na_own t E1
"Hown2" : na_own t (E2 ∖ ↑N)
"Hclose" : ▷ <pers> P ∗ na_own t (E2 ∖ ↑N) ={⊤}=∗
id (na_own t E2)
--------------------------------------∗
|={⊤}=> na_own t E1 ∗ na_own t E2 ∗ ▷ P
......@@ -63,14 +63,14 @@ Section iris_tests.
Lemma test_iInv_0 N P: inv N (<pers> P) ={}= P.
Proof.
iIntros "#H".
iInv N as "#H2".
iInv N as "#H2". Show.
iModIntro. iSplit; auto.
Qed.
Lemma test_iInv_0_with_close N P: inv N (<pers> P) ={}= P.
Proof.
iIntros "#H".
iInv N as "#H2" "Hclose".
iInv N as "#H2" "Hclose". Show.
iMod ("Hclose" with "H2").
iModIntro. by iNext.
Qed.
......@@ -88,7 +88,7 @@ Section iris_tests.
cinv N γ (<pers> P) cinv_own γ p ={}= cinv_own γ p P.
Proof.
iIntros "(#?&?)".
iInv N as "(#HP&Hown)".
iInv N as "(#HP&Hown)". Show.
iModIntro. iSplit; auto with iFrame.
Qed.
......@@ -96,7 +96,7 @@ Section iris_tests.
cinv N γ (<pers> P) cinv_own γ p ={}= cinv_own γ p P.
Proof.
iIntros "(#?&?)".
iInv N as "(#HP&Hown)" "Hclose".
iInv N as "(#HP&Hown)" "Hclose". Show.
iMod ("Hclose" with "HP").
iModIntro. iFrame. by iNext.
Qed.
......@@ -116,7 +116,7 @@ Section iris_tests.
|={}=> na_own t E1 na_own t E2 P.
Proof.
iIntros (?) "(#?&Hown1&Hown2)".
iInv N as "(#HP&Hown2)".
iInv N as "(#HP&Hown2)". Show.
iModIntro. iSplitL "Hown2"; auto with iFrame.
Qed.
......@@ -126,7 +126,7 @@ Section iris_tests.
|={}=> na_own t E1 na_own t E2 P.
Proof.
iIntros (?) "(#?&Hown1&Hown2)".
iInv N as "(#HP&Hown2)" "Hclose".
iInv N as "(#HP&Hown2)" "Hclose". Show.
iMod ("Hclose" with "[HP Hown2]").
{ iFrame. done. }
iModIntro. iFrame. by iNext.
......
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