Skip to content
Snippets Groups Projects
Commit 0005c5d9 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'ralf/style_guide' into 'master' 

Reformat style guide

See merge request iris/iris!1072
parents a92765d3 a658b538
Branches
Tags
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 156 additions and 157 deletions
docs/style_guide.md
+ 156
− 157
View file @ 0005c5d9
......@@ -9,203 +9,202 @@ so we can add it.
### Binders
**Good:** `(a : B)`
**Bad:** `(a:B)`, `(a: B)`
This applies to Context, Implicit Types, and definitions.
**TODO**: Prefer `(a : B)` to `a : B`
- **Put a space on both sides of the colon.**
Good: `(a : B)` <br>
Bad: `(a:B)`, `(a: B)`
- **Prefer `(a : B)` to `a : B`.** (TODO)
This applies to Context, Implicit Types, and definitions
### Patterns
#### Disjunctions & branches
Always mark the disjuncts when destructuring a disjunctive pattern, even if you don't bind anything, to indicate that the proof branches
- **Always mark the disjuncts when destructuring a disjunctive pattern, even if you don't bind anything, to indicate that the proof branches.**
**Good:**
```coq
Lemma foo : ∀ b : bool, b = true ∨ b = false.
Proof.
intros [|].
...
```
Good:
```coq
Lemma foo : ∀ b : bool, b = true ∨ b = false.
Proof.
intros [|].
...
```
**Bad:**
```coq
Lemma foo : ∀ b : bool, b = true ∨ b = false.
Proof.
intros [].
...
```
Bad:
```coq
Lemma foo : ∀ b : bool, b = true ∨ b = false.
Proof.
intros [].
...
```
#### Uncategorized
**TODO:** Use `"[H1 H2]"` when possible otherwise do `"(H1 & H2 & H3)"`
- **Use `"[H1 H2]"` when possible otherwise do `"(H1 & H2 & H3)"`.** (TODO)
### Unicode
Always use Unicode variants of forall, exists, ->, <=, >=
- **Always use Unicode variants of forall, exists, ->, <=, >=.**
**Good:** `∀ ∃ → ≤ ≥`
**Bad:** `forall exists -> <= >=`
Good: `∀ ∃ → ≤ ≥`<br>
Bad: `forall exists -> <= >=`
### Equivalent vernacular commands
Use `Context`, never `Variable`
- **Use `Context`, never `Variable`.**
**TODO:** Use `Implicit Types`, never `Implicit Type`
- **Use `Implicit Types`, never `Implicit Type`.** (TODO)
Use `Lemma`, not `Theorem` (or the other variants: `Fact`, `Corollary`,
`Remark`)
- **Use `Lemma`, not `Theorem` (or the other variants: `Fact`, `Corollary`, `Remark`)**.
**TODO:** Always add `Global` or `Local` to `Hint`, `Arguments`, and `Instance`.
- **Always add `Global` or `Local` to `Hint`, `Arguments`, and `Instance`.** (TODO)
### `Require`
Never put `Require` in the middle of a file. All `Require` must be at the top.
- **Never put `Require` in the middle of a file.** All `Require` must be at the top.
If you only want to *import* a certain module in some specific place (for instance, in a `Section` or other `Module`), you can do something like:
```coq
From lib Require component.
(* ... *)
Import component.
```
```coq
From lib Require component.
(* ... *)
Import component.
```
### Ltac
We prefer `first [ t1 | fail 1 "..." ]` to `t1 || fail "..."` because the latter will fail if `t1` doesn't make progress. See https://gitlab.mpi-sws.org/iris/iris/-/issues/216. Note that `first [ t1 | fail "..."]` is simply incorrect; the failure message will never show up and will be replaced with a generic failure.
- **Prefer `first [ t1 | fail 1 "..." ]` to `t1 || fail "..."`.** This is better because the latter will fail if `t1` doesn't make progress. See https://gitlab.mpi-sws.org/iris/iris/-/issues/216. Note that `first [ t1 | fail "..."]` is simply incorrect; the failure message will never show up and will be replaced with a generic failure.
### Coqdoc comments
Module-level comments (covering the entire file) go at the top of the file, before the `Require`.
- **Module-level comments (covering the entire file) go at the top of the file, before the `Require`.**
### Uncategorized
Indent the body of a match by one space:
**Good:**
```coq
match foo with
| Some x =>
long line here using
```
*RJ*: This is odd, usually everything is in (multiples of) 2 spaces, I think.
*Tej*: https://gitlab.mpi-sws.org/iris/iris/-/blob/920bc3d97b8830139045e1780f2aff4d05b910cd/iris_heap_lang/proofmode.v#L194
Avoid using the extra square brackets around an Ltac match:
**Good:**
```coq
match goal with
| |- ?g => idtac g
```
**Bad:**
```coq
match goal with
| [ |- ?g ] => idtac g
```
Use coqdoc syntax in comments for Coq identifiers and inline code, e.g. `[cmraT]`
Put proofs either all on one line (`Proof. reflexivity. Qed.`) or split up the usual way with indentation.
**Bad:**
```coq
Lemma foo : 2 + 2 = 4 ∧ 1 + 2 = 3.
Proof. split.
- reflexivity.
- done.
Qed.
```
Put the entire theorem statement on one line or one premise per line, indented by 2 spaces.
**Bad:**
```coq
Lemma foo x y z :
x < y → y < z →
- **Indent the body of a match by one space.**
Good:
```coq
match foo with
| Some x =>
long line here using
```
*RJ*: This is odd, usually everything is in (multiples of) 2 spaces, I think.
*Tej*: https://gitlab.mpi-sws.org/iris/iris/-/blob/920bc3d97b8830139045e1780f2aff4d05b910cd/iris_heap_lang/proofmode.v#L194
- **Avoid using the extra square brackets around an Ltac match.**
Good:
```coq
match goal with
| |- ?g => idtac g
```
Bad:
```coq
match goal with
| [ |- ?g ] => idtac g
```
- **Use coqdoc syntax in comments for Coq identifiers and inline code, e.g. `[cmraT]`.**
- **Put proofs either all on one line (`Proof. reflexivity. Qed.`) or split up the usual way with indentation.**
Bad:
```coq
Lemma foo : 2 + 2 = 4 ∧ 1 + 2 = 3.
Proof. split.
- reflexivity.
- done.
Qed.
```
- **Put the entire theorem statement on one line or one premise per line, indented by 2 spaces.**
Bad:
```coq
Lemma foo x y z :
x < y → y < z →
x < z.
```
Good:
```coq
Lemma foo x y z : x < y → y < z → x < z.
```
Good: (particularly if premises are longer)
```coq
Lemma foo x y z :
x < y →
y < z →
x < z.
```
**Good:**
```
```coq
Lemma foo x y z : x < y → y < z → x < z.
```
**Good:** (particularly if premises are longer)
```coq
Lemma foo x y z :
x < y →
y < z →
x < z.
```
If the parameters before the `:` become too long, indent later lines by 4 spaces and always have a newline after `:`:
**Bad:**
```coq
Lemma foo (very_long_name : has_a_very_long_type)
(even_longer_name : has_an_even_longer_type) : x < y → y < z →
x < z.
```
**Good:**
```coq
Lemma foo (very_long_name : has_a_very_long_type)
(even_longer_name : has_an_even_longer_type) :
x < y → y < z → x < z.
```
For definitions that don't fit into one line, put `:=` before the linebreak, not after.
**Bad:**
```coq
Definition foo (arg1 arg2 arg3 : name_of_the_type)
:= the body that is very long.
```
**Good:**
```coq
Definition foo (arg1 arg2 arg3 : name_of_the_type) :=
the body that is very long.
```
For tests with output put `Check "theorem name in a string"` before it so that the output from different tests is separated.
For long `t1; t2; t3` and `t; [t1 | t2 | t3]` split them like this, and indent by 2 spaces:
**Good:**
```coq
t;
[t1
|t2
|t3].
```
```coq
t;
t1;
t2.
```
- **If the parameters before the `:` become too long, indent later lines by 4 spaces and always have a newline after `:`.**
Bad:
```coq
Lemma foo (very_long_name : has_a_very_long_type)
(even_longer_name : has_an_even_longer_type) : x < y → y < z →
x < z.
```
Good:
```coq
Lemma foo (very_long_name : has_a_very_long_type)
(even_longer_name : has_an_even_longer_type) :
x < y → y < z → x < z.
```
- **For definitions that don't fit into one line, put `:=` before the linebreak, not after.**
Bad:
```coq
Definition foo (arg1 arg2 arg3 : name_of_the_type)
:= the body that is very long.
```
Good:
```coq
Definition foo (arg1 arg2 arg3 : name_of_the_type) :=
the body that is very long.
```
- **For tests with output put `Check "theorem name in a string"` before it so that the output from different tests is separated.**
- **For long `t1; t2; t3` and `t; [t1 | t2 | t3]` split them like this, and indent by 2 spaces.**
Good:
```coq
t;
[t1
|t2
|t3].
```
```coq
t;
t1;
t2.
```
**TODO:** Keep all `Require`, `Import` and `Export` at the top of the file.
## File organization
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment