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, ...)? (not discussed)
• 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

No consensus found on "service" given to users

= User contributions =

Discussion on making developments in Coq more visible world wide.

= Release process =

Reminder that a check-list file exists in coq-dev-tools/distrib/RELEASE to ensure optimal releasing process (to be updated though)

About the concrete point of checking consistency between the official and effective versions of ocaml required, it has been suggested to use Jenkins