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 (a fork of coq2html).

The generated HTML pages contain most comments and the code with proof scripts hidden by default.

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 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                                                             *)
(* ```                                                                         *)
(*   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                                                     *)
(*******************************************************************************)

• centered lists do not exist in Markdown that is why their are comprised between triple quotes
• 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

(**md ## level1sectionname *)
(**md ### level2sectionname *)

• bullets:

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