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
  • it may be better to put the date and the name of the author together with a TODO or an NB
• Local lemmas appear as blank lines
• comments are expected to be 80 characters wide
• typical header:

(****************************************)
(*           centeredtitle              *)
(*                                      *)
(* some introductory text               *)
(*                                      *)
(* Reference: bib entry if any          *)
(*                                      *)
(* * sectionname:                       *)
(*   definition == explanation          *)
(*     notation == explanation          *)
(*                 The HB class is XYZ. *)
(*         blah := for shortcuts        *)
(*                                      *)
(* Acknowledgments: people              *)
(****************************************)

• section names can also appear within the file

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

• bullets:

(* blah
- blah1
- blah2
*)