fix and test building with Coq 8.12

.gitlab-ci.yml

@@ -27,10 +27,10 @@ variables:
 
 ## Build jobs
 
-#build-coq.8.12.dev: # not compatible with iris-string-ident
-#  <<: *template
-#  variables:
-#    OPAM_PINS: "coq version 8.12.dev"
+build-coq.8.12.0:
+  <<: *template
+  variables:
+    OPAM_PINS: "coq version 8.12.0"
 
 build-coq.8.11.2:
   <<: *template
@@ -42,7 +42,7 @@ build-coq.8.11.2:
 build-iris.dev:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.11.dev   coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV   coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV"
+    OPAM_PINS: "coq version 8.12.dev   coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV   coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV"
   except:
   only:
   - triggers

README.md

@@ -6,7 +6,7 @@ Some example verification demonstrating the use of Iris.
 
 This version is known to compile with:
 
- - Coq 8.11.2
+ - Coq 8.11.2 / 8.12.0
  - A development version of [Iris](https://gitlab.mpi-sws.org/FP/iris-coq/)
  - The coq86-devel branch of [Autosubst](https://github.com/uds-psl/autosubst)
 

opam

@@ -9,7 +9,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/FP/iris-examples.git"
 synopsis: "A collection of case studies for Iris"
 
 depends: [
-  "coq-iris" { (= "dev.2020-07-21.2.e989ad6b") | (= "dev") }
+  "coq-iris" { (= "dev.2020-08-07.0.dc3d182b") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
   "coq-iris-string-ident"
 ]

theories/barrier/proof.v

@@ -114,7 +114,7 @@ Proof.
   set (γsps' := γsps ∖ {[γsp]}).
   iMod (saved_prop_alloc_cofinite γsps' R1) as (γsp1 Hγsp1) "#Hsp1".
   iMod (saved_prop_alloc_cofinite (γsps' ∪ {[ γsp1 ]}) R2)
-    as (γsp2 [? ?%not_elem_of_singleton]%not_elem_of_union) "#Hsp2".
+    as (γsp2 [? ?%not_elem_of_singleton_1]%not_elem_of_union) "#Hsp2".
   iMod (own_update _ _ (● _ ⋅ (◯ GSet {[ γsp1 ]} ⋅ ◯ (GSet {[ γsp2 ]})))
     with "H●") as "(H● & H◯1 & H◯2)".
   { rewrite -auth_frag_op gset_disj_union; last set_solver.
@@ -128,8 +128,8 @@ Proof.
     iDestruct (saved_prop_agree with "Hsp Hsp'") as "#Heq".
     iAssert (▷ R')%I with "[HR'']" as "HR'"; [iNext; by iRewrite "Heq"|].
     iDestruct ("HR" with "HR'") as "[HR1 HR2]".
-    iApply big_sepS_union; [set_solver|iFrame "HRs"].
-    iApply big_sepS_union; [set_solver|].
+    iApply big_sepS_union; first set_solver. iFrame "HRs".
+    iApply big_sepS_union; first set_solver.
     iSplitL "HR1"; rewrite big_sepS_singleton; eauto. }
   iModIntro; iSplitL "H◯1".
   - iExists γ, P, R1, γsp1. iFrame; auto.

theories/logatom/herlihy_wing_queue/hwq.v

@@ -2668,7 +2668,7 @@ Proof.
         - intros k. split; intros Hk; first by apply Hstate.
           intros Hk_in_deqs. apply elem_of_union in Hk_in_deqs.
           destruct Hk_in_deqs as [Hk_is_i|Hk_in_deqs].
-          + apply elem_of_singleton in Hk_is_i. subst k.
+          + apply elem_of_singleton_1 in Hk_is_i. subst k.
             rewrite /array_get Hslots_i decide_False in Hi; last done.
             rewrite /physical_value in Hi. rewrite Hslots_i in Hk.
             inversion Hk; subst dw. inversion Hi.
@@ -2690,7 +2690,7 @@ Proof.
             apply NoDup_app in Hpvs_ND as (HND & _ & _).
             apply NoDup_app in HND as (HND & _ & _).
             apply NoDup_cons in HND as (HND & _). apply HND, Hk.
-        - intros k Hk. apply elem_of_union in Hk as [Hk%elem_of_singleton|Hk].
+        - intros k Hk. apply elem_of_union in Hk as [Hk%elem_of_singleton_1|Hk].
           + subst k. rewrite Hslots_i /=.
             assert (dw = true) as ->.
             { rewrite /array_get Hslots_i decide_False in Hi; last done.