depend on nightly Iris and fix build

README.md

@@ -10,7 +10,7 @@ This tutorial comes in two versions:
 For the tutorial material you need to have the following dependencies installed:
 
 - Coq 8.10.2 / 8.11.2 / 8.12.0
-- [Iris](https://gitlab.mpi-sws.org/iris/iris) 3.3.0
+ - A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris)
 
 *Note:* the tutorial material will not work with earlier versions of Iris, it
 is important to install the exact versions as given above.
@@ -29,7 +29,15 @@ done so earlier):
     opam repo add coq-released https://coq.inria.fr/opam/released
     opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
 
-Then you can do `make build-dep` to install exactly the right version of Iris.
+Once you got opam set up, run `make build-dep` to install the right versions
+of the dependencies.
+
+Run `make -jN` to build the full development, where `N` is the number of your
+CPU cores.
+
+To update, do `git pull`.  After an update, the development may fail to compile
+because of outdated dependencies.  To fix that, please run `opam update`
+followed by `make build-dep`.
 
 ## Compiling the exercises
 

exercises/ex_04_parallel_add.v

@@ -83,7 +83,7 @@ Section proof2.
     own γ (●E n) -∗ own γ (◯E m) -∗ ⌜ n = m ⌝.
   Proof.
     iIntros "Hγ● Hγ◯".
-    by iDestruct (own_valid_2 with "Hγ● Hγ◯") as %?%excl_auth_agreeL.
+    by iDestruct (own_valid_2 with "Hγ● Hγ◯") as %?%excl_auth_agree_L.
   Qed.
 
   Lemma ghost_var_update γ n' n m :

exercises/ex_05_parallel_add_mul.v

@@ -42,7 +42,7 @@ Section proof.
     own γ (●E b) -∗ own γ (◯E c) -∗ ⌜ b = c ⌝.
   Proof.
     iIntros "Hγ● Hγ◯".
-    by iDestruct (own_valid_2 with "Hγ● Hγ◯") as %<-%excl_auth_agreeL.
+    by iDestruct (own_valid_2 with "Hγ● Hγ◯") as %<-%excl_auth_agree_L.
   Qed.
 
   Lemma ghost_var_update γ b' b c :

opam

@@ -9,7 +9,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/tutorial-popl18.git"
 synopsis: "The Iris tutorial at POPL 2018"
 
 depends: [
-  "coq-iris" { (= "3.3.0") | (= "dev") }
+  "coq-iris" { (= "dev.2020-09-15.2.59280f68") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]

solutions/ex_04_parallel_add.v

@@ -98,7 +98,7 @@ Section proof2.
     own γ (●E n) -∗ own γ (◯E m) -∗ ⌜ n = m ⌝.
   Proof.
     iIntros "Hγ● Hγ◯".
-    by iDestruct (own_valid_2 with "Hγ● Hγ◯") as %?%excl_auth_agreeL.
+    by iDestruct (own_valid_2 with "Hγ● Hγ◯") as %?%excl_auth_agree_L.
   Qed.
 
   Lemma ghost_var_update γ n' n m :
@@ -199,7 +199,7 @@ Section proof3.
     - iIntros (??) "[Hγ1◯ Hγ2◯] !>". wp_seq.
       wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "(Hr & Hγ●)".
       wp_seq. wp_load. iCombine "Hγ1◯ Hγ2◯" as "Hγ◯".
-      iDestruct (own_valid_2 with "Hγ● Hγ◯") as %->%frac_auth_agreeL.
+      iDestruct (own_valid_2 with "Hγ● Hγ◯") as %->%frac_auth_agree_L.
       by iApply "Post".
   Qed.
   (* END SOLUTION BEGIN TEMPLATE

solutions/ex_05_parallel_add_mul.v

@@ -42,7 +42,7 @@ Section proof.
     own γ (●E b) -∗ own γ (◯E c) -∗ ⌜ b = c ⌝.
   Proof.
     iIntros "Hγ● Hγ◯".
-    by iDestruct (own_valid_2 with "Hγ● Hγ◯") as %<-%excl_auth_agreeL.
+    by iDestruct (own_valid_2 with "Hγ● Hγ◯") as %<-%excl_auth_agree_L.
   Qed.
 
   Lemma ghost_var_update γ b' b c :