CoqWG20141023

Organization

This WG took place October 23th at PPS/Sophie Germain, 3rd floor, in the morning, from 10am to 13:30am, then, also during the afternoon.

Participants

Yves, Matthieu, Cyril, Hugo, Andrew, Enrico, Guillame M, Yann, Pierre L, Pierre-Marie, Maxime, Assia, Lourdes, Guillaume C, Pierre-Evariste Dagand.

International evolution of Coq by Yves Bertot

• For Inria Coq is important, they support it, but they want to do it in an organized way. Inria wants a consortium with industrial partners, but is also OK with academic partners. It can provide resources but is unclear how much. If the system is driven by a consortium, how do we weight the partners (given that Inria is the only one paying today?)

• We do have users, using Coq for their own research. High increasing ratio. Users say it is good piece of work but are not completely happy. The devel team did not increase at the same ratio of the user base. We need resources from outside Inria, but one has to show how the extra resources are going to be used.

• A step toward easing contributions: streamlining API for user contribution via plugin (with P. Letouzey)

  • The 2 year position to streamline the API and document them is still open. The problem for some potential candidates is again the duration.

• One important annoyance is: "contributions" are hardly integrated

  • Arnaud: we need a reviewing process
  • A problem: who maintains things that are integrated?
    • Yves: at least we should make it clear what the policy/reason is to explain why things are not integrated
  • Engineers: (related to the previous item, but discussed at the very end)
    • Who trains them? Are they permanent? Do we have qualified manpower to hire?
      • The problem seems: if the positions are permanent, yes we do or we are ready to invest time in training them. If they are temporary positions, qualified people will not apply, and we will lack motivation to train them (they will leave before we take profit).

• USA proposals for fundings should include some money to sustain the development of Coq (Yves is actively pushing this on a project being submitted now on a full certified software stack).

  • Andrew: it is hard to get money to pay people in France to develop Coq; much simpler to train/hire someone in the US to do that. Hence where an "open structure for Coq" would help.

• We try to have 2 workshops per year, see also "Meet the coq-dev" below

• Reorganizing the way things are developed:

  • Should we delimit critical parts of the source code and have a "trusted" set of developers? Maybe the distinction is between developers and "packagers" assembling what people call Coq but as an aggregate of various components?
  • Who maintains things is a real concern for Hugo
  • Yves: we may accept a contribution only if it comes with manpower

Presentation by Andrew Tolmach of his research

• Here for 1 year at LRI.
• Software engineering techniques for formal proofs, esp. refactorings
• Looking for interactions with developers to eventually build a prototype.

Guillame Claret on Opam-Coq

• (tentative name coq-eggs, indeed a Coq makes no eggs)
• demo of opam: installs coq, makes a new coq package depending on ninjas, then makes the pull request to integrate the package in the main repo of coq packages for opam.
• proposes some policies about naming, versioning, etc, e.g. names of the form coq-foo; policy to discuss with opam developers
• bench: scripts around opam to compile packages + generate a website with the results
• Guillaume and Yann will review pull requests for adding packages

Miscellaneous discussions

Meet the Coq-dev / Coq implementors meeting

• Idea by Derek: merge with Coq-workshop
• Yves/Enrico: can we do the two events during 1 week in Sophia?
• Yves/Enrico will check if it is doable in May-Nov (summer)

Website

• put subscription instructions to coqdev on the website
• almost migrated to the new machine
  • cocorico (should be easy)
  • bugzilla (easy)
  • we should probably use stack-overflow instead of the in-home FAQ thing called OSQA by Yann
• better to switch to html+css on a git repo (Drupal is unmaintainable)

Tutorial

• mail by Nahas on coqdev. put his tutorial on the website.
• unclear if it will end up in CoqIDE, since "today you look for things via goole" seemd a killer argument.

Coq 8.5

• Should it be 9.0? No, it is not disruptive hence it stays 8.x
• Should we use that number to say that we drop retro compatibility to simplify and clean up the code?
• Hugo makes the point that preserving backward compatibility is making the development of new features too high. We could announce that 8.5 is the last release were so much effort is put in retro-compat.
• Enrico thinks that advertising that the next version will break feature X in advance is bad communication. We shall do that when we have a replacement Y for X ready.
• 8.5 has Ltac incompatibilities. Bedrock is hard to repair.
  • Yves: we try to be kind and involve Adam in the porting to 8.5, but we won't wait for the porting to happen before releasing 8.5-beta.
  • Beta release to be made in few weeks (still some broken contribs, still minor API fixes by Arnaud to be made).