Coq Call 2023 10 24

• October 24th 4pm UTC+2 (Paris time zone offset)
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• Roadmap update (Théo, 10-15 minutes)
• moving the of notation for variants from ssreflect module to Coq core syntax? (Pierre, 10 minutes)
• support for dynamically recomputed recursive structure in guard condition (the standard asymmetry between recursing on tree or on list tree, PR #17950) (Hugo, 10-30 minutes)
• followup on removing recovery mode from camlp5/coqpp (CEP #71, PRs #18014 and #17876) (Pierre, 15-20 minutes, to be postponed if doesn't fit
• organizing a physical meeting one of these days (Hugo, 5 minutes)

Roles

• Chairman: Nicolas
• Secretary: Matthieu

Notes

Summary

• Physical meeting in January or during the defense season in Nantes? To be investigated.
• Roadmap: we will be also gathering longer term / more high-level items.
• Dynamic recompilation of recursive trees to handle nested types more completely: a priori in favor. Need to discuss between Hugo and Matthieu
• Moving "of" to core, no objection a priori
• doodle for a physical meeting end of december (TODO Matthieu)

More details about some points

Roadmap update (Theo Zimmermann)

There is some progress with the roadmap. The design of the roadmap has changed with a first short-time roadmap with immediate resources. There is more work to do on the long-term roadmap. We need to make explicit how the short-time items are linked to the long-term goals. Examples: universe polymorphism and SProp.

Ltac2 should belong to a mid-term item in the roadmap. Things which are not really detailed should be moved to mid-term (for example Sections).

Emilio thinks the long-term roadmap is really needed to increase collaborative efforts with a higher level vision.

For the moment, Theo proposes to focus on the short-term part and at least write a draft of a mid-term roadmap.

Emilio asks if the roadmap should be organized by topics instead. Emilio thinks that there could be coordinators by topic.

Parsing recovery mode

Pierre Roux discusses the progress on how to get rid of the parsing recovery mode. Hugo made a first PR (17876). Pierre needs some help to fix some parts, in particular with Ltac2. He mentions that mathcomp has been hard to patch. Hugo Herbelin proposes to help. Nicolas Tabareau proposes to help with Ltac2. Gaëtan asks if it could be possible to emit a warning when the recovery mode is used. There is consensus on it. Hugo proposes to look at it. The warning should then be documented so the user knows what she is warned about. Should it appear in the roadmap? Theo says there could be a section "things we want to remove" in the roadmap.

Discussion about nested inductive types

Hugo : Discussion about mutual and nested inductives.

Extension of ssreflect's "of" syntax

Pierre Roux : ssreflect has a notation 'of', should it be added in general to Vanilla? Then "of" would become a keyword. There is some overlap with "`{}". No objection, Pierre Roux will keep working on it.

Organization of an offline meeting between developers

Hugo thinks an offline meeting would be welcome. There were Coq working groups before the covid pandemic. Emilio thinks that there should be more meetings of Coq developpers. Theo warns that this could cut the usual developpers from the rest of the contributors. That is why most things need to be written instead of only be shared orally between a few core developers. Nicolas says there will be some phd defenses in december at Nantes just before holidays. Matthieu will launch a doodle.