search

coq / platform-docs

A project of short tutorials and how-to guides for Coq features and Coq Platform packages.
https://coq.inria.fr/platform-docs/
Other
19 stars 10 forks source link

The table of content should be an output, not an input #10

Open Villetaneuse opened 5 months ago

Villetaneuse commented 5 months ago

We should only give (unnumbered) titles, subtitles, etc and, if need be, the numbering and the table of content should be automatically written by some tool.

I can write some crude sh/awk/sed helpers, but maybe the format should stabilize before.

thomas-lamiaux commented 5 months ago

I agree. We are most likely to keep with coqdoc for a while, so it might be worth it doing something now. For the numbering, ideally it should up to the writer like in latex. For the moment, in coqdoc, we can ask the user to write it themselves in section titles. @Zimmi48 ?

Zimmi48 commented 5 months ago

Well, if it doesn't take too long to write, why not?

But indeed, when we switch formats later on, it probably won't be useful anymore.