From 74f756e49369ccb8c7f73ec4bee5b16fb12e2f13 Mon Sep 17 00:00:00 2001
From: Tej Chajed
Date: Thu, 19 Dec 2019 09:57:02 0500
Subject: [PATCH 1/4] [doc] Fix links to doc files

README.md  4 ++
docs/heap_lang.md  2 +
docs/proof_guide.md  6 +++
docs/proof_mode.md  2 +
docs/style_guide.md  10 +++++
5 files changed, 12 insertions(+), 12 deletions()
diff git a/README.md b/README.md
index 94d6075c6..d656b1c5a 100644
 a/README.md
+++ b/README.md
@@ 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
 [ProofMode.md](docs/proof_mode.md).
+ [proof_modProofModoe.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 [Editor.md](docs/editor.md).
+ collected in [editor.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.
diff git a/docs/heap_lang.md b/docs/heap_lang.md
index e3522e369..4897a8cd4 100644
 a/docs/heap_lang.md
+++ b/docs/heap_lang.md
@@ 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](ProofMode.md) for an
+ applying `wp_bind` as needed. See the [ProofMode docs](proof_mode.md) for an
explanation of `pm_trm`.
There is no tactic for `Fork`, just do `wp_apply wp_fork`.
diff git a/docs/proof_guide.md b/docs/proof_guide.md
index 81fb49820..0701e5648 100644
 a/docs/proof_guide.md
+++ b/docs/proof_guide.md
@@ 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](ProofMode.md) and
[HeapLang](HeapLang.md) as well as the documentation of syntactic conventions in
the [style guide](StyleGuide.md).
+This complements the tactic documentation for the [proof mode](docs/proof_mode.md) and
+[HeapLang](docs/heap_lang.md) as well as the documentation of syntactic conventions in
+the [style guide](docs/style_guide.md).
## Order of `Requires`
diff git a/docs/proof_mode.md b/docs/proof_mode.md
index 990a7a44e..5eaf4a041 100644
 a/docs/proof_mode.md
+++ b/docs/proof_mode.md
@@ 361,4 +361,4 @@ HeapLang tactics
================
If you came here looking for the `wp_` tactics, those are described in the
[HeapLang documentation](HeapLang.md).
+[HeapLang documentation](docs/heap_lang.md).
diff git a/docs/style_guide.md b/docs/style_guide.md
index f6bae4b6c..09f3a09ab 100644
 a/docs/style_guide.md
+++ b/docs/style_guide.md
@@ 1,9 +1,9 @@
# Iris Style Guide

