Refman improvements in 8.12 and beyond - coq/coq GitHub Wiki
Coq 8.12 includes major improvements to the reference manual: in particular, the documented syntax has been fixed in a large part of the manual and the manual has been given a new and more logical organization. These improvements to the reference manual are the start of a major effort to improve Coq documentation. We believe the documentation needs considerable work to better serve the needs of the Coq community. CEP#43 explains the need and plans in more detail. This recent Coq WG talk gives background on the changes to the manual since 2018 and the plans for the future.
The 8.12 manual is available at: https://coq.github.io/doc/v8.12/refman/
There's still a lot that can be done to improve the new manual in 8.12.0 (which is scheduled for July) and beyond. We are looking for volunteers to help refine, revise or add new material (such as better explanations and more examples) to the new pages.
What has already been done in Coq 8.12+beta1?
- The introduction has been rewritten (feedback is welcome)
- The previous organization, with a long list of top-level chapters, has given way to a new one, where the manual is organized in three main parts plus an appendix, which are divided in a total of nine top-level chapters, which themselves are divided into multiple pages.
- The documented syntax has been fixed in most of the first two chapters (except the "Polymorphic Universes", "SProp", "Implicit Coercions", "Typeclasses" and "Program" pages).
- The page documenting Ltac has been enhanced with new explanations and examples and the documented syntax has been fixed (feedback welcome).
What can still be improved in Coq 8.12.0 and further releases? (we need you!)
Many new pages have been created by splitting up and reorganizing material from various places in the 8.11 documentation. These pages often need:
- a better introduction,
- better explanations,
- more examples,
- and sometimes even different structures.
:warning: How can I help?
The tables below list the new pages with a short summary of their status.
Choose a page where there's no volunteer yet, add your name, an expected delivery date (non-binding of course, but it helps us keep track of what's in progress and what becomes delayed), create an issue and add a link to it in the table.
If there's already a volunteer but you want to help, go to the issue and offer your help.
If you need help or advice, you can ping @Zimmi48 or @jfehrle in your issue or start a chat on Zulip.
If you need help from an expert, ping @Zimmi48, who will try to point you to the right person. Experts can volunteer by going to the dedicated issue and offering their help or by adding @GitHub_nickname (expert) to the volunteer column if there is no issue yet.
If you need help with finding the right English formulation, ping @jfehrle.
What's left for Coq 8.13?
We plan to:
- Revise the "PROOFS" section for Coq 8.13. In particular, we'll split the very long page on tactics into multiple and more focused pages (@Zimmi48),
- Split the Vernacular page and distribute its content throughout the manual, in particular into the "USING COQ" section (@Zimmi48),
- Finish updating the syntax in the documentation (@jfehrle) and
- Make further improvements in the text.
Help is welcome for adding new chapters or sections to the "USING COQ" section, for instance on "Reviewing a Coq formalization" or on "Proof engineering" topics such as maintenance and tests.
List of new pages
Chapter Core language
| New page | Source of the material | Current state | Volunteers | Expected delivery date | Issue |
|---|---|---|---|---|---|
| Basic notions and conventions | Gallina + Vernacular chapters + new material | Already reviewed, in good shape | N/A | N/A | N/A |
| Sorts | Gallina chapter (syntax) + CIC chapter | Acceptable, could be revised together with page on universes | |||
| Functions and assumptions | several sections of the Gallina chapter | Needs an introduction, possibly fewer sections, glossary definitions, examples | |||
| Definitions | several sections of the Gallina chapter | Needs an introduction, more explanations and examples | |||
| Conversion rules | CIC chapter | Needs a better introduction and some concrete examples, could get new material describing the various reduction machines | |||
| Typing rules | CIC chapter | Needs new introduction, section on terms could be reduced, examples wouldn't hurt | |||
Variants and the match construct |
several sections of the Gallina chapter | Needs an introduction, rewritten explanations and examples | |||
| Record types | Gallina extensions chapter | Needs proofreading and partial rewrite | |||
| Inductive types and recursive functions | several sections of Gallina + CIC chapters | Needs an introduction, proofreading, deciding where the template polymorphism description should go (coordination with section on universe polymorphism) | |||
| Co-inductive types and co-recursive functions | several sections of the Gallina chapter | Needs a rewrite to emphasize the negative vs positive presentations and the limitations of the latter | |||
| Section mechanism | Gallina extensions chapter | Acceptable but proposal for improvements are welcome | |||
| The Module System | Module chapter + several sections of Gallina extensions | Needs complete proofreading, more explanations about Inline, possibly more examples |
|||
| Primitive objects | Gallina extensions chapter | Could deserve an introduction |
Chapter Language extensions
| New page | Source of the material | Current state | Volunteers | Expected delivery date | Issue |
|---|---|---|---|---|---|
| Existential variables | Gallina extensions chapter | Needs fewer sections, could get more working knowledge and a connection with the documentation of patterns | |||
| Implicit arguments | Gallina extensions chapter | Needs fewer sections, more examples, glossary definitions | |||
| Extended pattern matching | Extended pattern matching + Gallina extensions chapters | Needs proofreading and possibly restructuring with fewer sections | |||
| Setting properties of a function's arguments | Gallina extensions chapter and pieces from other sources | Needs an introduction and more explanations | |||
| Canonical Structures | Canonical structures + Gallina extensions chapter | Needs proofreading and possibly restructuring |
Chapter Libraries and plugins
| New page | Source of the material | Current state | Volunteers | Expected delivery date | Issue |
|---|---|---|---|---|---|
| Functional induction | Gallina extensions + tactics + schemes chapters | Needs an introduction and proofreading | |||
| Writing Coq libraries and plugins | Gallina chapter | Could get more material moved here and new material |
Chapter Command-line and graphical tools
| New page | Source of the material | Current state | Volunteers | Expected delivery date | Issue |
|---|---|---|---|---|---|
| Documenting Coq files with coqdoc | Utilities chapter | In good shape, could use some proofreading |