Stream: Coq users

Topic: coqdoc "table of contents"

Armaël Guéneau (Mar 02 2021 at 14:07):

Is there a way of customizing the output of coqdoc's table of contents? (emitted when passing --toc)
For instance re-ordering the files, and indicating a title for each. I would like to have it as the entrypoint to the docs, but it's a bit dry as is.

Paolo Giarrusso (Mar 02 2021 at 19:30):

IIRC the file order comes from _CoqProject/the argument order.

Paolo Giarrusso (Mar 02 2021 at 19:31):

On customizing the toc otherwise, http://adam.chlipala.net/cpdt/html/toc.html seems tolerable

Paolo Giarrusso (Mar 02 2021 at 19:31):

(but others might have better answers!)

Paolo Giarrusso (Mar 02 2021 at 19:32):

Coqrst/alectryon are better in many other ways, but today they're not made to replace coqdoc

Armaël Guéneau (Mar 03 2021 at 08:33):

Cpdt's TOC just looks like it's hand written, right? That would be an option indeed.

Armaël Guéneau (Mar 03 2021 at 08:34):

I hadn't realized that the order came from _CoqProject, that's helpful already, thanks

Christian Doczkal (Mar 03 2021 at 10:54):

For what it's worth, I'd use --toc together with --short to suppress the "Library" headers. Then one can use document comments such as (** * H1 *) and (** ** H2 *) to obtain a hierarchical ToC. This is for instance what I do here: https://coq-community.org/reglang/docs/latest/coqdoc/toc.html. (I also use CoqDocJS to obtain nicely hyperlinked documentation with foldable proofs, but that's orthogonal.)

Christian Doczkal (Mar 03 2021 at 10:57):

Armaël Guéneau said:

I hadn't realized that the order came from _CoqProject, that's helpful already, thanks

The order in the ToC has been dependent on the order in the _CoqProject file for a long time, but in 8.4 (or something similar) it used to be the reverse of the order in that file. Imagine my surprise when I had totally garbled ToCs after an update to Coq. :grinning:

Armaël Guéneau (Mar 03 2021 at 11:45):

Ah, those title documentation comments look exactly like what I was looking for.

Armaël Guéneau (Mar 03 2021 at 11:45):

(but too lazy to make changes 10 min before the deadline now.. :p)

Last updated: Oct 13 2024 at 01:02 UTC