CoqWG20140606

= Organisation =

This WG took place June 6th at PPS/Sophie Germain, 3rd floor, in the morning, from 9.30am to noon (coffee at 9am) and continued in the afternoon.

= Talks =

If you intend to give a talk, please add your name and title here and any information you'd like to give.

• Carst Tankink, A Quick jEdit+Coq demo (15min). I'll give a quick demo of the adaptation of Isabelle/jEdit's codebase to work with Coq, to allow asynchronous proof authoring.
• Pierre Boutillier, Review and proposal about manpower organization in Coq. (10min + discussions)
• Pierre-Marie Pédrot, Less global, better multigoal, fewer by default, ... tactics (30 min)

= Talking points =

• (Meta)data storage and installation (.glob, .aux, .cm*, .native, .o, .v, .vo, ...)
• SDK and precompiled plugins for 8.5
• Towards a bit more primitive notations for the standard library (e.g. for "existT", "exist", "proj1_sig", etc, for "S", for "eq_rect", for groupoid laws of equality, ...)?
• avoiding re-typing ltac bindings at use-time?
• Update on the migration of web/bugzilla/contribs, benchmarking tools
• release process, bug support policy

= Participants =

Frédéric Blanqui, Pierre Boutillier, Hugo Herbelin, Pierre Letouzey, Guillaume Melquiond, Matthieu Sozeau, Arnaud Spiwack, Carst Tankink, Enrico Tassi.

= Presentation of the new Jedit interface to Coq by Carst Tankink =

• A nice presentation with features such as constants hyperlinked in the editing window, or intermediate subgoals printed when partially evaluating a 3-steps tactic such as "rewrite H1, H2, H3".

• Discussion on completely separating the development of interfaces from the development of Coq; discussion on favoring adding new GUI extensions to CoqIDE, Jedit, PG, ...

= Guard condition =

Maxime asks about what to do with fixing guard for inductive and coinductive. At the current time, it is decided to go the safest way.

= Proposal for a revision of the TACTIC EXTEND model by Pierre-Marie Pédrot =

The idea is to move the parsing/pretting part of TACTIC EXTEND in ML files to "Tactic Notation"s in v-files. So, in TACTIC EXTEND, only lines of the form '"kwd" constr(c) ident(id)' are accepted, and used for interpreting Ltac expressions of the form "kwd c1 ipat:id".

Also, TACTIC EXTEND would produce arguments at the glob-level rather than at the type-level as now; it is the ml code which would be in charge of typing.

= Patch from Pierre-Marie Pédrot about drastically reducing time in univ.ml =

Patch is accepted.

Decision taken also to have the checker completely independent of the rest of the code (in particular this means having two univ.ml).

= Code cleaning =

Pierre Letouzey explains that sometimes anomalies are caught. The policy is not to do such catching.

= Presentation of the syntax for explicit universes by Matthieu Sozeau =

Matthieu proposed syntax "Type{foo}" for declaring an explicit universe level and "constant@{foo bar}" for instantiation of universe parameter of a constant.

Discussion about the alternative "Type@{foo}".

= New bench/web server

Xavier Clerc is working on using INRIA's Jenkins for compilation tests (see https://ci.inria.fr/coq)

• pyrolyse.rocq.inria.fr is a host for heavy compilation
• coq.rocq.inria.fr is a host for web server

= Auxiliary data storage and installation =

Generated files .cm*, .native, .o are at the date of the WG in a hidden directory .coq-native and .aux are hidden files.

Long discussion which seems to converge toward having a non hidden directory "coq-build" local to each directory for all generated files except the *.vi and *.vo files.

= About the Coq public service =

• pull requests on coq github: being clearer on whether this repository is officially watched by coq developpers or not

= User contributions =

Discussion on making developments in Coq more visible world wide.