Coq Call 2019 12 11

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

Topics

• no meeting next week, we will have Coq working group instead.

• vos and vio coexistence: https://github.com/coq/coq/issues/11195 (Arthur and Gaëtan)

• documentation for coq-vscode: is there one? plans for one? (Arthur suggested key bindings)

• how to organize the schedule of online meetings (for those who are only concerned by one or two points)

  people can add their constraints, should be up to the person responsible for the schedule

• rewriter-perf on pendulum (Maxime)

  • what should be done about it?
  • how come a 12h test reached this infrastructure, and was activated by default?

  we will remove it from the defaults; also we will open a ticket to investigate Jenkins upgrades and configuration tweaks.

• A few stuck PRs:

  PRs needed to support 4.10 => discussion at WG

  • https://github.com/coq/coq/pull/10582 (Show clear warning for experimental features)

  Just needs some time to be solved.

  • https://github.com/coq/coq/pull/10469 (Rename Int and Option modules)

  No real need, other than inconvenience, closing.

  • https://github.com/coq/coq/pull/10266 (Separate "named" objects from anonymous ones)

  It seems nametab registration and libobject should not be tied, we recommend closing in favor of a different approach.

• Towards an improved quoting mech (Emilio , c.f. https://github.com/coq/coq/pull/10667)

  Isabelle has a very powerful quoting mech [it can for example add ml:(...) stuff in the middle of tactics; Emilio would like to extend the quoting mech for Coq; this may be related with the open pretyper. We discussed a bit, for next WG [not the one in December] we will try discuss more.