From b615df4319b19bab8f9b04ff087619d100bbeb5f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 16 Dec 2020 13:50:40 +0100
Subject: [PATCH] separate ref files for Coq 8.11 where necessary

---
 Makefile.coq.local               |   3 +-
 tests/proofmode_ascii.8.11.ref   | 221 +++++++++++++++++++++++++++++++
 tests/proofmode_monpred.8.11.ref |  89 +++++++++++++
 3 files changed, 312 insertions(+), 1 deletion(-)
 create mode 100644 tests/proofmode_ascii.8.11.ref
 create mode 100644 tests/proofmode_monpred.8.11.ref

diff --git a/Makefile.coq.local b/Makefile.coq.local
index 2087b6ff3..c84026256 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -19,7 +19,8 @@ test: $(TESTFILES:.v=.vo)
 .PHONY: test
 
 COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
-COQ_MINOR_VERSION:=$(shell echo "$(COQ_VERSION)" | egrep '^[0-9]+\.[0-9]+\b' -o)
+# Need to make this a lazy variable (`=` instead of `:=`) since COQ_VERSION is only set later.
+COQ_MINOR_VERSION=$(shell echo "$(COQ_VERSION)" | egrep '^[0-9]+\.[0-9]+\b' -o)
 
 tests/.coqdeps.d: $(TESTFILES)
 	$(SHOW)'COQDEP TESTFILES'
