From 859871ab6302cf9db4bd857714edecc0f919ddb4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 17 May 2018 15:25:28 +0200
Subject: [PATCH] move test suite out of theories/ so it does not get
installed; also check output of test suite so that we can test printing
---
Makefile | 2 +-
Makefile.coq.local | 24 ++++
_CoqProject | 9 --
tests/algebra.ref | 0
{theories/tests => tests}/algebra.v | 0
tests/heap_lang.ref | 20 ++++
{theories/tests => tests}/heap_lang.v | 5 +-
tests/ipm_paper.ref | 0
{theories/tests => tests}/ipm_paper.v | 0
tests/list_reverse.ref | 0
{theories/tests => tests}/list_reverse.v | 0
tests/one_shot.ref | 0
{theories/tests => tests}/one_shot.v | 0
tests/proofmode.ref | 21 ++++
{theories/tests => tests}/proofmode.v | 4 +-
tests/proofmode_iris.ref | 110 ++++++++++++++++++
{theories/tests => tests}/proofmode_iris.v | 12 +-
tests/proofmode_monpred.ref | 0
{theories/tests => tests}/proofmode_monpred.v | 0
tests/tree_sum.ref | 0
{theories/tests => tests}/tree_sum.v | 0
21 files changed, 187 insertions(+), 20 deletions(-)
create mode 100644 Makefile.coq.local
create mode 100644 tests/algebra.ref
rename {theories/tests => tests}/algebra.v (100%)
create mode 100644 tests/heap_lang.ref
rename {theories/tests => tests}/heap_lang.v (97%)
create mode 100644 tests/ipm_paper.ref
rename {theories/tests => tests}/ipm_paper.v (100%)
create mode 100644 tests/list_reverse.ref
rename {theories/tests => tests}/list_reverse.v (100%)
create mode 100644 tests/one_shot.ref
rename {theories/tests => tests}/one_shot.v (100%)
create mode 100644 tests/proofmode.ref
rename {theories/tests => tests}/proofmode.v (99%)
create mode 100644 tests/proofmode_iris.ref
rename {theories/tests => tests}/proofmode_iris.v (96%)
create mode 100644 tests/proofmode_monpred.ref
rename {theories/tests => tests}/proofmode_monpred.v (100%)
create mode 100644 tests/tree_sum.ref
rename {theories/tests => tests}/tree_sum.v (100%)
diff --git a/Makefile b/Makefile
index e089b03f5..f29d7a117 100644
--- a/Makefile
+++ b/Makefile
@@ -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) || ( \
diff --git a/Makefile.coq.local b/Makefile.coq.local
new file mode 100644
index 000000000..1f6edfecc
--- /dev/null
+++ b/Makefile.coq.local
@@ -0,0 +1,24 @@
+# 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"
diff --git a/_CoqProject b/_CoqProject
index aa2bb70a7..ead8fc22c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -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
diff --git a/tests/algebra.ref b/tests/algebra.ref
new file mode 100644
index 000000000..e69de29bb
diff --git a/theories/tests/algebra.v b/tests/algebra.v
similarity index 100%
rename from theories/tests/algebra.v
rename to tests/algebra.v
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
new file mode 100644
index 000000000..ee58cebae
--- /dev/null
+++ b/tests/heap_lang.ref
@@ -0,0 +1,20 @@
+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⌠}}
+
diff --git a/theories/tests/heap_lang.v b/tests/heap_lang.v
similarity index 97%
rename from theories/tests/heap_lang.v
rename to tests/heap_lang.v
index 62b74b5e0..2e5f2e239 100644
--- a/theories/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -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 :=
diff --git a/tests/ipm_paper.ref b/tests/ipm_paper.ref
new file mode 100644
index 000000000..e69de29bb
diff --git a/theories/tests/ipm_paper.v b/tests/ipm_paper.v
similarity index 100%
rename from theories/tests/ipm_paper.v
rename to tests/ipm_paper.v
diff --git a/tests/list_reverse.ref b/tests/list_reverse.ref
new file mode 100644
index 000000000..e69de29bb
diff --git a/theories/tests/list_reverse.v b/tests/list_reverse.v
similarity index 100%
rename from theories/tests/list_reverse.v
rename to tests/list_reverse.v
diff --git a/tests/one_shot.ref b/tests/one_shot.ref
new file mode 100644
index 000000000..e69de29bb
diff --git a/theories/tests/one_shot.v b/tests/one_shot.v
similarity index 100%
rename from theories/tests/one_shot.v
rename to tests/one_shot.v
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
new file mode 100644
index 000000000..c535692a0
--- /dev/null
+++ b/tests/proofmode.ref
@@ -0,0 +1,21 @@
+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
+
diff --git a/theories/tests/proofmode.v b/tests/proofmode.v
similarity index 99%
rename from theories/tests/proofmode.v
rename to tests/proofmode.v
index bd5c516be..ee39d2b8a 100644
--- a/theories/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -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.
diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
new file mode 100644
index 000000000..2530df5c5
--- /dev/null
+++ b/tests/proofmode_iris.ref
@@ -0,0 +1,110 @@
+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
+
diff --git a/theories/tests/proofmode_iris.v b/tests/proofmode_iris.v
similarity index 96%
rename from theories/tests/proofmode_iris.v
rename to tests/proofmode_iris.v
index df20ac3d1..a85d637f4 100644
--- a/theories/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -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.
diff --git a/tests/proofmode_monpred.ref b/tests/proofmode_monpred.ref
new file mode 100644
index 000000000..e69de29bb
diff --git a/theories/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
similarity index 100%
rename from theories/tests/proofmode_monpred.v
rename to tests/proofmode_monpred.v
diff --git a/tests/tree_sum.ref b/tests/tree_sum.ref
new file mode 100644
index 000000000..e69de29bb
diff --git a/theories/tests/tree_sum.v b/tests/tree_sum.v
similarity index 100%
rename from theories/tests/tree_sum.v
rename to tests/tree_sum.v
--
GitLab