CoqWG20150512

Organization

The WG was held in Paris on May 12th at PPS, Sophie Germain, 10am.

Participants

Yves Bertot, Guillaume Claret, Julien Forest, Hugo Herbelin, Guillaume Melquiond, Pierre Letouzey, Cyprien Mangin, Pierre-Marie Pédrot, Matthieu Sozeau, Enrico Tassi, Andrew Tolmach.

Talks

Enrico about Opam

Talk based on https://github.com/gares/coq-opam-archive.

We give below an excerpt of the presentation and discussions.

Proposed layout for the opam repositories:

• core-dev (cot git)
• extra-dev (plugins/libraries git)
• released (coq+plugins/libraries, all versioned, included beta's, rc's)
• stable-8.4: a 8.4 globally consistent view at packages with links to "released"
• stable-8.5: a 8.5 globally consistent view at packages with links to "released"

Discussion on dropping the :contrib: name space for contribs with no maintainers and in removing the :contrib: version for contribs with an upstream version

Enrico's web site has a search engine

Category tags are taken from existing tags used for contributions

Providing a shell wrapper on top for opam to provide:

• opam coq help
• opam coq search
• opam coq install
• opem coq update
• opam coq upgrade

Tentative policy for submission at https://github.com/gares/coq-opam-archive:

A package can be updated as a stable package if all packages which depend on it are either adapted or kept working

Andrew: Haskell has a similar two-levels model: cabal and haskell-platform

Stable worlds:

• Enrico proposes to possibly keep several versions of a package as soon as there exists a selection of versions which makes the whole set of stable packages to compile
• To compensate the slow release cycle of Coq, Guillaume C proposes to add stable-8.4+6months views, etc.

Policy on quality:

• Hugo suggests: No Admitted, no admit (use Conjecture or Axiom instead)
• Hugo suggests: Have the target "make html" works; Pierre proposes a field with a link to documentation in opam description; using some "make doc" target of opam is also considered
• Hugo suggests no Obj.magic in ml code, towards insurance that kernel cannot be cheated; consensus seem to go towards doing code review by experts

Use of coq_makefile: recommended but not mandatory

Noone really willing to spend time reviewing code of packages

Pierre about extraction with Prop subset of Type

Pierre shows corner cases where extraction is not able to deal well with Prop subset of Type.

He shows on examples how the following embedding of Prop into Set solve the problem.

Set Primitive Projections.
Record lift (A:Prop) := up { down : A }.
Arguments up {A} _.
Arguments down {A} _.
Theorem up_down A (x:lift A) : up (down x) = x. Proof. reflexivity. Defined.
Theorem down_up (A:Prop) (x:A) : down (up x) = x. Proof. reflexivity. Defined.

One remaining issue is to look at how conversion works when Prop subset of Type is witnessed by up.

Yves about a consortium