Agenda

• News from Portland
• Installation instructions
• Status of PR #270
• Documentation for naming conventions of structures and modules (where to put caps?)
• PR #378: Reorder the arguments in compare_nat and ltngtP This is a compatibility breaking change. So we probably should have more discussion before merging.
• Release of Coq 8.10, taking advantage of new features and dropping support for old versions of Coq

Participants

Reynald Affeld, Yves Bertot, Cyril Cohen, Christian Doczkal, Georges Gonthier, Laurent Théry, Kazuhiko Sakaguchi

Minutes

• News from Portland

  No particular remarks from the people that were at Portland.

• Installation instruction

  this item is postponed to the next meeting

• Status of PR #270

  Cyril : most remarks have been addressed, Kazuhiko has done the renaming.

  Laurent : is it converging?

  Cyril : the documentation and tutorial are still mising.

  Georges : About the scope problem, it should be set to function scope

  Cyril : we hope this PR wil be merge by Nov. 5

• Documentation for naming conventions of structures and modules (where to put caps?)

  Cyril: the right place to put this is in CONTRIBUTING.md

  Reynald : I will open a PR

• PR #378: Reorder the arguments in compare_nat and ltngtP This is a compatibility breaking change. So we probably should have more discussion before merging.

  Kazuhiko: this PR breaks the 4 colour

  Georges: the solution is to use an explicit pattern in the PR of the 4 colour. Once this done, this PR can be merged.

  Kazuhiko: I will do it

• Release of Coq 8.10, taking advantage of new features and dropping support for old versions of Coq

  Cyril : I have experimented with rewrite everywhere in intro pattern.

  Georges : when assumptions are modified, they should appear explicitly in the script

  Cyril : maybe we need to restrict this new feature.

  Georges : we should provide guidance and this should be lead by example.

  Georges : Another new feature is to take advantage of custom syntax to simplify some code.

  Cyril : I will create an issue

  Yves : About multirules, why there is not mem_nil in inE`.

  Georges : this is to keep the number down

  Cyril: maybe we could compile multirules.

  Georges: this is not a priority

  Cyril: how many versions should we support?

  Georges : should move from 3 to 2 (1 year)

  Cyril : When is the next release?

  Laurent : we put it as first item of the agenda of next meeting.

  Cyril : is there some news about Georges' work on finmap.

  Georges: Not much progress since last meeting. A separate PR could be created to just remove duplicate between generic quotient and finmap. One needs a compatibility module. It is undocumented (not stable)

Next meeting November 14, 10am