Merge branch 'ci/reftests' into 'gen_proofmode'

Enable test suite to check printed output

See merge request FP/iris-coq!147

.gitlab-ci.yml

@@ -29,6 +29,7 @@ variables:
 build-coq.dev:
   <<: *template
   variables:
+    BUILD_TARGET: "ref" # don't check test output
     OPAM_PINS: "coq version dev"
     VALIDATE: "1"
 

Makefile

@@ -8,7 +8,7 @@ all: Makefile.coq
 
 clean: Makefile.coq
 	+@make -f Makefile.coq clean
-	find theories \( -name "*.v.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
+	find theories $$(test -d tests && echo tests) \( -name "*.v.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
 	rm -f Makefile.coq
 .PHONY: clean
 
@@ -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) || ( \

Makefile.coq.local

+# 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) $(COQLIBS) $< $(TIMING_EXTRA) > "$$TMPFILE" && \
+	  (diff --color=auto -u "tests/$$TEST.ref" "$$TMPFILE" || (rm "tests/$$TEST.vo" "$$TMPFILE" && exit 1)) && \
+	  rm "$$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) $(COQLIBS) $< $(TIMING_EXTRA) > "tests/$$TEST.ref"

_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

ci @ 16c8b610

-Subproject commit 99c935d2007358fe4028560e96f9c136e608e696
+Subproject commit 16c8b6107119db3448b6828d3d2757888f2b2376

tests/heap_lang.ref

+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⌝ }}
+  

theories/tests/heap_lang.v → 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 :=

tests/proofmode.ref

+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
+  

theories/tests/proofmode.v → 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.

tests/proofmode_iris.ref

+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
+  

theories/tests/proofmode_iris.v → 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.