support Coq 8.11; no longer test output in 8.8

Makefile.coq.local

@@ -9,7 +9,7 @@ test: $(TESTFILES:.v=.vo)
 .PHONY: test
 
 COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
-COQ_OLD=$(shell echo "$(COQ_VERSION)" | egrep "^8\.7\b" -q && echo 1)
+COQ_OLD=$(shell echo "$(COQ_VERSION)" | egrep "^8\.(7|8)\b" -q && echo 1)
 COQ_MINOR_VERSION=$(shell echo "$(COQ_VERSION)" | egrep '^[0-9]+\.[0-9]+\b' -o)
 
 tests/.coqdeps.d: $(TESTFILES)

opam

@@ -11,6 +11,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
 depends: [
-  "coq" { (= "8.7.2") | (= "8.8.2") | (>= "8.9" & < "8.11~") | (= "dev") }
+  "coq" { (= "8.7.2") | (= "8.8.2") | (>= "8.9" & < "8.12~") | (= "dev") }
   "coq-stdpp" { (= "dev.2019-09-19.1.9041e6d8") | (= "dev") }
 ]

tests/atomic.8.8.ref

-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  aheap : atomic_heap Σ
-  Q : iProp Σ
-  l : loc
-  v : val
-  ============================
-  "Hl" : l ↦ v
-  --------------------------------------∗
-  AACC << ∀ (v0 : val) (q : Qp), l ↦{q} v0 ABORT l ↦ v >> @ ⊤, ∅
-       << l ↦{q} v0, COMM Q -∗ Q >>
-  
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  P : val → iProp Σ
-  ============================
-  <<< ∀ x : val, P x >>> code @ ⊤ <<< ∃ y : val, P y, RET #() >>>
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  P : val → iProp Σ
-  Φ : language.val heap_lang → iProp Σ
-  ============================
-  "AU" : AU << ∀ x : val, P x >> @ ⊤, ∅ << ∃ y : val, P y, COMM Φ #() >>
-  --------------------------------------∗
-  WP code {{ v, Φ v }}
-  
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  P : val → iProp Σ
-  Φ : language.val heap_lang → iProp Σ
-  ============================
-  _ : AACC << ∀ x : val, P x
-              ABORT AU << ∀ x : val, P x >> @ ⊤, ∅
-                       << ∃ y : val, P y, COMM Φ #() >> >> @ ⊤, ∅
-           << ∃ y : val, P y, COMM Φ #() >>
-  --------------------------------------∗
-  WP code {{ v, Φ v }}
-  
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  l : loc
-  ============================
-  <<< ∀ x : val, l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  l : loc
-  Φ : language.val heap_lang → iProp Σ
-  ============================
-  "AU" : AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Φ #() >>
-  --------------------------------------∗
-  WP code {{ v, Φ v }}
-  
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  l : loc
-  Φ : language.val heap_lang → iProp Σ
-  ============================
-  _ : AACC << ∀ x : val, l ↦ x
-              ABORT AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Φ #() >> >> 
-           @ ⊤, ∅ << l ↦ x, COMM Φ #() >>
-  --------------------------------------∗
-  WP code {{ v, Φ v }}
-  
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  l : loc
-  ============================
-  <<< l ↦ #() >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  l : loc
-  Φ : language.val heap_lang → iProp Σ
-  ============================
-  "AU" : AU << l ↦ #() >> @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
-  --------------------------------------∗
-  WP code {{ v, Φ v }}
-  
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  l : loc
-  Φ : language.val heap_lang → iProp Σ
-  ============================
-  _ : AACC << l ↦ #()
-              ABORT AU << l ↦ #() >> @ ⊤, ∅
-                       << ∃ y : val, l ↦ y, COMM Φ #() >> >> @ ⊤, ∅
-           << ∃ y : val, l ↦ y, COMM Φ #() >>
-  --------------------------------------∗
-  WP code {{ v, Φ v }}
-  
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  l : loc
-  ============================
-  <<< l ↦ #() >>> code @ ⊤ <<< l ↦ #(), RET #() >>>
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  l : loc
-  Φ : language.val heap_lang → iProp Σ
-  ============================
-  "AU" : AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Φ #() >>
-  --------------------------------------∗
-  WP code {{ v, Φ v }}
-  
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  l : loc
-  Φ : language.val heap_lang → iProp Σ
-  ============================
-  _ : AACC << l ↦ #()
-              ABORT AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Φ #() >> >> 
-           @ ⊤, ∅ << l ↦ #(), COMM Φ #() >>
-  --------------------------------------∗
-  WP code {{ v, Φ v }}
-  
-"Now come the long pre/post tests"
-     : string
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  l : loc
-  ============================
-  <<< ∀ x : val, l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  l : loc
-  Φ : language.val heap_lang → iProp Σ
-  ============================
-  "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x >> @ ⊤, ∅
-            << ∃ y : val, l ↦ y, COMM Φ #() >>
-  --------------------------------------∗
-  WP code {{ v, Φ v }}
-  
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  l : loc
-  ============================
-  <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
-    code @ ⊤
-  <<< ∃ y : val, l ↦ y, RET #() >>>
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  l : loc
-  Φ : language.val heap_lang → iProp Σ
-  ============================
-  "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
-            @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
-  --------------------------------------∗
-  WP code {{ v, Φ v }}
-  
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  l : loc
-  ============================
-  <<< ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
-    code @ ⊤
-  <<< ∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
-      RET #() >>>
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  l : loc
-  Φ : language.val heap_lang → iProp Σ
-  ============================
-  _ : AU << ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
-         << ∃ yyyy : val, l ↦ yyyy
-                          ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
-            COMM Φ #() >>
-  --------------------------------------∗
-  WP code {{ v, Φ v }}
-  
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  l : loc
-  ============================
-  <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
-    code @ ⊤
-  <<< l ↦ x, RET #() >>>
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  l : loc
-  Φ : language.val heap_lang → iProp Σ
-  ============================
-  "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
-            << l ↦ x, COMM Φ #() >>
-  --------------------------------------∗
-  WP code {{ v, Φ v }}
-  
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  l : loc
-  x : val
-  ============================
-  <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
-    code @ ⊤
-  <<< ∃ y : val, l ↦ y, RET #() >>>
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  l : loc
-  x : val
-  Φ : language.val heap_lang → iProp Σ
-  ============================
-  "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
-            << ∃ y : val, l ↦ y, COMM Φ #() >>
-  --------------------------------------∗
-  WP code {{ v, Φ v }}
-  
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  l : loc
-  x : val
-  ============================
-  <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
-    code @ ⊤
-  <<< l ↦ #(), RET #() >>>
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  l : loc
-  x : val
-  Φ : language.val heap_lang → iProp Σ
-  ============================
-  "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
-            << l ↦ #(), COMM Φ #() >>
-  --------------------------------------∗
-  WP code {{ v, Φ v }}
-  
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  l : loc
-  xx, yyyy : val
-  ============================
-  <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
-    code @ ⊤
-  <<< l ↦ yyyy, RET #() >>>
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  l : loc
-  xx, yyyy : val
-  Φ : language.val heap_lang → iProp Σ
-  ============================
-  "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
-            @ ⊤, ∅ << l ↦ yyyy, COMM Φ #() >>
-  --------------------------------------∗
-  WP code {{ v, Φ v }}
-  
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  l : loc
-  xx, yyyy : val
-  ============================
-  <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
-    code @ ⊤
-  <<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
-      RET #() >>>
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  l : loc
-  xx, yyyy : val
-  Φ : language.val heap_lang → iProp Σ
-  ============================
-  "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
-            << l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
-               COMM Φ #() >>
-  --------------------------------------∗
-  WP code {{ v, Φ v }}
-  
-"Prettification"
-     : string
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  P : val → iProp Σ
-  Φ : language.val heap_lang → iProp Σ
-  ============================
-  "AU" : ∃ x : val, P x
-                    ∗ (P x
-                       ={∅,⊤}=∗ AU << ∀ x0 : val, 
-                                   P x0 >> @ ⊤, ∅
-                                   << ∃ y : val, P y, COMM Φ #() >>)
-                      ∧ (∀ x0 : val, P x0 ={∅,⊤}=∗ Φ #())
-  --------------------------------------∗
-  WP ! #0 @ ∅ {{ v, |={∅,⊤}=> Φ v }}
-  

tests/list_reverse.8.10.ref → tests/list_reverse.8.9.ref

@@ -10,7 +10,7 @@
   "Hys" : is_list acc ys
   "HΦ" : ∀ w : val, is_list w (reverse xs ++ ys) -∗ Φ w
   --------------------------------------∗
-  WP rev hd acc [{ v, Φ v }]
+  WP (rev hd) acc [{ v, Φ v }]
   
 1 subgoal
   
@@ -28,6 +28,6 @@
      | InjR "l" =>
        let: "tmp1" := Fst ! "l" in
        let: "tmp2" := Snd ! "l" in
-       "l" <- ("tmp1", acc);; rev "tmp2" (InjLV #())
+       "l" <- ("tmp1", acc);; (rev "tmp2") (InjLV #())
      end [{ v, Φ v }]
   

tests/list_reverse.ref

@@ -10,7 +10,7 @@
   "Hys" : is_list acc ys
   "HΦ" : ∀ w : val, is_list w (reverse xs ++ ys) -∗ Φ w
   --------------------------------------∗
-  WP (rev hd) acc [{ v, Φ v }]
+  WP rev hd acc [{ v, Φ v }]
   
 1 subgoal
   
@@ -28,6 +28,6 @@
      | InjR "l" =>
        let: "tmp1" := Fst ! "l" in
        let: "tmp2" := Snd ! "l" in
-       "l" <- ("tmp1", acc);; (rev "tmp2") (InjLV #())
+       "l" <- ("tmp1", acc);; rev "tmp2" (InjLV #())
      end [{ v, Φ v }]