How to document

Tentative summary of the MathComp-Analysis documentation format

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 and HB.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.
• 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
• 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 *)

• bullets:

(**md list of blahs
- blah 1
- blah 2
*)