Session with the Coq Development Team
summary
Two releases land in 2022 and Coq 8.16 ships on Sept 5 with the matching platform arriving Oct 10, and an 8.17 release candidate (fsrc1) is out with the platform due in a month or two. Concrete changes include an improved guard check for structural recursion backed by metacoq work, fixes to a rare vm_compute inconsistency, per-notation enable/disable, non‑uniform coercions, and work to support OCaml 5. The team pushes Ltac2 growth, acknowledges performance is bottlenecked by a single expert, starts hiring and an editorial board to curate libraries, expands UI work (LSP/VSCoq) and revives certified extraction with a new postdoc.
AI-written summary · about
chapters (20)
- 0:00Welcome to the session
- 1:04Coq platform and release updates
- 3:38Coq 8.16 and 8.17 improvements
- 6:26Ltac 2 and UI streamlining
- 7:49OCaml 5 compatibility and multi-core
- 8:53Coq platform ecosystem
- 12:55Proof engine bottlenecks
- 16:06Reduction and automation performance
- 22:45Hashconsing and term sharing
- 27:05User interface API for syntax trees
- 30:20Debugging universe constraints
- 33:30Global vs local universes debate
- 35:37Trusted computing base
- 38:16Coq library ecosystem status
- 41:11Library fragmentation and redundancy
- 45:24Standard library ownership
- 47:10Community engagement and workshops
- 48:19Bringing new contributors
- 51:12In-person workshops and accessibility
- 54:01Certified extraction status
