Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
examples
Commits
c75b4277
Commit
c75b4277
authored
Feb 19, 2019
by
Ralf Jung
Browse files
fix uses of wp_par
parent
d586b5fc
Pipeline
#14773
failed with stage
in 9 minutes and 38 seconds
Changes
2
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
opam
View file @
c75b4277
...
...
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [
"coq-iris" { (= "dev.2019-0
1-27.0.9896799d
") | (= "dev") }
"coq-iris" { (= "dev.2019-0
2-18.1.a1cf5cb9
") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
theories/barrier/example_client.v
View file @
c75b4277
...
...
@@ -41,8 +41,8 @@ Section client.
Proof
.
iIntros
""
;
rewrite
/
client
.
wp_alloc
y
as
"Hy"
.
wp_let
.
wp_apply
(
newbarrier_spec
N
(
y_inv
1
y
)
with
"[//]"
).
iIntros
(
l
)
"[Hr Hs]"
.
wp_let
.
iA
pply
(
wp_par
(
λ
_
,
True
%
I
)
(
λ
_
,
True
%
I
)
with
"[Hy Hs] [Hr]"
)
;
last
auto
.
iIntros
(
l
)
"[Hr Hs]"
.
wp_a
pply
(
wp_par
(
λ
_
,
True
%
I
)
(
λ
_
,
True
%
I
)
with
"[Hy Hs] [Hr]"
)
;
last
auto
.
-
(* The original thread, the sender. *)
wp_store
.
iApply
(
signal_spec
with
"[-]"
)
;
last
by
iNext
;
auto
.
iSplitR
"Hy"
;
first
by
eauto
.
...
...
@@ -51,7 +51,7 @@ Section client.
iDestruct
(
recv_weaken
with
"[] Hr"
)
as
"Hr"
.
{
iIntros
"Hy"
.
by
iApply
(
y_inv_split
with
"Hy"
).
}
iMod
(
recv_split
with
"Hr"
)
as
"[H1 H2]"
;
first
done
.
iA
pply
(
wp_par
(
λ
_
,
True
%
I
)
(
λ
_
,
True
%
I
)
with
"[H1] [H2]"
)
;
last
auto
.
wp_a
pply
(
wp_par
(
λ
_
,
True
%
I
)
(
λ
_
,
True
%
I
)
with
"[H1] [H2]"
)
;
last
auto
.
+
by
iApply
worker_safe
.
+
by
iApply
worker_safe
.
Qed
.
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment