Pierre Letouzey edited this page Nov 3, 2017 · 44 revisions

Second Coq Implementors Workshop, May 30 - June 3, 2016, Sophia-Antipolis

This page collects useful infos for the participants to the second Coq Implementors Workshop.

The Coq Implementors Workshop is an event that brings together the core developers of Coq and people willing to understand, improve or extend the system.


The Implementors Workshop takes place at the Inria Center in Sophia-Antipolis (how to reach the Inria center, accommodation infos).


Program PDF

Talks by devs:

Do log what you did/learnt/implemented!

Write it here.


For organization purposes we require the participants to register (free of charge) by subscribing to the coordination mailing list.

The mailing list is also the preferred channel to contact the organizers. Subscription is required in order to post.

Beach event


Quick list of dinner options

(pick what you prefer and build your dinner group around you)

List of participants

  1. Yves Bertot
  2. Maxime Dénès
  3. Enrico Tassi
  4. Pierre-Marie Pédrot
  5. Matej Košík
  6. Matthieu Sozeau
  7. Cyprien Mangin
  8. Guillaume Melquiond
  9. Pierre Letouzey
  10. Hugo Herbelin
  11. Emilio J. Gallego Arias
  12. Nicolas Magaud
  13. Pierre-Évariste Dagand
  14. Lionel Rieg
  15. Cyril Cohen
  16. Théo Zimmermann

(+) Late subscription (tradition says you pay a round at the pub...)

Bug squashing

bug triaging is very welcome (check if a bug is still valid, add extra info, close solved bugs...).

"Little" projects

Finish the safe string patch

A good little project is to submit some cleanups for -safe-string as hinted in

Fix Ocaml Warnings

Compiling Coq with Ocaml Warning enabled provides interesting cases to look at for cleanups. More details in Bug #4671.

A special interesting project is to get the kernel to compile warning clean with all warnings enabled.

Using Merlin is highly recommended for this task.

Remove redundant typing

In 8.4 setoid_rewrite, there was code to type-check terms known to be well-typed. It would be useful to scan the codebase to look for other redundant type-checks.

Brainstorming ("harder" projects, to be considered carefully)


Individual Projects

Insert here your individual plan for the week:

Emilio J. Gallego Arias

  • Look at weird behavior when using new universe unification (PR#178) and universe polimorphism (happens both in trunk and v8.5)
  • PR#143 merge: Follow the plan outlined at:
    • Feedback from the devs? Enrico is looking at it. PMP did a preliminary eval.
    • PR#133?
  • New protocol/serialization:
  • jsCoq/uDoc:
    • complete new linking support
    • Move to a thread.
    • new UI
    • vm_compute
  • Plugin packing: It would be great to have proper namespacing.

Discussion on the roadmap

The changes we should discuss during the implementors workshop are:

  • ? PR #143 now #179: Feedback/pp cleanup (E. J. Gallego)

    [EJGA] I should be able to get this in shape for 8.6. [EJGA] Done

  • ? PR #158: Fixing the "beautifier" and checking the parsing-printing reversibility (H. Herbelin)

  • ? PR #86: simplify sort_fields (G. Scherer)

  • ? PR #117: iota split into iota0+phi+psi and ML API cleanup for

    reduction functions (H. Herbelin)

  • ? New warning system

  • ? Flag deprecated commands: Add Setoid/Morphism/...?

  • ? Error resilient mode for STM (Enrico) #173

  • ? Compartimentalize IDE-API specific serialization in IDE (PR#180, EJGA). Parts of this could be merged on 8.6 but some more discussion is needed.

  • ? PR #79 Assume Positive/Guarded/... Syntax issue on attributes, naming.

  • ? New flag "Shrink Abstract" that minimizes proofs generated by the abstract

    tactical w.r.t. variables appearing in the body of the proof. Also improved Shrink Obligations.

  • ? PR #114: Set Debug Foo vs Set Foo Debug (H. Herbelin)

  • ? PR #67: Add a Show Proof query to CoqIDE

  • ? PR #166: Add -o option to coqc to choose the .vo file directory (Enrico)

  • ? Option to add eta-unification during resolution.

    • ? Option to do resolution following the dependency order of subgoals in resolution (previously, and by default, the most dependent ones are tried first, respecting the semantics of the previous proof engine).
    • ? Option to switch to an iterative deepening search strategy.
    • ?! New implementation of typeclasses eauto based on new proof engine, could replace eauto as well: full backtracking, Hint Cut supported, iterative deepening, limited search, ... (M. Sozeau) branch. To be turned into a PR, compatibility checks to do first.
  • ? congruence now uses build_selector from Equality (H. Herbelin)

  • ? PR #140: Iff as a proper connective (H. Herbelin)

  • ? PR #150: LtacProf (Coq v8.5) (J. Gross, P. Steckler)

  • ? Fix semantics of pattern-matching in Ltac (non-linear patterns, difference between hyps and goal and hyps)

    (M. Sozeau)

  • Update the website (contribs and others?)

  • opam ?

Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.