From 15f1ac56412d09388e6b4edab34cc312d333fc67 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 9 Oct 2019 17:00:45 +0200
Subject: [PATCH] support Coq 8.11; no longer test output in 8.8

---
 Makefile.coq.local                            |   2 +-
 opam                                          |   2 +-
 tests/atomic.8.8.ref                          | 339 ------------------
 ..._reverse.8.10.ref => list_reverse.8.9.ref} |   4 +-
 tests/list_reverse.ref                        |   4 +-
 5 files changed, 6 insertions(+), 345 deletions(-)
 delete mode 100644 tests/atomic.8.8.ref
 rename tests/{list_reverse.8.10.ref => list_reverse.8.9.ref} (89%)

diff --git a/Makefile.coq.local b/Makefile.coq.local
index 182c618ac..fe6320aa2 100644
--- a/Makefile.coq.local
+++ b/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)
diff --git a/opam b/opam
index 1385e6ddb..49ebc832e 100644
--- a/opam
+++ b/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") }
 ]
diff --git a/tests/atomic.8.8.ref b/tests/atomic.8.8.ref
deleted file mode 100644
index a3f918527..000000000
--- a/tests/atomic.8.8.ref
+++ /dev/null
@@ -1,339 +0,0 @@
-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 }}
-  
diff --git a/tests/list_reverse.8.10.ref b/tests/list_reverse.8.9.ref
similarity index 89%
rename from tests/list_reverse.8.10.ref
rename to tests/list_reverse.8.9.ref
index 9440658db..2c8d90077 100644
--- a/tests/list_reverse.8.10.ref
+++ b/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 }]
   
diff --git a/tests/list_reverse.ref b/tests/list_reverse.ref
index 2c8d90077..9440658db 100644
--- a/tests/list_reverse.ref
+++ b/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 }]
   
-- 
GitLab