Prose syntax
Documentation lives in the .v file, in comments. This page quotes Prose.v and shows, under each quote, the HTML that the plugin's own renderer produced from it during this build.
The same file as a page shows the comments in place.
The three comment forms
| Opening | Format | Becomes |
|---|---|---|
| Two stars | Doc | Prose with headings, paragraphs and code spans |
Two stars and md |
Markdown | Prose with everything Markdown offers |
| One star | Plain | Prose that reads like a doc comment, or code when it sits inside a sentence |
Doc comments
Headings
One to four stars open a heading:
(** * A doc comment heading
One to four stars open a heading in a doc comment. *)
A doc comment heading
One to four stars open a heading in a doc comment.
(** ** A second-level heading *)
A second-level heading
Paragraphs and code
Lines join into a paragraph. Square brackets mark code, and a name that resolves becomes a link with a hover card:
(** A paragraph in a doc comment.
Lines join into one paragraph, and a blank line starts the next.
Square brackets mark code: [total] links to its declaration, and [1 + 1] stays plain code. *)
A paragraph in a doc comment. Lines join into one paragraph, and a blank line starts the next.
Square brackets mark code: total links to its declaration, and 1 + 1 stays plain code.
No lists
A doc comment has headings, paragraphs and code spans, and nothing else. A leading dash stays text:
(** - This dash is plain text, since doc comments have no lists: only headings, paragraphs and
[code]. Use a Markdown comment for lists. *)
- This dash is plain text, since doc comments have no lists: only headings, paragraphs and
code. Use a Markdown comment for lists.
Markdown comments
Headings
One to six # marks open a heading:
(**md ## A Markdown heading
The `md` marker after the opening stars selects Markdown, with one to six `#` marks for a heading. *)
A Markdown heading
The md marker after the opening stars selects Markdown, with one to six # marks for a heading.
Everything else
Markdown comments use CommonMark. Backticks mark code, and a name that resolves becomes a link, as with square brackets in a doc comment:
(**md **Bold**, *emphasis*, `total` as a linked name and `1 + 1` as plain code.
- A list item
- Another, with a [link to a declaration](Core.html#append)
| Form | Marker | Lists |
|---|---|---|
| Doc | none | no |
| Markdown | `md` | yes |
```text
A fenced block. `total` stays text here.
```
An external [link](https://rocq-prover.org), and raw HTML shown as text: <b>not bold</b>. *)
Bold, emphasis, total as a linked name and 1 + 1 as plain code.
- A list item
- Another, with a link to a declaration
| Form | Marker | Lists |
|---|---|---|
| Doc | none | no |
| Markdown | md |
yes |
A fenced block. `total` stays text here.
An external link, and raw HTML shown as text: <b>not bold</b>.
Pipe tables render too, as in that comment. Other Markdig extensions can be added to the site's options:
|> Rocq.extensions [ Markdig.Extensions.EmphasisExtras.EmphasisExtraExtension Markdig.Extensions.EmphasisExtras.EmphasisExtraOptions.Strikethrough ]
Three rules hold for every comment:
- Raw HTML appears as text.
- A link with a scheme other than
http,httpsormailtoloses its link, and keeps its text. - A fenced block holds text only, so names inside it stay unlinked.
Extensions cannot enable raw HTML.
Links and names
| You write | It links to |
|---|---|
[total] or a backticked total |
The declaration, when the name matches one symbol, or one in the same file |
[text](Core.html#append) |
The declaration on that module's page. Core can be the full module name, or a dotted suffix naming one module |
[text](https://example.com) |
That address |
A name matching several symbols in other files stays plain code.
Arguments
One - [name:] text line documents an argument of the declaration below. Lines indented past the dash continue the entry. It works in both prose forms:
(** Arguments in a doc comment.
- [n:] the count added, whose entry
continues on an indented line.
- [t:] the tally extended, mentioning [size]. *)
Arguments in a doc comment.
n- the count added, whose entry continues on an indented line.
t- the tally extended, mentioning
size.
(**md Arguments in a Markdown comment.
- [t:] the tally read, mentioning `append`. *)
Arguments in a Markdown comment.
t- the tally read, mentioning
append.
The entries leave the comment's text, and appear in an Arguments list by the code and on the binder's hover card, with its type. Here is the first of those declarations on its real page:
An entry naming no binder of the statement still appears, and raises the build warning rocq/argument-unmatched, which fails a --strict build.
Readers choose how arguments appear in Settings.
Attached and free comments
A comment in any form documents the declaration directly below it. A blank line between them breaks the link, and the comment reads as prose between declarations:
(** A comment that has a line of its own, and is attached to no declaration, reads as prose between
the declarations. *)
A comment that has a line of its own, and is attached to no declaration, reads as prose between the declarations.
A comment inside a sentence stays in the code. A comment on the same line as the end of a sentence documents nothing below it. This declaration has both a plain comment above it, which appears as documentation, and one inside its statement, which stays where it is:
Definition with_plain_comment (* a comment inside the statement *) := 0.
Titles for the Guarantees page
A Markdown comment on a Theorem or Corollary whose first line is wholly in bold gives the theorem a title, and puts it on the Guarantees page:
(**md
**A first line wholly in bold titles a theorem.**
A `Theorem` or `Corollary` with this form appears on the Guarantees page under that title. A `Lemma`
never does.
*)
A first line wholly in bold titles a theorem.
A Theorem or Corollary with this form appears on the Guarantees page under that title. A Lemma
never does.
What the library sees
The same comments are data. Comment.Format, Comment.AttachedTo and Model.Headings come from the library.