Coq Call 2019 10 16 - coq/coq GitHub Wiki

October 16th at 4pm Paris time. Add topics you would like to see discussed.

Topics:

  • Duplication of the parsing state (system and parsing in Vernacstate.t) (Maxime, if Emilio is present)
  • CEP #40: where to put the proofs? (Enrico, with Pierre-Marie, if Emilio is present)

Notes:

Emilio not present so above points postponed.

  • 8.10.1 with soundness bug of SProp to fix and notation issue
  • Discussion of #10298 and the like: not ready for 8.10.1
  • Problem of putting too much on the CI? Proposal to remove legacy contribs that are no longer maintained (e.g. fiat-crypto). Should be reconsidered at the next WG. This slows down important bugfixes: we don't have infinite ressources!