CoqWG20171218 - coq/coq GitHub Wiki
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