Refman improvements in 8.12 and beyond

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.

⚠️ 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