Join GitHub today
GitHub is home to over 28 million developers working together to host and review code, manage projects, and build software together.Sign up
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:
- "sources" avec scripts pour http, svn, git
- Coq dev provided "patches"
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
- 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
- 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]
- Arnaud to-do's list:
- Unfocused as a replacement of Unfocus (cf aussi message d'erreur) [done end of March]
- 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
- 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]
- 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)
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