Session with the Coq Development Team
summary
Coq 8.14 and 8.15 introduce a new case representation change that fixes surprising match-occurrence bugs and a Metacoq-checked subject reduction proof; native compilation now supports separate native binaries and CoqMake handling; typeclass resolution gains mode-aware backtracking and clearer errors; Ltac2 gets inductive-manipulation and printf-like APIs; a signed primitive-integers library lands; apply with explicit binders stops alpha-renaming; hint/unfold and discrimination-nets get fixes; the Coq Platform binaries provide synchronized, tested package sets and installers; CI now uses an automated bug-minimizer and Docker images.
AI-written summary · about
chapters (5)
- 0:00Start
- 21:32For users who don't want to use new extensions like inductive-inductive types, can we turn them off globally to avoid TCB growth?
- 23:19Question Is the Coq Platform now the preferred way for non- experts to install Coq? In particular, should Software Foundations recommend it?
- 24:41What is the current set of "non experimental" / supported front ends?
- 34:41Is there any work on improving teh performance predicatability of rewriting?
related talks
46mSession with the Coq Development Team
44mSession with the Coq Development Team
42mMetaCoq as a tool to prevent future unsoundness in Coq
42mSession with the Rocq Development Team
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
19mExtensible Metatheory Mechanization via Family Polymorphism
31mA Coq Library of Undecidable Problems
54m10-Year Most Influential Paper Talk: Coq: the world's best macro assembler?