CRGTCoq20120119

Participants: Jean-Marc Notin, Pierre Boutillier, Bruno Barras, Cyril Cohen, Pierre Courtieu, Hugo Herbelin, Pierre Letouzey, Assia Mahboubi, Guillaume Melquiond, Arnaud Spiwack, Pierre-Yves Strub, Enrico Tassi

Jean-Marc Notin: A new infrastructure for Coq user contributions

Warning: the following only describe a small part of the discussion

Jean-Marc proposes an architecture where each contrib is made of:

• "description"
• "sources" avec scripts pour http, svn, git
• Coq dev provided "patches"
• "versions"

together with a recommendation to authors to set branches for each Coq version 8.3, 8.4, trunk

Pierre C: Question of dependence of a contrib in another one: what to do if living contrib A is updated and breaks the compilation of contrib B which depends on it: who is responsible

Note: 143 contribs (over 154) compiled in less than 10mns

Question: continuous checks rather than fixed hour checks

Several kinds of contribs e.g.:

• RSA: only local
• CoLoR: developed upstream

Two configurations:

• upstream publishes for a stable version
  • one downloads the last upstream version for stable version 8.x for each V in 8.x, 8.3, 8.4, trunk one applies our 8.x-to-V patches;
  • patching might fail or succeed, compilation can then fail or succeed
• upstream follows Coq trunk

Developers will have to prepare guidelines for library contributors.

The discussion ended without clear conclusion.

Pierre Boutillier: parsing "match" patterns like terms are parsed

Pierre proposes to parse "match" patterns using the same syntax as for terms, i.e.

• add _ for non-implicit parameters
• don't write implicit arguments (even if non parameters)
• use @ if implicit arguments need to be given.

Advantages: more symmetry and uniformity

Disadvantages: virtually more _ to write when parameters are not implicit and @ when arguments are implicit

Various opinions:

• Arnaud is clearly favorable because of the added pattern/term symmetry
• Guillaume and Hugo are afraid of having to write more _ or @

General approval and commit done. Option "Patterns Compatibility" governs the compatibility.

Discussion about 8.4

Features removed in 8.4:

• Tactic "info": consensus on saying it is useful for auto, intuition, ltac code, ... [implemented early April by Pierre Letouzey]
• "Show Script": marginal usage, mainly by people using coqtop w/o any other interface [implemented in March by Pierre Letouzey]

Ongoing works:

• Arnaud to-do's list:
  • Unfocused as a replacement of Unfocus (cf aussi message d'erreur) [done end of March]
  • Documentation
• Pierre L.:
  • Adding a "compatibility" option in "Notation" for alerting that an abbreviation or notation is deprecated.
  • new code for filter/partition was applied in MSetAVL
  • ...
• Hugo:
  • proposes to add "Set Parsing Explicit" to deactivating implicit argumets (request from Assia and Guillaume for educational purpose [done 20/1/12])
  • proposes to use "idtac foo" as possible breakpoints in Ltac [done 20/1/12]

At the time of the GT, 8.4 was planned for end of March [not done yet]

Open questions:

• Should we document tactics from Tactics.v?
• Assia: efficiency issues are critical for some files of the math. comp. library (especially separable.v and wielandt_fixpoint.v)

Reference Manual

Hugo suggested that a pass be collectively done on the Reference Manual (correctness of the text, evaluation of the global and local organization of the documentation, correct balance between the different sections, possible obsolescence of some sections, all other recommendations for improvement).

The followed names agreed to work on the following chapters:

• Chapter 2 (Gallina): Hugo + Enrico
• Chapter 3 (Gallina extensions): Jean-Marc
• Chapter 8 (tactics): Assia + Guillaume
• Chapter 9 (Ltac): Pierre Letouzey
• Chapter 11 (C-zar): Jean-Marc
• Chapter 12 (notations): Pierre-Yves
• Chapter 18 and 20 (type classes + setoids): Cyril