From b4f5fe15c7d1362dc5f281e89a3cc1e2cf01c3fa Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 20 Sep 2019 18:50:25 +0200
Subject: [PATCH] First attempt at fixing compatibility with Coq master.
---
opam | 2 +-
theories/lang/arc.v | 16 ++++++++--------
theories/typing/lib/arc.v | 6 +++---
theories/typing/lib/rc/rc.v | 2 ++
theories/typing/lib/rwlock/rwlock.v | 4 ++--
theories/typing/lib/rwlock/rwlock_code.v | 6 +++---
.../typing/lib/rwlock/rwlockreadguard_code.v | 8 ++++----
.../typing/lib/rwlock/rwlockwriteguard_code.v | 6 +++---
theories/typing/programs.v | 2 +-
9 files changed, 27 insertions(+), 25 deletions(-)
diff --git a/opam b/opam
index f83032d2..fa500c00 100644
--- a/opam
+++ b/opam
@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
depends: [
- "coq-gpfsl" { (= "dev.2019-09-19.0.5c030976") | (= "dev") }
+ "coq-gpfsl" { (= "dev.2019-09-20.0.0f49245e") | (= "dev") }
]
diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index fbb6da04..6f25bc17 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -1,11 +1,11 @@
From Coq.QArith Require Import Qcanon.
-From iris.base_logic.lib Require Import invariants.
-From iris.proofmode Require Import tactics.
From iris.bi Require Import fractional.
+From iris.proofmode Require Import tactics.
From iris.algebra Require Import excl csum frac auth agree.
-From lrust.lang Require Import notation new_delete arc_cmra.
-From gpfsl.logic Require Import view_invariants.
+From iris.base_logic.lib Require Import invariants.
From gpfsl.gps Require Import middleware protocols.
+From gpfsl.logic Require Import view_invariants.
+From lrust.lang Require Import notation new_delete arc_cmra.
Set Default Proof Using "Type".
(* Rust Arc has a maximum number of clones to prevent overflow. We currently
@@ -728,13 +728,13 @@ Section arc.
{ iIntros "!>" (t' [] v' [_ Ext']). rewrite /StrongTok. iIntros "!>". iSplit.
- iIntros "#SI !>". iFrame "SI SMA". rewrite /StrongTok. iFrame "St".
iDestruct "SI" as (st) "[% Eq]". subst v'. iExists (Z_of_arcstrong_st st).
- destruct st as [[]|]; simpl; [|done]. iPureIntro. split; [done|lia].
+ destruct st as [[]|]; simpl; [|done]. iPureIntro. split; [done|split].
- iDestruct 1 as (st) "(Eq1 & SA & SI)". iDestruct "Eq1" as %?. subst v'.
destruct st as [[q' n]|]; simpl.
+ iModIntro. iFrame "SMA". rewrite /StrongTok. iFrame "St".
iSplitR""; [iExists (Some (q',n))|iExists (Z.pos n)].
* iSplitL""; [done|]. by iFrame.
- * iPureIntro. split; [done|lia].
+ * iPureIntro. split; [done|split].
+ iDestruct (StrongTok_Auth_agree with "[$SA St]") as %(?&?&EQ&?).
rewrite /StrongTok. iFrame "St". done. }
iIntros "!>" (t' [] v'). iDestruct 1 as "(_ & RR' & IS & Rs & St & SMA)".
@@ -1723,7 +1723,7 @@ Section arc.
iSplitR "SD"; [iExists _; iFrame "WU SeenU'"|]. by iExists _.
+ iSplitL "SDA". { rewrite /Q Pos2Z.id decide_False; [|done].
iSplitR ""; [by iExists _|done]. }
- rewrite decide_False; last first. { destruct n; try lia. done. }
+ rewrite decide_False; last first. { by destruct n; try lia. }
iDestruct "WA" as (q2 Eq2) "WA".
iExists (None, Some $ Cinl (q2, Pos.pred n)). iSplitL "".
{ iPureIntro. f_equal. by rewrite Z.sub_1_r -Pos2Z.inj_pred. }
@@ -2174,7 +2174,7 @@ Section arc.
{ by rewrite Qp_plus_assoc (Qp_plus_comm q2). } iFrame "HP".
iExists _,_. iFrame "R' SM SD SeenD' oW".
rewrite /Mt' (decide_False _ _ nEq). iFrame "SeenM'".
- rewrite decide_False; last first. { simpl. destruct n; try lia. done. }
+ rewrite decide_False; last first. { simpl. by destruct n; try lia. }
rewrite -Qp_plus_div. by iFrame "tok tok'". }
(* finally done with the CAS *)
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 967f2d59..6b25d86c 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -1,16 +1,16 @@
From Coq.QArith Require Import Qcanon.
+From iris.bi Require Import fractional.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth csum frac agree.
-From iris.bi Require Import fractional.
+
+From gpfsl.gps Require Import middleware protocols escrows.
From lrust.lang Require Import memcpy arc arc_cmra.
From lrust.lifetime Require Import at_borrow.
From lrust.typing Require Export type.
From lrust.typing Require Import typing option.
-From gpfsl.gps Require Import middleware protocols escrows.
-
Set Default Proof Using "Type".
Definition arcN := lrustN .@ "arc".
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index b0ffc6ab..f351f1dd 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -6,6 +6,8 @@ From lrust.typing Require Export type.
From lrust.typing Require Import typing option.
Set Default Proof Using "Type".
+Unset Printing Notations.
+
Definition rc_stR :=
prodUR (optionUR (csumR (prodR fracR positiveR) (exclR unitO))) natUR.
Class rcG Σ :=
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 06fc0cbb..3da2f344 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -1,10 +1,10 @@
From Coq.QArith Require Import Qcanon.
+From iris.bi Require Import fractional.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth excl csum frac agree.
-From iris.bi Require Import fractional.
+From gpfsl.gps Require Import middleware protocols.
From lrust.lifetime Require Import at_borrow.
From lrust.typing Require Import typing.
-From gpfsl.gps Require Import middleware protocols.
From lrust.logic Require Import gps.
Set Default Proof Using "Type".
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 3d29bd59..9c66a055 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -1,12 +1,12 @@
+From iris.bi Require Import fractional.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth csum frac agree.
-From iris.bi Require Import fractional.
+From gpfsl.gps Require Import middleware protocols.
+From lrust.logic Require Import gps.
From lrust.lang Require Import memcpy.
From lrust.lifetime Require Import at_borrow.
From lrust.typing Require Import typing option.
From lrust.typing.lib.rwlock Require Import rwlock rwlockreadguard rwlockwriteguard.
-From gpfsl.gps Require Import middleware protocols.
-From lrust.logic Require Import gps.
Set Default Proof Using "Type".
(** SYNCHRONIZATION CONDITIONS of rwlock *)
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index a1d00eb5..aae742a9 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -1,12 +1,12 @@
From Coq.QArith Require Import Qcanon.
+From iris.bi Require Import fractional.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth csum frac agree.
-From iris.bi Require Import fractional.
+From gpfsl.gps Require Import middleware protocols.
+From lrust.logic Require Import gps.
From lrust.lifetime Require Import at_borrow.
From lrust.typing Require Import typing.
From lrust.typing.lib.rwlock Require Import rwlock rwlockreadguard.
-From gpfsl.gps Require Import middleware protocols.
-From lrust.logic Require Import gps.
Set Default Proof Using "Type".
Section rwlockreadguard_functions.
@@ -161,7 +161,7 @@ Section rwlockreadguard_functions.
tctx_hasty_val' //=; simpl.
iFrame "Hx". iExists _,_,_,_. iFrame "Hx' Hαβ Hν H◯ H†".
iExists _,_,_. iSplitL "R''".
- - iExists _,_; by iDestruct "R''" as "[$ ?]".
+ - iExists _,_; by iDestruct "R''" as "[$ ?]".
- iFrame "EqO EqS". iExists _,_. by iFrame "R'". }
iApply type_jump; solve_typing.
Qed.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 6d0fa49c..4c9a3ca3 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -1,12 +1,12 @@
From Coq.QArith Require Import Qcanon.
+From iris.bi Require Import fractional.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth csum frac agree.
-From iris.bi Require Import fractional.
+From gpfsl.gps Require Import middleware.
+From lrust.logic Require Import gps.
From lrust.lifetime Require Import at_borrow.
From lrust.typing Require Import typing.
From lrust.typing.lib.rwlock Require Import rwlock rwlockwriteguard.
-From gpfsl.gps Require Import middleware.
-From lrust.logic Require Import gps.
Set Default Proof Using "Type".
Section rwlockwriteguard_functions.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 2be078c8..1b3d3a74 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -1,6 +1,6 @@
From gpfsl.logic Require Import proofmode.
From lrust.lang Require Export memcpy.
-From lrust.typing Require Export type lft_contexts type_context cont_context.
+From lrust.typing Require Export lft_contexts type_context cont_context type.
Set Default Proof Using "Type".
Implicit Types tid : thread_id.
--
GitLab