Restructuring the reference manual. #43
Conversation
|
Can you say a bit more about |
|
Thanks for asking. First, just to be clear, the detailed outline of each chapter is something that will have to be proposed and debated in specific PRs on the Coq repo. But to still answer your question, what I have in mind as of today is the following. I think we may want to keep the proof handling chapter as a first section (on its own page) that provides a good introduction (it is not too long today, but maybe it could still be improved a bit), then I mostly intend to split out different sections of the Tactics chapter into multiple pages (cf. a few ideas that I proposed in coq/coq#8946) and to kill the "Detailed example of tactics" chapter which makes no sense today. Regarding SSReflect, I do not intend any change for now (except maybe a pass to check the grammar), so this would mean that it would still be presented on a single page, which would be one of the top-level sections of the "Writing proofs" chapter (much like the proof handling one). Longer term it would be great to at least take out the non-proof parts of SSReflect:
And possibly to try to provide more symmetry between the way that vanilla and SSReflect tactics are presented, possibly with lots of cross-references between the two, or even by having sections by type of tactics divided in sub-sections presenting the vanilla version and the SSReflect one. |
|
The I'm OK with the plan. My point is that SSR is a language, with a style, idioms, etc, not a list of tactics and tactic combinators that can be presented in any order, or grouped by domain. Hence I'd like its description to stay in a single place. Search and Gallina extensions can of course be moved elsewhere. |
As a first step toward a deeper refactoring of the reference manual, we move existing chapters into a new structure. We use the Sphinx support for top-level chapters spanning multiple pages to consolidate existing chapters into a smaller number of chapters and a smaller number of parts. Now the full top-level table of content can be seen in one glance. Most of the new chapters are divided into several sub-chapters (on separate pages) that correspond to the pre-existing chapters. These new top-level chapters gathering several chapters together have gained a new introduction. The main introduction has been rewritten / simplified as well. For now, the URL of pre-existing chapters does not change. The intent is to further refactor the manual by splitting some of these sub-chapters into smaller ones, and by moving things around. While the sub-chapters are likely to evolve very much in the future, the top-level table of content is almost final (except that the "Using Coq" part may gain one or two additional chapters on proof engineering / project management). Thanks to Jim Fehrle for investigating how to split a chapter on multiple pages and to both Jim and Matthieu Sozeau for the discussion that led to this new structure. See also the related CEP: coq/ceps#43 Additional notes: - A new directory structure has been created reflecting the new chapter structure. - The indexes chapter has been removed from the PDF version since it wasn't working. Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
As a first step toward a deeper refactoring of the reference manual, we move existing chapters into a new structure. We use the Sphinx support for top-level chapters spanning multiple pages to consolidate existing chapters into a smaller number of chapters and a smaller number of parts. Now the full top-level table of content can be seen in one glance. Most of the new chapters are divided into several sub-chapters (on separate pages) that correspond to the pre-existing chapters. These new top-level chapters gathering several chapters together have gained a new introduction. The main introduction has been rewritten / simplified as well. For now, the URL of pre-existing chapters does not change. The intent is to further refactor the manual by splitting some of these sub-chapters into smaller ones, and by moving things around. While the sub-chapters are likely to evolve very much in the future, the top-level table of content is almost final (except that the "Using Coq" part may gain one or two additional chapters on proof engineering / project management). Thanks to Jim Fehrle for investigating how to split a chapter on multiple pages and to both Jim and Matthieu Sozeau for the discussion that led to this new structure. See also the related CEP: coq/ceps#43 Additional notes: - A new directory structure has been created reflecting the new chapter structure. - The indexes chapter has been removed from the PDF version since it wasn't working. Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net> Co-authored-by: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Zimmi48
force-pushed
the
refactor-refman
branch
from
3b1c753
to
73b6b55
Compare
|
The proposal if ambitious and very relevant! With all my support. |
|
The plan described by this CEP is not yet complete (Tactics and Vernacular chapters still remaining to be split, lots of new sections could be improved) but I don't think the plan is going to change now (discussions happen in corresponding PRs), so I propose to merge this CEP to avoid keeping a long list of open CEPs in various states. |
This CEP comes quite late as work in already ongoing with coq/coq#11601 et al., but better late than never.
Rendered