Coq Call 2020 03 04

• March 4th 2020, 4pm-5pm Paris Time
• How to join the call
• Add your topics below

Topics

• vo as zip file (PMP tried but I'd love a summary, gares)

• https://github.com/coq/coq/pull/7825 (Matthieu) What are we doing with shelved goals, interp_open_constr, refine and the ';' vs '.' discrepancy?

• First steps toward refactoring the refman (cf. CEP #43)

Notes

Pierre-Marie: Trying to zip .vo files.

• Very slight overhead w/o compression About 15% overhead with compression. Not clear if uncompression is the main culprit. Camlzip is not ideal (API mismatch) Option to do hashconsing or not: not much change. We need to use the disk writes for decompression due to a limitation of ocaml ?! Maybe ask Xavier about this, are there other options?

  Without hashconsing the perf is ok.

  Best solution right now: use camlzip without compression, just for the content addressing part (and less auxiliary files visible).

  We seem to all agree on that plan, let's notify Xavier.

• 7825: big issue with shelving information being duplicated and somewhat ill-scoped. PMP agrees we should have all information in a single place. We should synchronize the proofview shelve information with the sigma.

• Coq Refman: proceed with the refactoring

• Next working group: wait a bit until we know about travel restrictions

• CUDW: Nantes or the Croisic (but we're a bit late)

• Maxime mentions stdlib2 porting issues:

  • Problem of scripts relying on generated names: Hugo suggests warning strategy for intros to port scripts, suggested by Jason.
  • Few issues porting tactics w.r.t universes and primitive projections