-
Notifications
You must be signed in to change notification settings - Fork 43
How to document
affeldt-aist edited this page Mar 31, 2024
·
16 revisions
MathComp-Analysis follows the documentation format of MathComp with minor modifications to accommodate (a fork of) coq2html
(instead of the MathComp documentation tool based on coqdoc
).
The purpose of this wiki entry is to summarize how to document MathComp-Analysis scripts so that:
- they are useful, and
- they render ok with
coq2html
.
The generated HTML pages contain most comments and the code with proof scripts hidden by default but that can be revealed by clicking Proof.
.
Basic rules for comments in scripts:
- comments are expected to be 80 characters wide
- definitions and notations should be documented in the header
- mathematical structures are expected to come first
- unless there is a good reason, HB mixins and factories are presented as "interfaces"
- it is ok to reduce the amount of documentation by assuming that the user will use
HB.about
andHB.howto
- notations should appear soon after the definitions
- lemmas are not documented by default because it is too difficult to do so while keeping the documentation readable; there are some exceptions for some particularly important theorems
- mathematical structures are expected to come first
- only sentences are expected to end with a "."
- typical header (in Markdown):
(**md***************************************************************************)
(* # Title *)
(* *)
(* Some introductory text: what is this file about, instructions to use this *)
(* file, etc. Possibly using LaTeX formulas in between $'s. *)
(* *)
(* Reference: bib entry if any *)
(* *)
(* ## Section Name *)
(* ``` *)
(* structType == name of structures should make clear the corresponding *)
(* HB structure with the following sentence: *)
(* "The HB class is Xyz." *)
(* definition == prose explanation of the definition and its parameters *)
(* notation == prose explanation, scope information should appear nearby *)
(* shortcut := a shortcut can be explained with (pseudo-)code instead of *)
(* prose *)
(* ``` *)
(* *)
(* Acknowledgments: people *)
(*******************************************************************************)
- centered lists do not exist in Markdown, that is why their are comprised between triple quotes; this imposes to stick to verbatim inside centered lists
- it is however possible to format centered lists using Markdown tables (there is an example in
classical_sets.v
) so as to use, say, LaTeX notations inside
- it is however possible to format centered lists using Markdown tables (there is an example in
- we may indicate clearly when a comment is a todo (
TODO
:) or a memo (NB:
)- however, TODOs should better be github issues
- it is better to put the date and the name of the author with a TODO or an NB
- Markdown is expected to be privileged over
coqdoc
markup language, in particular:- section names can also appear within the file:
(**md ## level1sectionname *)
,(**md ### level2sectionname *)
, etc. - bullets:
- section names can also appear within the file:
(**md list of blahs
- blah 1
- blah 2
*)