From 3818868ebe0de46de042a207762817f2018f502c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 21 Sep 2017 13:40:02 +0200
Subject: [PATCH] update build system and Iris

---
 .gitlab-ci.yml                  |  2 +-
 Makefile                        | 37 +++++++++++++++----------
 build/opam-ci.sh                | 48 ++++++++++++++++++++++++---------
 build/opam-pins.sh              | 26 ------------------
 opam                            |  7 ++---
 opam.pins                       |  1 -
 theories/adequacy.v             |  4 +--
 theories/base/at_shared.v       |  6 ++---
 theories/base/fork.v            |  4 +--
 theories/base/ghosts.v          | 15 ++++++-----
 theories/base/helpers.v         |  2 +-
 theories/base/na_shared.v       |  4 +--
 theories/blocks.v               |  2 +-
 theories/examples/nat_tokens.v  |  2 +-
 theories/examples/rcu.v         |  6 ++---
 theories/examples/rcu_data.v    |  2 +-
 theories/examples/ticket_lock.v |  6 ++---
 theories/gps/cas.v              | 13 +++++----
 theories/gps/fai.v              | 13 +++++----
 theories/gps/write.v            | 13 +++++----
 theories/lifting.v              | 10 +++----
 theories/rsl.v                  |  4 +--
 theories/viewpred.v             |  6 ++---
 23 files changed, 117 insertions(+), 116 deletions(-)
 delete mode 100755 build/opam-pins.sh
 delete mode 100644 opam.pins

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index af344b4c..ba59019e 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -16,7 +16,7 @@ variables:
   - 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \((real|user): [0-9]" | tee build-time.txt'
   - 'if test -n "$VALIDATE" && (( RANDOM % 10 == 0 )); then make validate; fi'
   cache:
-    key: "coq$COQ_VERSION-ssr$SSR_VERSION"
+    key: "coq.$COQ_VERSION-ssr.$SSR_VERSION"
     paths:
     - opamroot/
   only:
diff --git a/Makefile b/Makefile
index 7bfa06f8..4a7e6442 100644
--- a/Makefile
+++ b/Makefile
@@ -1,38 +1,47 @@
-# Process flags
-ifeq ($(Y), 1)
-	YFLAG=-y
-endif
-
 # Forward most targets to Coq makefile (with some trick to make this phony)
 %: Makefile.coq phony
 	+@make -f Makefile.coq $@
 
 all: Makefile.coq
 	+@make -f Makefile.coq all
+.PHONY: all
 
 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
 	rm -f Makefile.coq
+.PHONY: clean
 
-# Create Coq Makefile. POSIX awk can't do in-place editing, but coq_makefile wants the real filename, so we do some file gymnastics.
+# Create Coq Makefile. POSIX awk can't do in-place editing, but coq_makefile wants the real
+# filename, so we do some file gymnastics.
 Makefile.coq: _CoqProject Makefile awk.Makefile
 	coq_makefile -f _CoqProject -o Makefile.coq
 	mv Makefile.coq Makefile.coq.tmp && awk -f awk.Makefile Makefile.coq.tmp > Makefile.coq && rm Makefile.coq.tmp
 
 # Install build-dependencies
-build-dep:
-	build/opam-pins.sh < opam.pins
-	opam upgrade $(YFLAG) # it is not nice that we upgrade *all* packages here, but I found no nice way to upgrade only those that we pinned
-	opam pin add opam-builddep-temp "$$(pwd)#HEAD" -k git -n -y
-	opam install opam-builddep-temp --deps-only $(YFLAG)
-	opam pin remove opam-builddep-temp
+build-dep/opam: opam
+	# Create the build-dep package.
+	@mkdir -p build-dep
+	@sed <opam 's/^\(build\|install\|remove\):.*/\1: []/; s/^name: *"\(.*\)" */name: "\1-builddep"/' > build-dep/opam
+	@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check
+
+build-dep: build-dep/opam phony
+	@# We want opam to not just instal the build-deps now, but to also keep satisfying these
+	@# constraints.  Otherwise, `opam upgrade` may well update some packages to versions
+	@# that are incompatible with our build requirements.
+	@# To achieve this, we create a fake opam package that has our build-dependencies as
+	@# dependencies, but does not actually install anything.
+	# Add the pin and (re)install build-dep package.
+	@# Reinstallation is needed in case the pin already exists, but the builddep package changed.
+	@BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')"; \
+	  opam pin add "$$BUILD_DEP_PACKAGE".dev "$$(pwd)/build-dep" -k path $(OPAMFLAGS) && \
+	  opam reinstall "$$BUILD_DEP_PACKAGE"
 
 # Some files that do *not* need to be forwarded to Makefile.coq
 Makefile: ;
 _CoqProject: ;
 awk.Makefile: ;
 
-# Phony targets (i.e. targets that should be run no matter the timestamps of the involved files)
+# Phony wildcard targets
 phony: ;
-.PHONY: all clean phony
+.PHONY: phony
diff --git a/build/opam-ci.sh b/build/opam-ci.sh
index 20d87f9d..27ae623d 100755
--- a/build/opam-ci.sh
+++ b/build/opam-ci.sh
@@ -1,42 +1,66 @@
 #!/bin/bash
 set -e
-# This script installs the build dependencies for CI builds.
+## This script installs the build dependencies for CI builds.
+function run_and_print() {
+    echo "$ $@"
+    "$@"
+}
 
 # Prepare OPAM configuration
 export OPAMROOT="$(pwd)/opamroot"
 export OPAMJOBS="$((2*$CPU_CORES))"
 export OPAM_EDITOR="$(which false)"
 
-# Make sure we got a good OPAM
-test -d "$OPAMROOT" || (mkdir "$OPAMROOT" && opam init --no-setup -y)
+# Make sure we got a good OPAM.
+test -d "$OPAMROOT" || (mkdir "$OPAMROOT" && run_and_print opam init --no-setup -y)
 eval `opam conf env`
+# Delete old pins from opam.pins times.
+run_and_print opam pin remove coq-stdpp -n
+run_and_print opam pin remove coq-iris -n
+# Make sure the pin for the builddep package is not stale.
+run_and_print make build-dep/opam
+
+# Get us all the latest repositories
 if test $(find "$OPAMROOT/repo/package-index" -mtime +0); then
     # last update was more than a day ago
-    opam update
+    run_and_print opam update
 else
-    echo "[opam-ci] Not updating opam."
+    # only update iris-dev
+    if test -d "$OPAMROOT/repo/iris-dev"; then run_and_print opam update iris-dev; fi
 fi
-test -d "$OPAMROOT/repo/coq-extra-dev" || opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev -p 5
-test -d "$OPAMROOT/repo/coq-core-dev" || opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev -p 5
-test -d "$OPAMROOT/repo/coq-released" || opam repo add coq-released https://coq.inria.fr/opam/released -p 10
+test -d "$OPAMROOT/repo/coq-extra-dev" && run_and_print opam repo remove coq-extra-dev
+test -d "$OPAMROOT/repo/coq-core-dev" || run_and_print opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev -p 5
+test -d "$OPAMROOT/repo/coq-released" || run_and_print opam repo add coq-released https://coq.inria.fr/opam/released -p 10
+test -d "$OPAMROOT/repo/iris-dev" || run_and_print opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git -p 20
+echo
+
+# We really want to run all of the following in one opam transaction, but due to opam limitations,
+# that is not currently possible.
 
-# Install fixed versions of some dependencies
+# Install fixed versions of some dependencies.
 echo
 while (( "$#" )); do # while there are arguments left
     PACKAGE="$1" ; shift
     VERSION="$1" ; shift
+
     # Check if the pin is already set
     if opam pin list | fgrep "$PACKAGE.$VERSION " > /dev/null; then
         echo "[opam-ci] $PACKAGE already pinned to $VERSION"
     else
         echo "[opam-ci] Pinning $PACKAGE to $VERSION"
-        opam pin add "$PACKAGE" "$VERSION" -k version -y
+        run_and_print opam pin add "$PACKAGE" "$VERSION" -k version -y
     fi
 done
 
-# Install build-dependencies
+# Upgrade cached things.
+echo
+echo "[opam-ci] Upgrading opam"
+run_and_print opam upgrade -y
+
+# Install build-dependencies.
 echo
-make build-dep Y=1
+echo "[opam-ci] Installing build-dependencies"
+make build-dep OPAMFLAGS=-y
 
 # done
 echo
diff --git a/build/opam-pins.sh b/build/opam-pins.sh
deleted file mode 100755
index 5291cb23..00000000
--- a/build/opam-pins.sh
+++ /dev/null
@@ -1,26 +0,0 @@
-#!/bin/bash
-set -e
-## Process an opam.pins file from stdin: Add all the given pins, but don't install anything.
-## Usage:
-##   ./opam-pins.sh < opam.pins
-
-if ! which curl >/dev/null; then
-    echo "opam-pins needs curl. Please install curl and try again."
-    exit 1
-fi
-
-# Process stdin
-while read PACKAGE URL HASH; do
-    if echo "$URL" | egrep '^https://gitlab\.mpi-sws\.org' > /dev/null; then
-        echo "[opam-pins] Recursing into $URL"
-        # an MPI URL -- try doing recursive pin processing
-        curl -f "$URL/raw/$HASH/opam.pins" 2>/dev/null | "$0"
-    fi
-    if opam pin list | fgrep "$PACKAGE.dev.$HASH " > /dev/null; then
-        echo "[opam-pins] $PACKAGE already at commit $HASH"
-    else
-        echo "[opam-pins] Applying pin: $PACKAGE -> $URL#$HASH"
-        opam pin add "$PACKAGE.dev.$HASH" "$URL#$HASH" -k git -y -n
-        echo
-    fi
-done
diff --git a/opam b/opam
index b3dba1e7..206e80a7 100644
--- a/opam
+++ b/opam
@@ -1,16 +1,13 @@
 opam-version: "1.2"
 name: "coq-igps"
-version: "dev"
 maintainer: "Jan-Oliver Kaiser, Hoang-Hai Dang"
 authors: "Jan-Oliver Kaiser, Hoang-Hai Dang"
 homepage: "http://plv.mpi-sws.org/igps/"
 bug-reports: "https://gitlab.mpi-sws.org/FP/sra-gps/issues"
 dev-repo: "https://gitlab.mpi-sws.org/FP/sra-gps.git"
-build: [
-  [make "-j%{jobs}%"]
-]
+build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/igps" ]
 depends: [
-  "coq-iris"
+  "coq-iris" { (= "dev.2017-09-20.3") | (= "dev") }
 ]
diff --git a/opam.pins b/opam.pins
deleted file mode 100644
index 63e03a3a..00000000
--- a/opam.pins
+++ /dev/null
@@ -1 +0,0 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq ea42f9947c8498292a0b02a3f901f0826b80ea63
diff --git a/theories/adequacy.v b/theories/adequacy.v
index 5ce53a9d..d05e08f3 100644
--- a/theories/adequacy.v
+++ b/theories/adequacy.v
@@ -49,7 +49,7 @@ Qed.
 Lemma Some_helper {X : Type} (x y : X) : Some x = Some y ↔ x = y. 
 Proof. naive_solver. Qed.
 
-Lemma dom_map_imap `{Countable K} {B} (f : K -> () -> B) g :
+Lemma dom_map_imap `{Countable K} {B} (f : K -> () -> B) (g: gmap _ _) :
   dom (gset K) (map_imap (λ x y, Some (f x y)) g) ≡ dom _ g.
 Proof.
   intros.
@@ -289,4 +289,4 @@ Proof.
         { by apply FA. }
         { apply H2; last apply FA; auto. }
   - by rewrite /IInv /to_info dom_fmap to_hist_dom.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/base/at_shared.v b/theories/base/at_shared.v
index 64a15eed..4f2aacce 100644
--- a/theories/base/at_shared.v
+++ b/theories/base/at_shared.v
@@ -8,7 +8,7 @@ Import uPred.
 From igps Require Export notation.
 From igps.base Require Export accessors helpers ghosts.
 
-Lemma write_at_update_hist Ï‚ Ï‚' V h t l v (m: message)
+Lemma write_at_update_hist Ï‚ Ï‚' (V: View) h t l v (m: message)
   (HOld: h ≡ map_vt (hist_from (mem ς) l t))
   (Disj : MS_msg_disj (msgs (mem Ï‚)) m)
   (MUpd : mem Ï‚' = add_ins (mem Ï‚) m Disj)
@@ -58,7 +58,7 @@ Proof.
 Qed.
 
 Lemma write_at_update_HInv `{fG : !foundationG Σ}
-  Ï‚ Ï‚' V (h h': History) (l : loc) v (m: message) HIST
+  (Ï‚ Ï‚': state) (V: View) (h h': History) (l : loc) v (m: message) HIST
   (HInvς: HInv ς HIST)
   (HH: HIST !! l = Excl' h)
   (HUpd: h' ≡ {[mval m, mview m]} ∪ h)
@@ -103,4 +103,4 @@ Proof.
         rewrite elem_of_difference elem_of_union ?elem_of_singleton EqVal.
         move => [[[-> //]|?] ?]. apply (IS v0 V0).
         by rewrite elem_of_difference elem_of_singleton.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/base/fork.v b/theories/base/fork.v
index a0697deb..2d0bc200 100644
--- a/theories/base/fork.v
+++ b/theories/base/fork.v
@@ -21,7 +21,7 @@ Proof.
     iIntros (Ï‚' V') "(% & % & % & % & OÏ‚')". inversion H7. subst.
 
     have: (∃ ρ : thread, VIEW !! ρ = None) => [|[ρ Hρ]].
-    { exists (fresh (dom _ (VIEW))).
+    { eexists (fresh (dom _ (VIEW))).
       by generalize (is_fresh (dom (gset positive) VIEW)) => /not_elem_of_dom. }
 
     iMod ((Views_alloc _ ρ) with "[$HV]") as "[AV' FV']"; first done.
@@ -35,4 +35,4 @@ Proof.
     iSplit;[|iSplit]; iPureIntro; [|done|done].
     move => ? ?.
     by rewrite lookup_insert_Some => [] [[_ [<- //]]|[_ /H0 //]].
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/base/ghosts.v b/theories/base/ghosts.v
index 1ed9991f..ab85a997 100644
--- a/theories/base/ghosts.v
+++ b/theories/base/ghosts.v
@@ -36,6 +36,7 @@ Global Instance foundationG_hist_singleton `{foundationG Σ} :
 
 Section Hist.
 
+  Implicit Type l: loc.
   Definition map_vt := map_gset (λ msg, (mval msg, mview msg)).
   Definition hTime l (x: Val * View) := match x with | (_,V) => V !! l end.
   Global Arguments map_vt _ /.
@@ -62,7 +63,7 @@ Section Hist.
   Definition no_adj_right l (h: History) (V : View) :=
     ¬ ∃ p, p ∈ h ∧ adj_opt (V !! l) (p.2 !! l).
 
-  Lemma adj_eq l (h: History) p1 p2 V
+  Lemma adj_eq l (h: History) p1 p2 (V: View)
     (In1: p1 ∈ h) (In2: p2 ∈ h) (Disj: hTime_pw_disj l h)
     (Adj1: adj_opt (p1.2 !! l) (V !! l))
     (Adj2: adj_opt (p2.2 !! l) (V !! l))
@@ -143,7 +144,7 @@ Section GhostDefs.
   Context `{fG : !foundationG Σ}.
 
   Implicit Types
-           (Ï‚ : state)
+           (Ï‚ : state) (l: loc)
            (VIEW : AuthType foundationG_view)
            (HIST : AuthType foundationG_hist)
            (INFO : AuthType foundationG_info).
@@ -367,7 +368,7 @@ Section Exclusives.
   Context `{Countable K} {A : cmraT}.
 
   Lemma gmapR_singleton_Exclusive (i: K) (x y: A) `{!Exclusive x}:
-    ✓ ({[i := x]} ⋅ {[i := y]}) → False.
+    ✓ (({[i := x]} : gmapR _ _) ⋅ {[i := y]}) → False.
   Proof.
     rewrite op_singleton. move/(_ i). rewrite lookup_singleton.
     by apply exclusive_l.
@@ -480,7 +481,7 @@ Section UpdateGhosts.
   Collection level1 := Σ fG.
   Local Set Default Proof Using "level1".
 
-  Implicit Types (π ρ : thread) (l : loc) (V : View) (h : History).
+  Implicit Types (π ρ : thread) (l : loc) (V : View) (h : History) (v: dec_agreeR InfoT).
   Local Open Scope I.
 
   Lemma Views_update_override π V (VIEW: Views) V'
@@ -585,10 +586,10 @@ Section UpdateGhosts.
   Close Scope I.
 
   Lemma IInv_update
-    Ï‚ INFO l v v'
+    Ï‚ INFO l zv zv'
     (Inv: IInv Ï‚ INFO)
-    (Hl: INFO !! l = Some v)
-    : IInv Ï‚ (<[l:=v']> INFO).
+    (Hl: INFO !! l = Some zv)
+    : IInv Ï‚ (<[l:=zv']> INFO).
   Proof.
     cbn in *.
     rewrite <-Inv.
diff --git a/theories/base/helpers.v b/theories/base/helpers.v
index 39a60f0b..dccdfde6 100644
--- a/theories/base/helpers.v
+++ b/theories/base/helpers.v
@@ -6,7 +6,7 @@ From igps Require Export ghosts.
 Set Bullet Behavior "Strict Subproofs".
 
 
-Lemma init_pre_helper Ï‚ h t l V_l v V
+Lemma init_pre_helper Ï‚ h t l (V_l: View) v (V: View)
   (Hinv: phys_inv Ï‚)
   (HH : h ≡ map_vt (hist_from (mem ς) l t))
   (In: (v, V) ∈ h)
diff --git a/theories/base/na_shared.v b/theories/base/na_shared.v
index 25776422..9e71fdd6 100644
--- a/theories/base/na_shared.v
+++ b/theories/base/na_shared.v
@@ -9,7 +9,7 @@ From igps Require Export notation history proofmode.
 From igps.base Require Export ghosts accessors helpers.
 
 Lemma write_na_update_HInv `{fG : !foundationG Σ}
-  Ï‚ Ï‚' (h  h2: History) (l : loc) (m: message) HIST
+  (Ï‚ Ï‚': state) (h  h2: History) (l : loc) (m: message) HIST
   (HInvς: HInv ς HIST)
   (Disj : MS_msg_disj (msgs (mem Ï‚)) m)
   (MUpd : mem Ï‚' = add_ins (mem Ï‚) m Disj)
@@ -52,4 +52,4 @@ Proof.
             { destruct (memory_ok (mem Ï‚') _ _ Inm In'') as [|[]] => //.
               exfalso. rewrite -EqLoc in EqL. auto. } }
       * move => ? ?. abstract set_solver+.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/blocks.v b/theories/blocks.v
index f73ab8fa..d125bd13 100644
--- a/theories/blocks.v
+++ b/theories/blocks.v
@@ -96,7 +96,7 @@ Section GHist.
       + by move => ->.
   Qed.
 
-  Lemma gblock_ends_ins_sL_update l (h: History) p p'
+  Lemma gblock_ends_ins_sL_update (l: loc) (h: History) p p'
     (In': p' ∈ gblock_ends l h)
     (NIn': p ∉ gblock_ends l h)
     (Adj: adj_opt (p'.2 !! l) (p.2 !! l))
diff --git a/theories/examples/nat_tokens.v b/theories/examples/nat_tokens.v
index 39cd4f0f..c1ffb814 100644
--- a/theories/examples/nat_tokens.v
+++ b/theories/examples/nat_tokens.v
@@ -101,5 +101,5 @@ Lemma coPset_of_gset_empty :
 Proof. by apply leibniz_equiv. Qed.
 
 Lemma coPset_difference_top_empty:
-  ⊤ ∖ ∅ = ⊤.
+  ⊤ ∖ ∅ = (⊤ : coPset).
 Proof. by apply leibniz_equiv. Qed.
diff --git a/theories/examples/rcu.v b/theories/examples/rcu.v
index 26e2d127..b1d1e215 100644
--- a/theories/examples/rcu.v
+++ b/theories/examples/rcu.v
@@ -774,7 +774,7 @@ Section RCU.
 
       assert (DD: dead (D γ) = ∅). { by apply RCUData_dead_singleton. }
       assert (SD: SinglePtr (D γ)). { by apply RCUData_SinglePtr_singleton. }
-      assert (DoD: dom _ (D γ) = {[i]}). { by apply RCUData_dom_singleton. }
+      assert (DoD: dom (gset _) (D γ) = {[i]}). { by apply RCUData_dom_singleton. }
       (* preparing reader's loop *)
       move Eqn' : {1 2 4}NPosn => n'.
       move Eqj: {5}(0%nat) => j.
@@ -2140,7 +2140,7 @@ Section RCU.
       wp_bind ([_]_na <- _)%E.
 
       (* setting up new history *)
-      set j' : aloc := fresh (dom _ D3).
+      set j' : aloc := fresh (dom (gset _) D3).
       set D3' : gname -> RCUData
         := λ γ', ((i, Abs j')::(j', bj)::(ix, Dead)::D3.1, (j',x',γ')::D3.2).
       set L1 := (L ++ (p, v0) :: (Z.pos x', v') :: L')%list.
@@ -3222,7 +3222,7 @@ Section RCU.
       iDestruct "Last" as (i γi) "(% & Last)".
 
       (* setting up new history *)
-      set j : aloc := fresh (dom _ D3).
+      set j : aloc := fresh (dom (gset _) D3).
       set D3' : gname -> RCUData 
         := λ γ, ((i, Abs j) :: (j, Null) :: D3.1, (j,x,γ) :: D3.2).
       set L1 := (L ++ (p, v) :: (Z.pos x, v') :: nil)%list.
diff --git a/theories/examples/rcu_data.v b/theories/examples/rcu_data.v
index 2f029d32..8ef40d34 100644
--- a/theories/examples/rcu_data.v
+++ b/theories/examples/rcu_data.v
@@ -845,7 +845,7 @@ Section RCUData.
   Proof. by rewrite rcu_hist'_cons_next. Qed.
 
   Lemma RCUData_dom_singleton i L:
-    dom _ ((i, Null) :: nil, L) = {[i]}.
+    dom (gset _) ((i, Null) :: nil, L) = {[i]}.
   Proof. by rewrite /= /RCUData_dom /= /RCUHist_dom /= union_empty_r_L. Qed.
 
   Lemma RCUData_dead_singleton i L:
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index 7d4822e8..b58c1a2b 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -154,7 +154,7 @@ Section TicketLock.
         (split; last auto); by eexists.
     Qed.
 
-    Local Instance Mtkt_dec3 M (t: nat):
+    Local Instance Mtkt_dec3 (M: gmapNOpN) (t: nat):
       Decision (∃ i, i ∈ dom (gset nat) M ∧ M !! i = Excl2 t).
     Proof.
       apply set_Exists_dec. intro j.
@@ -163,7 +163,7 @@ Section TicketLock.
       case (decide (k = t)) => [->|NEq]; by [left|right; move => []].
     Qed.
 
-    Lemma Mtkt_singleton M (t: nat)
+    Lemma Mtkt_singleton (M: gmapNOpN) (t: nat)
       (Inj : ∀ i k : nat, M !! i = Excl2 k →
               (∀ j : nat, M !! j = Excl2 k → i = j)):
       size (Mtkt_range M t (S t)) ≤ 1.
@@ -784,4 +784,4 @@ Section TicketLock.
     Qed.
   End proof.
 
-End TicketLock.
\ No newline at end of file
+End TicketLock.
diff --git a/theories/gps/cas.v b/theories/gps/cas.v
index 6b4abe19..1e45fe9c 100644
--- a/theories/gps/cas.v
+++ b/theories/gps/cas.v
@@ -183,8 +183,7 @@ Section CAS.
               apply Pos.lt_succ_r. by rewrite -Pos.add_1_r.
             + move => e2 In2. apply NEq, elem_of_union. by right.
           - apply (H3 e t); auto.
-            move => e' In'. apply (NEq e'), elem_of_union. right.
-            by apply elem_of_singleton. }
+            move => e' In'. apply (NEq e'), elem_of_union. right. done. }
 
         iFrame (Hi' HS HC' HI HF).
         iSplitL "oBEI oAI F Fp"; last first.
@@ -233,11 +232,11 @@ Section CAS.
           apply HI;
           [abstract set_solver+Hin1 InVr by auto
             |abstract set_solver+Hin2 InVr by auto]. }
-        rewrite 2!gset_map_singleton.
-        do 2!(rewrite -block_ends_fmap; [|done|done]).
-        rewrite /Consistent in HC'.
+        rewrite 2!gset_map_singleton. unfold sBE.
+        erewrite <-2!block_ends_fmap;
+          first (rewrite /Consistent in HC'; rewrite H2 HC' Hh');
+          [|done..].
 
-        rewrite H2 HC' Hh'.
         apply gblock_ends_ins_sL_update;[| |done|..].
         * apply elem_of_filter. split; auto.
           move => p ? ? ?. apply HNAdj. by exists p.
@@ -319,4 +318,4 @@ Section CAS.
             with "[$VV' $kS' $Hs'' $oI $ofX $oR' $VrV $VVr IF]").
     destruct b; iDestruct "IF" as "[? ?]"; by iFrame.
   Qed.
-End CAS.
\ No newline at end of file
+End CAS.
diff --git a/theories/gps/fai.v b/theories/gps/fai.v
index 6d8d5045..4af0c2e0 100644
--- a/theories/gps/fai.v
+++ b/theories/gps/fai.v
@@ -166,8 +166,7 @@ Section FAI.
             apply Pos.lt_succ_r. by rewrite -Pos.add_1_r.
           + move => e2 In2. apply NEq, elem_of_union. by right.
         - apply (H3 e t); auto.
-          move => e' In'. apply (NEq e'), elem_of_union. right.
-          by apply elem_of_singleton. }
+          move => e' In'. apply (NEq e'), elem_of_union. right. done. }
 
       iNext. iExists ({[s'', (v', V')]} ∪ ζ), h', (s_x, (v_x, V_x)).
       iFrame (Hi' HC' HI HS HF) "oA' oAX Hist'".
@@ -217,11 +216,11 @@ Section FAI.
         apply HI;
         [abstract set_solver+Hin1 InVr by auto
           |abstract set_solver+Hin2 InVr by auto]. }
-      rewrite 2!gset_map_singleton.
-      do 2!(rewrite -block_ends_fmap; [|done|done]).
-      rewrite /Consistent in HC'.
+      rewrite 2!gset_map_singleton. unfold sBE.
+      erewrite <-2!block_ends_fmap;
+        first (rewrite /Consistent in HC'; rewrite H2 HC' Hh');
+        [|done..].
 
-      rewrite H2 HC' Hh'.
       apply gblock_ends_ins_sL_update;[| |done|..].
       * apply elem_of_filter. split; auto.
         move => p ? ? ?. apply HNAdj. by exists p.
@@ -232,4 +231,4 @@ Section FAI.
       * apply (hTime_pw_disj_mono _ _ h');
         [by rewrite Hh'|by apply H8].
   Qed.
-End FAI.
\ No newline at end of file
+End FAI.
diff --git a/theories/gps/write.v b/theories/gps/write.v
index c6b1e701..0647a51c 100644
--- a/theories/gps/write.v
+++ b/theories/gps/write.v
@@ -114,8 +114,7 @@ Section Write.
       assert (FinalInv l (s_x, (v_x, V_x)) ({[s', (v, V')]} ∪ ζ)).
         { move => e t /elem_of_union [/elem_of_singleton -> //= | ?] ? ? NEq.
           apply (H4 e t) => //.
-          move => e' In'. apply (NEq e'), elem_of_union. right.
-          by apply elem_of_singleton. }
+          move => e' In'. apply (NEq e'), elem_of_union. right. done. }
 
       iFrame (HC' HS' H11 HI HInit).
       iSplit; last first.
@@ -150,10 +149,10 @@ Section Write.
             |abstract set_solver+Hin2 by auto]. }
 
         rewrite gset_map_union.
-        rewrite gset_map_singleton.
-        do 2!(rewrite -block_ends_fmap; [|done|done]).
-        rewrite /Consistent in HC' H3.
-        rewrite H3 HC' Hh' /fm /=.
+        rewrite gset_map_singleton. unfold sBE.
+        erewrite <-2!block_ends_fmap;
+          first (rewrite /Consistent in HC' H3; rewrite H3 HC' Hh' /fm /=);
+          [|done..].
         by apply block_ends_ins_mono.
   Qed.
 
@@ -345,4 +344,4 @@ Section Write.
     iNext. iIntros (V') "(VV' & kS' & oI & Q & ofX' & oR' & oW' & Max)".
     iApply ("Post" $! V' with "[$VV' $kS' $oI $Q $ofX' $oR' $oW' $Max]").
   Qed.
-End Write.
\ No newline at end of file
+End Write.
diff --git a/theories/lifting.v b/theories/lifting.v
index 2eb1b1a9..8ad11c0a 100644
--- a/theories/lifting.v
+++ b/theories/lifting.v
@@ -256,20 +256,20 @@ Qed.
 Instance constant_dec {T : Prop} {X : Type} 
                       `{Decision T} : ∀ x, (Decision ((λ x : X, T) x)) := _.
 
-Inductive drf_pre (σ : state) V l : Prop :=
+Inductive drf_pre (σ : state) (V: View) (l: loc) : Prop :=
   | _singleton_drf
                    otl otn
                    (Local : V !! l = otl)
                    (NATS : nats σ !! l = otn)
                    (LE : otn ⊑ otl).
 
-Inductive drf_pre_read_na (σ : state) V l : Prop :=
+Inductive drf_pre_read_na (σ : state) (V: View) (l: loc) : Prop :=
   | _singleton_drf_read_na
                             otl
                             (Local : V !! l = otl)
                             (Max : MaxTime (mem σ) l otl).
 
-Inductive init_pre (σ : state) V l : Prop :=
+Inductive init_pre (σ : state) (V: View) (l: loc) : Prop :=
   | _singleton_init
                     (tl : positive)
                     (Local : V !! l = Some tl)
@@ -413,7 +413,7 @@ Proof.
       econstructor; subst; eauto.
 Qed.
 
-Inductive alloc_pre (σ : state) V l : Prop :=
+Inductive alloc_pre (σ : state) (V: View) (l: loc) : Prop :=
   | _singleton_alloc
                     (tl : positive)
                     (Local : V !! l = Some tl)
@@ -943,4 +943,4 @@ Proof.
 Qed.
 
 Close Scope positive.
-End lifting.
\ No newline at end of file
+End lifting.
diff --git a/theories/rsl.v b/theories/rsl.v
index 10375227..a03eba2f 100644
--- a/theories/rsl.v
+++ b/theories/rsl.v
@@ -582,7 +582,7 @@ Instance InitRaw_persistent V jγ : PersistentP (InitRaw V jγ) := _.
       as (i) "[% #Hi]".
     destruct (frame_steps_RMW_branch _ _ _ H _ _ H0) as [I' [h' Eq]].
 
-    iMod ("SClose" $! (state_ISet_insert i s') ({[Change i]})
+    iMod ("SClose" $! (state_ISet_insert i s') ({[Change i]} : sts.tokens rsl_sts)
               with "[Inv]") as "(Inv & Own')". 
         { iSplitL "".
           - iPureIntro. by apply state_ISet_insert_steps.
@@ -1442,7 +1442,7 @@ Instance InitRaw_persistent V jγ : PersistentP (InitRaw V jγ) := _.
           by eapply frame_steps_steps. }
 
 
-      iMod ("HClose2" $! s'' {[Change i1; Change i2]} with "[Inv]")
+      iMod ("HClose2" $! s'' ({[Change i1; Change i2]} : sts.tokens rsl_sts) with "[Inv]")
         as "(Inv & Own)".
         { iSplitL "".
           - iPureIntro. by apply state_ISet_split_steps.
diff --git a/theories/viewpred.v b/theories/viewpred.v
index 3c91bd45..2a377f43 100644
--- a/theories/viewpred.v
+++ b/theories/viewpred.v
@@ -90,7 +90,7 @@ Section ViewPredicates.
   Global Instance vPred_upclose : UpClose (vPred) (vPred) := vPred_close.
   Global Instance vPred_vProp_upclose : UpClose (vPred) (View -> iProp) := λ P, {| ofe_mor_car := ((vPred_app P)) |}.
 
-  Definition vPred_impl_aux (P Q : vPred) :=
+  Definition vPred_impl_aux (P Q : vPred) : View -c> iProp :=
     ↑(λ V, vPred_app P V → vPred_app Q V)%I.
   Definition vPred_impl_mono (P Q : vPred) :
     vPred_Mono (vPred_impl_aux P Q) := vProp_upclose_mono _.
@@ -101,7 +101,7 @@ Section ViewPredicates.
     intros ?. by rewrite (H _) (H1 _).
   Qed.
 
-  Definition vPred_wand_aux P Q :=
+  Definition vPred_wand_aux P Q : View -c> iProp :=
     ↑(λ V, vPred_app P V -∗ vPred_app Q V)%I.
   Definition vPred_wand_mono P Q :
     vPred_Mono (vPred_wand_aux P Q) := vProp_upclose_mono _.
@@ -323,4 +323,4 @@ Notation "P ={ E }=> Q" := (P ={E,E}=> Q)%VP
 Arguments vPred [_].
 (* Arguments vPred_pred [_] _ : simpl never. *)
 Arguments vPred_app [_] _ _ : simpl never.
-Arguments vPred_mono [_ _] _ _ _.
\ No newline at end of file
+Arguments vPred_mono [_ _] _ _ _.
-- 
GitLab