CoqWG20171218

Organization

This Coq Working Group took place on December 18th and 19th at Inria Paris (2, rue Simone Iff). Videos are available on Coq's YouTube channel

Topics

Monday:

• 10h-11h:

  • Equations & the Function replacement plan (Matthieu, Cyprien, Thierry, 45 min)
  • as [pat|..|pat] / as '(x, y, z) intropatterns / https://github.com/coq/coq/pull/1003 (15 min)

• 11h15-12h15:

  • Attributes (Vincent, 30 min)
  • Integers and arrays (Maxime, 30 min)

• 14h-15h:

  • API - Emilio

• 15h30-..: Technical work in groups, subject proposals (need one lead per group, not two groups with same lead).

  • EConstr API completion (taking input from e.g. Equations, ssreflect) Lead: Matthieu Participants: Cyprien? Pierre-Marie? Emilio
  • Evar_source/evar_kinds Lead: ? Participants: Matthieu, ...
  • Future goals and the shelf etc... looking at what unifall-infra adds there. Lead: ? Participants: Maxime, Emilio
  • Porting the ssr plugin to modern APIs Lead: Maxime Participants: Georges ? Pierre-Marie ? Enrico ? Emilio

Tuesday:

• 10h-11h00:

  • Plugin Developer Program (Emilio, 30 min)
  • Fire drill

• 11h15-12h15:

  • A presentation of TLC 2.0 (covering library design, not tactics) (Arthur, 45min + questions)

• 14h-15h:

  • Evaluation inside Coq with non-constructive recursive definitions (Arthur, 20 min)
  • Coq Meetup [Théo, Emilio] (15 min)

• 15h

  • coq-community, a new birth for Coq contribs (Théo, 25 minutes), or Ltac2 (or Ltac3) by Pierre-Marie (or Enrico)

• 15h30-..: Working groups

PRs that need to be discussed (possibly around a computer)

From oldest to most recent:

• https://github.com/coq/coq/pull/313 (Scoped options) Emilio suggests that this needs to be discussed with a small group, around a computer so we can have a closer look to the way liboject is working.
• https://github.com/coq/coq/pull/400 (Reducing temporary allocations in CClosure) Pierre-Marie needs to convince Guillaume of the importance of his patch, and Emilio that this has nothing to do with Flambda.
• https://github.com/coq/coq/pull/616 (Make some keywords into normal idents) Gaetan will lead the discussion (last time this was discussed, he was not here).
• ...
• https://github.com/coq/coq/pull/1003 (intros '(x,y)) The debate is about "syntactic pollution". I guess the people that are rather against the merge of this PR (Pierre-Marie, Maxime) should explain their viewpoint.
• https://github.com/coq/coq/pull/1136 (dir-locals)

Issues that need to be discussed (possibly around a computer)

• https://github.com/coq/coq/issues/5448 (Stack overflow on cbv delta in a trivial tactic in terms) Leader?

Participants

• Yves Bertot
• Cyril Cohen
• Maxime Dénès
• Emilio Gallego
• Gaëtan Gilbert
• Georges Gonthier
• Hugo Herbelin
• Vincent Laporte
• Guillaume Melquiond
• Pierre-Marie Pédrot
• Matthieu Sozeau
• Enrico Tassi
• Théo Zimmermann
• Arthur Charguéraud
• Cyprien Mangin