From ca41e9e75f9ad015d080810016b892addb5f5993 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Sat, 23 Mar 2019 11:40:43 +0100
Subject: [PATCH] Bump Iris version
---
guix.scm | 12 ++++++------
opam | 2 +-
theories/logic/spec_rules.v | 3 +--
3 files changed, 8 insertions(+), 9 deletions(-)
diff --git a/guix.scm b/guix.scm
index 5c515ab..ca9072b 100644
--- a/guix.scm
+++ b/guix.scm
@@ -30,8 +30,10 @@
#:use-module (gnu packages coq)
#:use-module ((guix licenses) #:prefix license:))
-(define stdpp-commit "f948024480ee7ab247be51cef058d21e36e3df24")
-(define iris-commit "2d1c83520d8c2656d1868dfa6d7e8a95fe3c6c4c")
+(define stdpp-commit "700545bb31db8c5268a6813bebaf0e4115d229d9")
+(define stdpp-sha256 (base32 "0i469sk69qb0bjxjaykralc3fr2zw2241dy350slydkas90xmjwk")) ;; sha256 hash of the specific std++ checkout
+(define iris-commit "9936cb1238afbd21e2202ecdb72c844b3c572f80")
+(define iris-sha256 (base32 "0jqk71197irjx0mpdmhb7bdlgyhjim172arjqal8chm3miwiag7f")) ;; sha256 hash of the specific std++ checkout
(define %source-dir (dirname (current-filename)))
(define-public coq-stdpp
@@ -47,8 +49,7 @@
(url "https://gitlab.mpi-sws.org/iris/stdpp.git")
(commit commit)))
(file-name (git-file-name name version))
- (sha256
- (base32 "08myrcbxag16vr9axys7cvxqlgnpb5bxn9q7cmr3j84m31rn4s39"))))
+ (sha256 stdpp-sha256)))
(build-system gnu-build-system)
(native-inputs
`( ;; need for egrep for tests
@@ -87,8 +88,7 @@
(url "https://gitlab.mpi-sws.org/iris/iris.git")
(commit commit)))
(file-name (git-file-name name version))
- (sha256
- (base32 "1hlihcds432h367k8dijqsbzycf4lczdm0pw2p2xpwizagqwjv9b"))))
+ (sha256 iris-sha256)))
(build-system gnu-build-system)
(native-inputs
`(;; need for egrep for tests
diff --git a/opam b/opam
index 7a115b0..994b1f7 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
depends: [
- "coq-iris" { (= "dev.2019-03-15.0.33ee70bf") | (= "dev") }
+ "coq-iris" { (= "dev.2019-03-22.0.9936cb12") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index dc3d786..1904ed2 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -132,8 +132,7 @@ Section rules.
iFrame. iApply "Hclose". iNext.
iExists (<[j:=fill K #()]> tp), σ.
rewrite to_tpool_insert'; last eauto. iFrame. iPureIntro.
- eapply rtc_r, step_insert_no_fork; eauto.
- eapply (ResolveProphS #p _ (of_val w)); eauto.
+ eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
Qed.
(** Alloc, load, and store *)
--
GitLab