Skip to content

How to document

affeldt-aist edited this page Jan 20, 2022 · 16 revisions

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.

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 (caveat), see the result for version 0.3.12.

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 *)
(*   blah := definition        *)
(*******************************)
  • section names can also appear within the file
(** * level1sectionname *)
(** ** level2sectionname *)
  • bullets:
(* blah
- blah1
- blah2
*)