Coq Call 20192509
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
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
Morning talk by Damiano Mazza. Hugo won't be there.
- SProp + UIP with ppedrot and skyskimmer
- PR reviewing and discussion time?
- 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