From 3e12b4d9bc70f56530b9870f87b32707f289cf7e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 19 Jun 2020 09:48:56 +0200
Subject: [PATCH] update dependencies and Makefile, import numbers
---
Makefile | 2 +-
opam | 2 +-
theories/lang/arc_cmra.v | 2 +-
theories/lifetime/model/creation.v | 2 +-
theories/lifetime/model/definitions.v | 2 +-
theories/lifetime/model/faking.v | 2 +-
theories/lifetime/model/reborrow.v | 2 +-
theories/typing/lib/rc/rc.v | 2 +-
theories/typing/lib/rc/weak.v | 2 +-
theories/typing/lib/refcell/ref_code.v | 2 +-
theories/typing/lib/refcell/refcell.v | 2 +-
theories/typing/lib/refcell/refmut_code.v | 2 +-
theories/typing/lib/rwlock/rwlock.v | 2 +-
theories/typing/lib/rwlock/rwlockreadguard_code.v | 2 +-
theories/typing/product.v | 2 +-
theories/typing/product_split.v | 1 +
theories/typing/type.v | 1 +
17 files changed, 17 insertions(+), 15 deletions(-)
diff --git a/Makefile b/Makefile
index 8d615e4b..331cb03f 100644
--- a/Makefile
+++ b/Makefile
@@ -8,7 +8,7 @@ all: Makefile.coq
clean: Makefile.coq
+@make -f Makefile.coq clean
- find theories tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
+ find theories tests exercises solutions \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
rm -f Makefile.coq .lia.cache
.PHONY: clean
diff --git a/opam b/opam
index df51f920..46fb02f8 100644
--- a/opam
+++ b/opam
@@ -16,7 +16,7 @@ This branch uses a proper weak memory model.
"""
depends: [
- "coq-gpfsl" { (= "dev.2020-06-06.0.d7449e86") | (= "dev") }
+ "coq-gpfsl" { (= "dev.2020-06-19.0.1c30e9d2") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/lang/arc_cmra.v b/theories/lang/arc_cmra.v
index 09bfa2b4..07ec46d1 100644
--- a/theories/lang/arc_cmra.v
+++ b/theories/lang/arc_cmra.v
@@ -2,7 +2,7 @@ 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.algebra Require Import excl csum frac auth agree.
+From iris.algebra Require Import excl csum frac auth agree numbers.
From lrust.lang Require Import notation.
From gpfsl.gps Require Import middleware protocols.
From gpfsl.logic Require Import view_invariants.
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index b1bb4138..df30fe50 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -1,6 +1,6 @@
From lrust.lifetime Require Export primitive.
From lrust.lifetime Require Import faking.
-From iris.algebra Require Import csum auth frac gmap agree gset.
+From iris.algebra Require Import csum auth frac gmap agree gset numbers.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type*".
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 53db3b02..ee6fbc85 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Import csum auth excl frac gmap agree gset.
+From iris.algebra Require Import csum auth excl frac gmap agree gset numbers.
From lrust.lifetime.model Require Import boxes.
From lrust.lifetime Require Export lifetime_sig.
From gpfsl.base_logic Require Export lattice_cmra.
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 0704936e..23f13c27 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -1,5 +1,5 @@
From lrust.lifetime.model Require Export primitive.
-From iris.algebra Require Import csum auth excl frac gmap agree gset.
+From iris.algebra Require Import csum auth excl frac gmap agree gset numbers.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type*".
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index debb35eb..0622b412 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -1,5 +1,5 @@
From lrust.lifetime Require Import borrow accessors.
-From iris.algebra Require Import csum auth excl frac gmap agree gset.
+From iris.algebra Require Import csum auth excl frac gmap agree gset numbers.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type*".
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 35a255fb..a098f55a 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -1,5 +1,5 @@
From Coq.QArith Require Import Qcanon.
-From iris.algebra Require Import auth excl csum frac agree.
+From iris.algebra Require Import auth excl csum frac agree numbers.
From lrust.lang Require Import memcpy.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Export type.
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index b91f07af..77586f49 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -1,6 +1,6 @@
From Coq.QArith Require Import Qcanon.
From iris.proofmode Require Import tactics.
-From iris.algebra Require Import auth csum frac agree.
+From iris.algebra Require Import auth csum frac agree numbers.
From lrust.lang Require Import memcpy.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Export type.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 4ea4c7c5..4a42835e 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -1,5 +1,5 @@
From Coq.QArith Require Import Qcanon.
-From iris.algebra Require Import auth csum frac agree.
+From iris.algebra Require Import auth csum frac agree numbers.
From iris.bi Require Import fractional.
From lrust.lifetime Require Import lifetime na_borrow.
From lrust.typing Require Import typing.
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index 45cb8549..1341fca8 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Import auth csum frac agree.
+From iris.algebra Require Import auth csum frac agree numbers.
From iris.bi Require Import fractional.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Import typing.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 8863fcbc..bc776aba 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -1,5 +1,5 @@
From Coq.QArith Require Import Qcanon.
-From iris.algebra Require Import auth csum frac agree.
+From iris.algebra Require Import auth csum frac agree numbers.
From iris.bi Require Import fractional.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Import typing.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 5efbe556..248132e6 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -1,7 +1,7 @@
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.algebra Require Import auth excl csum frac agree numbers.
From gpfsl.gps Require Import middleware protocols.
From lrust.lifetime Require Import at_borrow.
From lrust.typing Require Import typing.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index aae742a9..ecd96a97 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -1,7 +1,7 @@
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.algebra Require Import auth csum frac agree numbers.
From gpfsl.gps Require Import middleware protocols.
From lrust.logic Require Import gps.
From lrust.lifetime Require Import at_borrow.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index a1c70ad9..9abc418e 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -1,5 +1,5 @@
From iris.proofmode Require Import tactics.
-From iris.algebra Require Import list.
+From iris.algebra Require Import list numbers.
From lrust.typing Require Import lft_contexts.
From lrust.typing Require Export type.
Set Default Proof Using "Type".
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index ac417767..4463e0d1 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -1,4 +1,5 @@
From Coq Require Import Qcanon.
+From iris.algebra Require Import numbers.
From iris.proofmode Require Import tactics.
From lrust.typing Require Export type.
From lrust.typing Require Import type_context lft_contexts product own uniq_bor shr_bor.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 1ed100d0..7515f0b3 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -1,3 +1,4 @@
+From iris.algebra Require Import numbers.
From gpfsl.lang Require Export notation.
From gpfsl.base_logic Require Export na.
From gpfsl.logic Require Export na_invariants.
--
GitLab