Coq Call 2019 11 06

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.