Coq Call 2019 09 25 - coq/coq GitHub Wiki

• 8.10 and Arthur's bug (@mattam82)

  • ask Nicolas Tabareau about trying with univalence for free to see if notypeclasses refine's new semantics is worth it.

• Depreciation of local hints added into core (#10559) Does NOT mean that core is deprecated (yet) Backward compatible fix is to add : core.

• Quick update on MetaCoq (@mattam82)

• 8.11 release management: setting the dates (@ppedrot and @mattam82) Stick to 6 month, and be careful about communication.

• VSCoq beta testing, when is it ready to advertise / work with at scale?

  • release will happen this week (one click install)

• vos/voi/vok: what's the status?

  • discussed last week https://github.com/coq/coq/wiki/Coq-Call-20190918
  • some complex rebasings to do but should happen soon (@maximedenes is on it)

Be careful about the dune / Make blockers (test-suite and native files), (coqchk?) Plan B would be to use make only for the test-suite

• Review/update of the Nantes WG schedule

  • Tuesday afternoon:

    Morning talk by Damiano Mazza. Hugo won't be there.

    • SProp + UIP with ppedrot and skyskimmer
    • PR reviewing and discussion time?

  • Wednesday:

    • Multiverses / handling sorts (Gaëtan, PMP, Matthieu, Hugo)
    • Reals (Vincent Semeriva, Cyril and Kazuhiko remotely, maybe Bas remotely)
    • CI (what do we test? Allowed failures? Enrico) Do we have the right tools?
    • Ltac2 ? Binding ? (Hugo and PMP)
    • CoqMT reloaded (Maxime, Matthieu, Nicolas, Bas?, P-Y will be there in Nantes)

  Alexis Saurin will be there