How to document

Tentative summary of the MathComp-Analysis documentation format

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 the MathComp documentation tool based on coqdoc.

(At some point, this wiki entry should make its way to the MathComp wiki.) (NB: CONTRIBUTING.md also contains some (redundant) information about commenting.)

Indeed, MathComp provides a script that does in particular some sed processing before calling coqdoc that gives result like [this one](https://math-comp.github.io/htmldoc_1_14_0/mathcomp.ssreflect.seq.html. The MathComp scripts can be used with MathComp-Analysis, see the result for version 0.3.13.

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
• 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
*)