Session with the Coq Development Team
summary
Coq 8.13 appears: compile libraries with 8.13 to see new hint warnings and migrate by changing a hint’s attribute from global to export so it only activates when its module is imported; keep the global attribute temporarily to silence breaks. Notation printing uses a new most specific wins rule and prefers most recently imported notations, so display may change. Native evaluation is opt‑in via the cognative package (precompiles lambdas to native code). Kernel fixes, a primitive persistent array type, s‑prop equality irrelevance (caveat on consistency), and plans toward 8.14 (full cumulative inductives fix) are discussed; 15–20 packages were asked to tag releases for the new platform distribution.
AI-written summary · about
chapters (7)
- 0:00Start
- 4:50Upgrading to 8.13 - Notations
- 7:14The coq-native OPAM package
- 11:22The release process
- 14:42Coq 8.13 Features
- 18:04In the Pipeline for Coq 8.14
- 24:26Development news
related talks
44mSession with the Coq Development Team
42mSession with the Rocq Development Team
54m10-Year Most Influential Paper Talk: Coq: the world's best macro assembler?
42mMetaCoq as a tool to prevent future unsoundness in Coq
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
31mA Coq Library of Undecidable Problems
24mREPLica: REPL Instrumentation for Coq Analysis
15mCompiling with Continuations, Correctly