Tentative summary of the MathComp documentation format

The purpose of this wiki entry is to summarize how to document MathComp scripts so that:

• they are useful, and
• they render ok with the MathComp documentation tool based on coqdoc.

The generated HTML pages contain most comments and the code without the proofs (and no Local lemmas which appear as blank lines).

Basic rules for comments in scripts:

• comments are expected to be 80 characters wide
• definitions and notations should be documented in the header
  • notations should appear soon after the definitions
  • lemmas are not documented by default because we don't want to discourage users from actually reading the documentation. There are some exceptions for some particularly important theorems.
• only sentences are expected to end with a "."
• typical header:

(*****************************************************************************)
(*                             Centered Title                                *)
(*                                                                           *)
(* Some introductory text: what is this file about, instructions to use this *)
(* file, etc.                                                                *)
(*                                                                           *)
(* Reference: bib entry if any                                               *)
(*                                                                           *)
(* * Section Name                                                            *)
(*   definition == prose explanation of the definition and its parameters    *)
(*     notation == prose explanation, scope information should appear nearby *)
(*   structType == name of structures should make clear the corresponding    *)
(*                 HB structure with the following sentence:                 *) 
(*                 "The HB class is Xyz."                                    *)
(*     shortcut := a shortcut can be explained with (pseudo-)code instead of *)
(*                 prose                                                     *)
(*                                                                           *)
(* Acknowledgments: people                                                   *)
(*****************************************************************************)

• 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
• section names can also appear within the file

(** * level1sectionname *)
(** ** level2sectionname *)

• bullets:

(* blah
- blah1
- blah2
*)