Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Dmitry Khalanskiy
Iris
Commits
d5763982
Commit
d5763982
authored
Dec 19, 2019
by
Tej Chajed
Committed by
Ralf Jung
Dec 19, 2019
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
[doc] Fix links to doc files
parent
359c21c2
Changes
5
Hide whitespace changes
Inline
Sidebyside
Showing
5 changed files
with
15 additions
and
15 deletions
+15
15
README.md
README.md
+3
3
docs/heap_lang.md
docs/heap_lang.md
+1
1
docs/proof_guide.md
docs/proof_guide.md
+3
3
docs/proof_mode.md
docs/proof_mode.md
+4
4
docs/style_guide.md
docs/style_guide.md
+4
4
No files found.
README.md
View file @
d5763982
...
...
@@ 9,7 +9,7 @@ For using the Coq library, check out the
For understanding the theory of Iris, a LaTeX version of the core logic
definitions and some derived forms is available in
[
docs
/iris.tex
](
tex/iris.tex
)
. A compiled PDF version of this document is
[
tex
/iris.tex
](
tex/iris.tex
)
. A compiled PDF version of this document is
[
available online
](
http://plv.mpisws.org/iris/appendix3.2.pdf
)
.
## Building Iris
...
...
@@ 83,7 +83,7 @@ followed by `make builddep`.
[
MoSeL
](
http://irisproject.org/mosel/
)
, which extends Coq with contexts for
intuitionistic and spatial BI++ assertions. It also contains tactics for
interactive proofs. Documentation can be found in
[
P
roof
M
ode.md
](
docs/proof_mode.md
)
.
[
p
roof
_m
ode.md
](
docs/proof_mode.md
)
.
*
The folder
[
heap_lang
](
theories/heap_lang
)
defines the MLlike concurrent heap
language
*
The subfolder
[
lib
](
theories/heap_lang/lib
)
contains a few derived
...
...
@@ 137,7 +137,7 @@ Contacting the developers:
Miscellaneous:
*
Information on how to set up your editor for unicode input and output is
collected in
[
E
ditor.md
](
docs/editor.md
)
.
collected in
[
e
ditor.md
](
docs/editor.md
)
.
*
If you are writing a paper that uses Iris in one way or another, you could use
the
[
Iris LaTeX macros
](
tex/iris.sty
)
for typesetting the various Iris
connectives.
docs/heap_lang.md
View file @
d5763982
...
...
@@ 100,7 +100,7 @@ Further tactics:
the goal is for a single, atomic operation 
`wp_bind`
can be used to bring
the goal into the right shape.

`wp_apply pm_trm`
: Apply a lemma whose conclusion is a
`WP`
, automatically
applying
`wp_bind`
as needed. See the
[
ProofMode docs
](
P
roof
M
ode.md
)
for an
applying
`wp_bind`
as needed. See the
[
ProofMode docs
](
./p
roof
_m
ode.md
)
for an
explanation of
`pm_trm`
.
There is no tactic for
`Fork`
, just do
`wp_apply wp_fork`
.
...
...
docs/proof_guide.md
View file @
d5763982
...
...
@@ 2,9 +2,9 @@
This workinprogress document serves to explain how Iris proofs are typically
carried out in Coq: what are the common patterns, what are the common pitfalls.
This complements the tactic documentation for the
[
proof mode
](
P
roof
M
ode.md
)
and
[
HeapLang
](
H
eap
L
ang.md
)
as well as the documentation of syntactic conventions in
the
[
style guide
](
S
tyle
G
uide.md
)
.
This complements the tactic documentation for the
[
proof mode
](
./p
roof
_m
ode.md
)
and
[
HeapLang
](
./h
eap
_l
ang.md
)
as well as the documentation of syntactic conventions in
the
[
style guide
](
./s
tyle
_g
uide.md
)
.
## Order of `Requires`
...
...
docs/proof_mode.md
View file @
d5763982
...
...
@@ 3,7 +3,7 @@ Tactic overview
Many of the tactics below apply to more goals than described in this document
since the behavior of these tactics can be tuned via instances of the type
classes in the file
[
proofmode/classes
](
proofmode/classes.v
)
. Most notably, many
classes in the file
[
proofmode/classes
](
theories/
proofmode/classes.v
)
. Most notably, many
of the tactics can be applied when the connective to be introduced or to be eliminated
appears under a later, an update modality, or in the conclusion of a
weakest precondition.
...
...
@@ 260,12 +260,12 @@ For example, given:
You can write
iIntros (x Hx) "!
#
$ [[]  #[HQ HR]] /= !>".
iIntros (x Hx) "!
>
$ [[]  #[HQ HR]] /= !>".
which results in:
x : nat
H : x = 0
H
x
: x = 0
______________________________________(1/1)
"HQ" : Q
"HR" : R
...
...
@@ 361,4 +361,4 @@ HeapLang tactics
================
If you came here looking for the
`wp_`
tactics, those are described in the
[
HeapLang documentation
](
H
eap
L
ang.md
)
.
[
HeapLang documentation
](
./h
eap
_l
ang.md
)
.
docs/style_guide.md
View file @
d5763982
...
...
@@ 2,8 +2,8 @@
This document lays down syntactic conventions about how we usually write our
Iris proofs in Coq. It is a workinprogress. This complements the tactic
documentation for the
[
proof mode
](
P
roof
M
ode.md
)
and
[
HeapLang
](
H
eap
L
ang.md
)
as
well as the
[
proof guide
](
P
roof
G
uide.md
)
.
documentation for the
[
proof mode
](
./p
roof
_m
ode.md
)
and
[
HeapLang
](
./h
eap
_l
ang.md
)
as
well as the
[
proof guide
](
.doco/p
roof
_g
uide.md
)
.
## Implicit generalization
...
...
@@ 114,8 +114,8 @@ is used by clients.
*
R: cameras
*
UR: unital cameras or resources algebras
*
F: functors (can be combined with all of the above, e.g. OF is an OFE functor)
*
G: global camera functor management (typeclass; see
`P
roof
G
uide.md
`
)
*
G: global camera functor management (typeclass; see
[
p
roof
\_g
uide.md
](
./proof_guide.md
)
)
*
I: bunched implication logic (of type
`bi`
)
*
SI: stepindexed bunched implication logic (of type
`sbi`
)
*
T: canonical structures for algebraic classes (for example ofeT for OFEs, cmraT for cameras)
*
Σ: global camera functor management (
`gFunctors`
; see
`P
roof
G
uide.md
`
)
*
Σ: global camera functor management (
`gFunctors`
; see
[
p
roof
\_g
uide.md
](
./proof_guide.md
)
)
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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