diff --git a/tests/proofmode_ascii.8.11.ref b/tests/proofmode_ascii.8.11.ref
new file mode 100644
index 000000000..a8e890845
--- /dev/null
+++ b/tests/proofmode_ascii.8.11.ref
@@ -0,0 +1,221 @@
+1 subgoal
+  
+  Σ : gFunctors
+  invG0 : invG Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
+  N : namespace
+  P : iProp Σ
+  ============================
+  "H" : inv N (<pers> P)
+  "H2" : â–· <pers> P
+  --------------------------------------â–¡
+  |={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> ▷ P)
+  
+1 subgoal
+  
+  Σ : gFunctors
+  invG0 : invG Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
+  N : namespace
+  P : iProp Σ
+  ============================
+  "H" : inv N (<pers> P)
+  "H2" : â–· <pers> P
+  --------------------------------------â–¡
+  "Hclose" : ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp
+  --------------------------------------∗
+  |={⊤ ∖ ↑N,⊤}=> ▷ P
+  
+1 subgoal
+  
+  Σ : gFunctors
+  invG0 : invG Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
+  γ : gname
+  p : Qp
+  N : namespace
+  P : iProp Σ
+  ============================
+  _ : cinv N γ (<pers> P)
+  "HP" : â–· <pers> P
+  --------------------------------------â–¡
+  "Hown" : cinv_own γ p
+  --------------------------------------∗
+  |={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> cinv_own γ p ∗ ▷ P)
+  
+1 subgoal
+  
+  Σ : gFunctors
+  invG0 : invG Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
+  γ : gname
+  p : Qp
+  N : namespace
+  P : iProp Σ
+  ============================
+  _ : cinv N γ (<pers> P)
+  "HP" : â–· <pers> P
+  --------------------------------------â–¡
+  "Hown" : cinv_own γ p
+  "Hclose" : ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp
+  --------------------------------------∗
+  |={⊤ ∖ ↑N,⊤}=> cinv_own γ p ∗ ▷ P
+  
+1 subgoal
+  
+  Σ : gFunctors
+  invG0 : invG Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
+  t : na_inv_pool_name
+  N : namespace
+  E1, E2 : coPset
+  P : iProp Σ
+  H : ↑N ⊆ E2
+  ============================
+  _ : na_inv t N (<pers> P)
+  "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
+  invG0 : invG Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
+  t : na_inv_pool_name
+  N : namespace
+  E1, E2 : coPset
+  P : iProp Σ
+  H : ↑N ⊆ E2
+  ============================
+  _ : na_inv t N (<pers> P)
+  "HP" : â–· <pers> P
+  --------------------------------------â–¡
+  "Hown1" : na_own t E1
+  "Hown2" : na_own t (E2 ∖ ↑N)
+  "Hclose" : ▷ <pers> P ∗ na_own t (E2 ∖ ↑N) ={⊤}=∗ na_own t E2
+  --------------------------------------∗
+  |={⊤}=> na_own t E1 ∗ na_own t E2 ∗ ▷ P
+  
+"test_iInv_12"
+     : string
+The command has indeed failed with message:
+Tactic failure: iInv: selector 34 is not of the right type .
+The command has indeed failed with message:
+Tactic failure: iInv: invariant nroot not found.
+The command has indeed failed with message:
+Tactic failure: iInv: invariant "H2" not found.
+"test_iInv"
+     : string
+1 subgoal
+  
+  Σ : gFunctors
+  invG0 : invG Σ
+  I : biIndex
+  N : namespace
+  E : coPset
+  𝓟 : iProp Σ
+  H : ↑N ⊆ E
+  ============================
+  "HP" : ⎡ ▷ 𝓟 ⎤
+  --------------------------------------∗
+  |={E ∖ ↑N}=> ⎡ ▷ 𝓟 ⎤ ∗ (|={E}=> emp)
+  
+"test_iInv_with_close"
+     : string
+1 subgoal
+  
+  Σ : gFunctors
+  invG0 : invG Σ
+  I : biIndex
+  N : namespace
+  E : coPset
+  𝓟 : iProp Σ
+  H : ↑N ⊆ E
+  ============================
+  "HP" : ⎡ ▷ 𝓟 ⎤
+  "Hclose" : ⎡ ▷ 𝓟 ={E ∖ ↑N,E}=∗ emp ⎤
+  --------------------------------------∗
+  |={E ∖ ↑N,E}=> emp
+  
+"p1"
+     : string
+1 subgoal
+  
+  PROP : bi
+  ============================
+  forall (P : PROP) (_ : True), bi_entails P P
+"p2"
+     : string
+1 subgoal
+  
+  PROP : bi
+  ============================
+  forall P : PROP, and True (bi_entails P P)
+"p3"
+     : string
+1 subgoal
+  
+  PROP : bi
+  ============================
+  ex (fun P : PROP => bi_entails P P)
+"p4"
+     : string
+1 subgoal
+  
+  PROP : bi
+  ============================
+  bi_emp_valid (bi_exist (fun x : nat => bi_pure (eq x O)))
+"p5"
+     : string
+1 subgoal
+  
+  PROP : bi
+  ============================
+  bi_emp_valid (bi_exist (fun _ : nat => bi_pure (forall y : nat, eq y y)))
+"p6"
+     : string
+1 subgoal
+  
+  PROP : bi
+  ============================
+  ex
+    (unique
+       (fun z : nat =>
+        bi_emp_valid
+          (bi_exist
+             (fun _ : nat =>
+              bi_sep (bi_pure (forall y : nat, eq y y)) (bi_pure (eq z O))))))
+"p7"
+     : string
+1 subgoal
+  
+  PROP : bi
+  ============================
+  forall (a : nat) (_ : eq a O) (y : nat),
+  bi_entails (bi_pure True) (bi_pure (ge y O))
+"p8"
+     : string
+1 subgoal
+  
+  PROP : bi
+  ============================
+  forall (a : nat) (_ : eq a O) (y : nat), bi_emp_valid (bi_pure (ge y O))
+"p9"
+     : string
+1 subgoal
+  
+  PROP : bi
+  ============================
+  forall (a : nat) (_ : eq a O) (_ : nat),
+  bi_emp_valid (bi_forall (fun z : nat => bi_pure (ge z O)))
diff --git a/tests/proofmode_monpred.8.11.ref b/tests/proofmode_monpred.8.11.ref
new file mode 100644
index 000000000..4c240744e
--- /dev/null
+++ b/tests/proofmode_monpred.8.11.ref
@@ -0,0 +1,89 @@
+1 subgoal
+  
+  I : biIndex
+  PROP : bi
+  P, Q : monPred
+  i : I
+  ============================
+  "HW" : (P -∗ Q) i
+  --------------------------------------∗
+  (P -∗ Q) i
+  
+1 subgoal
+  
+  I : biIndex
+  PROP : bi
+  P, Q : monPred
+  i, j : I
+  ============================
+  "HW" : (P -∗ Q) j
+  "HP" : P j
+  --------------------------------------∗
+  Q j
+  
+1 subgoal
+  
+  I : biIndex
+  PROP : bi
+  P, Q : monPred
+  Objective0 : Objective Q
+  𝓟, 𝓠 : PROP
+  ============================
+  "H2" : ∀ i : I, Q i
+  "H3" : 𝓟
+  "H4" : 𝓠
+  --------------------------------------∗
+  ∀ i : I, 𝓟 ∗ 𝓠 ∗ Q i
+  
+1 subgoal
+  
+  I : biIndex
+  PROP : bi
+  FU : BiFUpd PROP
+  P, Q : monPred
+  i : I
+  ============================
+  --------------------------------------∗
+  (Q -∗ emp) i
+  
+1 subgoal
+  
+  I : biIndex
+  PROP : bi
+  FU : BiFUpd PROP
+  P : monPred
+  i : I
+  ============================
+  --------------------------------------∗
+  ∀ _ : (), ∃ _ : (), emp
+  
+The command has indeed failed with message:
+Tactic failure: iFrame: cannot frame (P i).
+1 subgoal
+  
+  I : biIndex
+  Σ : gFunctors
+  invG0 : invG Σ
+  N : namespace
+  𝓟 : iProp Σ
+  ============================
+  "H" : ⎡ inv N (<pers> 𝓟) ⎤
+  "H2" : ⎡ ▷ <pers> 𝓟 ⎤
+  --------------------------------------â–¡
+  |={⊤ ∖ ↑N}=> ⎡ ▷ <pers> 𝓟 ⎤ ∗ (|={⊤}=> ⎡ ▷ 𝓟 ⎤)
+  
+1 subgoal
+  
+  I : biIndex
+  Σ : gFunctors
+  invG0 : invG Σ
+  N : namespace
+  𝓟 : iProp Σ
+  ============================
+  "H" : ⎡ inv N (<pers> 𝓟) ⎤
+  "H2" : ⎡ ▷ <pers> 𝓟 ⎤
+  --------------------------------------â–¡
+  "Hclose" : ⎡ ▷ <pers> 𝓟 ={⊤ ∖ ↑N,⊤}=∗ emp ⎤
+  --------------------------------------∗
+  |={⊤ ∖ ↑N,⊤}=> ⎡ ▷ 𝓟 ⎤
+  
-- 
GitLab