How to document

Tentative summary of the math-comp/coqdoc documentation format

The purpose of this wiki entry is to summarize how to document Coq scripts so they render ok with the math-comp/coqdoc tool (at some point, this wiki entry should make its way to math-comp).

math-comp provides a script that does in particular some sed processing before calling coqdoc that gives result like this this one.

The mathcomp scripts can be used with mathcomp-analysis (modulo a bug as of 2022-01-20), see the result for version 0.3.13.

Hints:

• the generated html pages contains:
  • most comments
  • the code without the proofs (not the Local lemmas)
• we may want to indicate clearly when a comment is a todo (TODO:) or a memo (NB:) (though todos shoud better be issues)
• Local lemmas appear as blank lines
• comments are expected to be 80 characters wide in general
• typical header:

(*********************************)
(*        centeredtitle          *)
(*                               *)
(* some introductory text        *)
(*                               *)
(* * sectionname:                *)
(*   definition == explanation   *)
(*     notation == explanation   *)
(*         blah := for shortcuts *)
(*********************************)

• section names can also appear within the file

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

• bullets:

(* blah
- blah1
- blah2
*)