+ProofModo
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](ProofMode.md) and [HeapLang](HeapLang.md) as
well as the [proof guide](ProofGuide.md).
+documentation for the [proof mode](docs/proof_mode.md) and [HeapLang](docs/heap_lang.md) as
+well as the [proof guide](docs/proof_guide.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 `ProofGuide.md`)
+* G: global camera functor management (typeclass; see [proof\_guide.md](docs/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 `ProofGuide.md`)
+* Σ: global camera functor management (`gFunctors`; see [proof\_guide.md](docs/proof_guide.md))

GitLab
From 8338c7c421017b1b0f91bae913c26c8214357afa Mon Sep 17 00:00:00 2001
From: Tej Chajed
Date: Thu, 19 Dec 2019 10:01:38 0500
Subject: [PATCH 2/4] [doc] Use !> in iIntros example

docs/proof_mode.md  2 +
1 file changed, 1 insertion(+), 1 deletion()
diff git a/docs/proof_mode.md b/docs/proof_mode.md
index 5eaf4a041..1b82c5736 100644
 a/docs/proof_mode.md
+++ b/docs/proof_mode.md
@@ 260,7 +260,7 @@ For example, given:
You can write
 iIntros (x Hx) "!# $ [[]  #[HQ HR]] /= !>".
+ iIntros (x Hx) "!> $ [[]  #[HQ HR]] /= !>".
which results in:

GitLab
From 75ca36b7e141b4051bad7dba86148210cc6b73bc Mon Sep 17 00:00:00 2001
From: Tej Chajed
Date: Thu, 19 Dec 2019 10:40:40 0500
Subject: [PATCH 3/4] Fixes to doc fixes

README.md  2 +
docs/proof_mode.md  2 +
2 files changed, 2 insertions(+), 2 deletions()
diff git a/README.md b/README.md
index d656b1c5a..13aa94278 100644
 a/README.md
+++ b/README.md
@@ 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
 [proof_modProofModoe.md](docs/proof_mode.md).
+ [proof_mode.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
diff git a/docs/proof_mode.md b/docs/proof_mode.md
index 1b82c5736..4f7c39388 100644
 a/docs/proof_mode.md
+++ b/docs/proof_mode.md
@@ 265,7 +265,7 @@ You can write
which results in:
x : nat
 H : x = 0
+ Hx : x = 0
______________________________________(1/1)
"HQ" : Q
"HR" : R

GitLab
From 07175adc1657bac28ddc88ddb00a9c6fe1962d21 Mon Sep 17 00:00:00 2001
From: Tej Chajed
Date: Thu, 19 Dec 2019 11:58:19 0500
Subject: [PATCH 4/4] Use relative links

README.md  2 +
docs/heap_lang.md  2 +
docs/proof_guide.md  6 +++
docs/proof_mode.md  4 ++
docs/style_guide.md  10 +++++
5 files changed, 12 insertions(+), 12 deletions()
diff git a/README.md b/README.md
index 13aa94278..ccb04694a 100644
 a/README.md
+++ b/README.md
@@ 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
diff git a/docs/heap_lang.md b/docs/heap_lang.md
index 4897a8cd4..682410d3a 100644
 a/docs/heap_lang.md
+++ b/docs/heap_lang.md
@@ 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](proof_mode.md) for an
+ applying `wp_bind` as needed. See the [ProofMode docs](./proof_mode.md) for an
explanation of `pm_trm`.
There is no tactic for `Fork`, just do `wp_apply wp_fork`.
diff git a/docs/proof_guide.md b/docs/proof_guide.md
index 0701e5648..c3de71761 100644
 a/docs/proof_guide.md
+++ b/docs/proof_guide.md
@@ 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](docs/proof_mode.md) and
[HeapLang](docs/heap_lang.md) as well as the documentation of syntactic conventions in
the [style guide](docs/style_guide.md).
+This complements the tactic documentation for the [proof mode](./proof_mode.md) and
+[HeapLang](./heap_lang.md) as well as the documentation of syntactic conventions in
+the [style guide](./style_guide.md).
## Order of `Requires`
diff git a/docs/proof_mode.md b/docs/proof_mode.md
index 4f7c39388..60229568a 100644
 a/docs/proof_mode.md
+++ b/docs/proof_mode.md
@@ 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.
@@ 361,4 +361,4 @@ HeapLang tactics
================
If you came here looking for the `wp_` tactics, those are described in the
[HeapLang documentation](docs/heap_lang.md).
+[HeapLang documentation](./heap_lang.md).
diff git a/docs/style_guide.md b/docs/style_guide.md
index 09f3a09ab..65fd05759 100644
 a/docs/style_guide.md
+++ b/docs/style_guide.md
@@ 1,9 +1,9 @@
# Iris Style Guide
ProofModo
+
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](docs/proof_mode.md) and [HeapLang](docs/heap_lang.md) as
well as the [proof guide](docs/proof_guide.md).
+documentation for the [proof mode](./proof_mode.md) and [HeapLang](./heap_lang.md) as
+well as the [proof guide](.doco/proof_guide.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 [proof\_guide.md](docs/proof_guide.md))
+* G: global camera functor management (typeclass; see [proof\_guide.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 [proof\_guide.md](docs/proof_guide.md))
+* Σ: global camera functor management (`gFunctors`; see [proof\_guide.md](./proof_guide.md))

GitLab