Coq Call 2021 09 15

• September 15th 2021, 4pm-5pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• https://github.com/coq/coq/pull/12425 (Emilio J. Gallego Arias)

  • caching is not satisfactory
  • we are basically testing opam install, so it is worth the current setup?
  • should we stop the workers at ci.inria.fr ?

• preliminary evaluation of coqnative (Emilio J. Gallego Arias) https://github.com/ocaml/dune/pull/4750

  • overhead not trivial
  • removal of configure flag set? [Note dune 3.0 can support that fine with vendored setup]

• internal survey on preferences for proposed Alternative names (toward drafting a "shortlist") (Théo and Matthieu).

Notes

• https://github.com/coq/coq/pull/12425

  • opam install -t would be better
  • stopping the workers at ci.inria.fr? Still using the mac os runner to sign the releases. Might be moved to a new mac os box from Yves Still using them for 8.13 and 8.14
  • bugs opened at
    • https://github.com/coq/platform/issues/130
    • https://github.com/coq/platform/issues/131
    • https://github.com/coq/coq/issues/14886

• slowdown of coqnative

  • could be avoided by going through malfunction
  • We need a more stable compiler-libs from ocaml to improve on this
  • could be a good point to have a better story for extraction avoiding a complex printing-parsing phase too...
  • current numbers https://github.com/ocaml/dune/pull/4750#issuecomment-866151524