Coq Call 2019 11 06 - coq/coq GitHub Wiki
November 6th at 4pm Paris time. Add topics you would like to see discussed.
Topics
- plan for https://github.com/coq/coq/issues/11039 ("new" proof of false)
- need for CI testing the output of Coq, eg
Show
(cfr https://github.com/coq/coq/pull/11053). In particular:- where to store the reference output (for stdlib but also for other CI projects)
- how to update the reference output (when the CI project gets updated or the printer changed)
- can we hack
Proof
to log on disk? Would this provide sufficient coverate (and be fast enough)?
- 8.11 release summary
- PR https://github.com/coq/coq/pull/11010
Notes:
-
https://github.com/coq/coq/issues/11039 2 steps:
- Emergency fix: forbid template polymorphic universes to even appear in the constructors or constraints. Morally, the universe would be irrelevant if the inductive was seen as a Polymorphic Cumulative Inductive. Remaining question: Is Prop instantiation really ok?
- For 8.12: remove template poly and switch key container inductives to polymorphic cumulative (Nicolas has a branch doing that partially already, ref https://github.com/CoqHott/coq/tree/remove_template_polymorphism
-
Devs in CI should have tests for notations/output: probably in a file doing About on some representative theorems / Show in proofs. Maybe instrumentation of coq_makefile to handle these tests could help.
-
8.11 going smoothly apart for the lovely soundness bug above. Some steps of release plan are unclear and need to be documented
-
Guillaume mentionned https://github.com/coq/coq/issues/11057 which is blocking, we're asking Arthur and Emilio will finish and review and provide patches to allow opt-in into vos.
-
PR https://github.com/coq/coq/pull/11010: do all branches at once or none. The only disadvantage we see is when using blame on github. But we AGREED TO DO IT! Bye bye tabs.