Coq Call 2020 04 01 - coq/coq GitHub Wiki

• April 1st 2020, 4pm-5pm Paris Time
• The call will be on rendez-vous: https://rendez-vous.renater.fr/coq-call
• Add your topics below

Notes

• Report on fiddling with the object file format (PMP)

  zip not cutting it: size limit on files. zip64 not a better idea. Now storing opaque files on disk and out of live memory, for a nice speedup: https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/903/console

• Upfront substitution considered harmful (PMP)

  Big speed-up in odd-order theorem by switching to delayed substitution selectively, and others as well. PR #11955 looking good, only a first step. Still need to decide about the splitting of cbn which does unfolding /reductionops PR #11922 ready as well