CoqWG 2019 02 06

The first Coq Working Group of 2019 will take place in Paris on February 6th/7th 2019

The meeting will take place at Inria Paris: Room A226

Visioconference Access

Inria Room 308 pin 8024 on Wednesday

Inria Room 310 pin 9136 on Thursday

On a local computer, visit visio.inria.fr and input the credentials to get access to the room.

Schedule

The WG will be split over two days with the following schedule:

• 6th: 11am-1pm / 3pm - 5pm
• 7th: 10am-1pm / 3pm - 4pm

The detailed schedule is as follows:

Wednesday, February 6th 2019:

• 11 a.m.:

  • Changes in Coq since the last WG (Vincent, 15 minutes)
    • Quiet period, less than 110 changes (merged PRs)
    • Document by Vincent: Changes-in-Coq-since-the-last-WG-(20181216)
    • SProp => waiting for review, docs have been reviewed, a few rough edges but fairly ready, one issue still remaining
  • Stale Pull Requests [@ejgallego, 15 minutes]
    • Many open issues, many open PRs => this is a big problem
    • Using a tag to re-triage?
    • Théo: automatic closing? Not too fond of it. Try to close issues more often. Add to known_issues doc? Labels?
    • Classification? 25% not even labelled. Classification for component? Improve on labels?
    • Conclusion: issues is an important subject, we try to label and triage issues better, more manpower. About PR, we still didn't converge, consensus on whether to close? 30 days limit? Next WG more time for session.
  • Requirements of an ideal Proof_global API (@mattam82, 30min)
    • Slides by Matthieu
    • Long discussion about abstract / document model
    • Good first design document, we will try to make progress towards implementation

• 12 a.m.:

  • Coq packages and the upper bound policy (@gares, 20 minutes)
    • Slides by Enrico
    • Upper bounds added when Coq was releasing every 2-3 years
    • Now we release often, Coq has better backward policy
    • Better testing needed than just compiling [notations / runtime]
    • Using OPAM 2.0 for 8.10 released ?
    • Conclusion: we add automation, then we relax upper bounds; (strict vs soft upper bounds)
  • Coq development team communication [@ejgallego 20 mins]
    • Site is missing list of members, list of developers; role of communication person?
    • Open an issue to update list of current and past members
    • Hiring a professional in web communication would be very useful
    • Community manager?
    • Institutional communication: different role, with INRIA and with others. Needs to improve
    • One or several persons for communication
    • Developers talking personally vs the responsability they bear as representatives of the Coq team.
  • Launching Coq's Discourse (@Zimmi48, 20 minutes)
    • Discourse: modern software for forums (example https://discuss.ocaml.org/)
    • Instance created by Théo, to decide: division in categories; maybe OCaml and Nix have too many.
    • Proposal for categories: learning plugin development coq development announcements general discussion
    • Create some content before advertising
    • Role vs other existing systems [mailing list / stack overflow] etc...
    • What to do with coqdev [replaced by discourse] needs discussion

• 1 p.m.: Lunch !

• 3 p.m.: Template universe polymorphism, present and future. [@gares, 1 hour]

  • Soundness bug https://github.com/coq/coq/issues/9294 8.9 released with it [inadvertenly]
  • Proposal by @mattam82 to fix https://github.com/coq/coq/pull/9444 , long term fix?
  • Removal of template poly? => everything would break.
  • What would a hot fix be? Possible.
  • The plan for 8.9 is the hotfix, for 8.10 the full PR.

• 4 p.m.: Diversity in the Coq Community (@ejgallego, 30-45 minutes)

  • Some complains about diversity for some Coq events, this made us realize we should try to be more proactive about it
  • Lack of diversity on the core team makes it difficult to attract / understand possible issues.
  • 3 people listening, Larry Lee joins and provides some comments.
  • Coq has a bad visibility low / bad discoverability
  • learning material is bad, in particular for people not in the type theory community
  • user communities are missing
  • Théo => making it easier for groups to form => community page about users => group in Japan
  • presentations about Coq in devs / industrial conferences? Adam has been doing that
  • Yves: documents written are too academic? Larry: BIAS is very theoretical, requires type theory etc...
  • community should be more proactive =>
    • "here's what we are doing"
    • "here is what is going on in your area"
  • Gabriel: Japanese / French / Spanish versions of discourse
  • Outreachy: should be easy to do and with good effort
  • We decide to continue a diversity meeting for every WG

Thursday, February 7th 2019:

• 10 a.m.:

  • Anonymous sections (@maximedenes, 20 mins)
    • Conclusion: let's wait.
  • Making parsing and execution phases independent (@maximedenes, 20 mins)
    • Current parsing requires full state [notations, etc...]
    • Some cleanups have made the parsing state functional, cleanups very welcome
    • Big milestone [removal of dynamic commands] almost there
    • Ok to remove the Refine Instance Mode option
  • Towards taking benefit of primitive projections in the standard library (@herbelin, 20 minutes)
    • What is the motivation and meaning of PrimProjs [compact representation vs negative]
    • Compatibility mode is problematic
  • A reflection on our organization model (@herbelin, 30 minutes)

• 11:30 a.m.:

  • Hacking session

• 1 p.m.: Lunch

• 2:30 p.m.:

  • Plan for voi/vos integration (@charguer, 45 minutes)
    • Having a single vo [with holes] vos? Rules when both files a present?
    • Karl mentions they need to check single proofs
    • Size of the vio file?
    • Incremental compilation, too early? There are already two papers [iCoq & piCoq]
    • Arthur proposes file format, also in https://github.com/ejgallego/coq-serapi/issues/108
    • More feedback by Karl https://github.com/coq/coq/issues/9262
    • It seems good to merge; we should notify Arthur about the right rebase point and try to merge
    • Would be very interesting to rerun icoq to get data
  • GTK3 and CoqIDE (@ejgallego, @herbelin, 15 minutes)
    • GTK2 being deprecated fast in some distributions such as Debian
    • Huge effort by Hugo to port to GTK 3 https://github.com/coq/coq/pull/9279 , almost ready
    • Status bar lost because it needs to be ported from pixmap to cairo
    • We will merge the GTK3 version on master
    • Release a GTK3 version for 8.9.1?

• 19:00 Coq Users in Paris Meetup: At École de Mines de Paris, Salle V334 [Metro Luxembourg] https://www.meetup.com/Coq-Users-in-PariS/events/258266635/

Proposed topics

• template universe polymorphism, present and future. Given the current status of the universes I think we should sit around a table and come up with a plan. I'm not the most competent one on the subject (@gares) so I hope Hugo, Matthieu and Gaetan want to participate. It may not be of general interest, it may be worth doing it in the spare time. I think > 1h. @mattam82, maybe should be scheduled the latest on the 7th?
• coq packages and the upper bound policy (@gares, 20 minutes)
• Diversity in the Coq Community (@ejgallego) (30-45 minutes, last session of the 6th as to allow people overseas to participate)
• Towards taking benefit of primitive projections in the standard library (@herbelin)
• A reflection on our organization model: for instance, I feel that more planning and clearer task dispatching would help, but maybe are we satisfied with more freedom in selecting our priorities? (@herbelin)
• launching Coq's Discourse (@Zimmi48, 20 minutes)
• Plan for voi/vos integration (@charguer, on the 7th after lunch) [@ejgallego: people overseas wants to participate so let's make this at 14:00]
• Making parsing and execution phases independent (@maximedenes, 20 mins, on the 7th)
• Anonymous sections (@maximedenes, 20 mins, on the 7th)
• GTK3 and CoqIDE (@ejgallego @herbelin 15 min)
• Requirements of an ideal Proof_global API (@mattam82, 30min, on the 6th is fine): what functionality I/we would like to have and how does it interact with the STM/document model.
• Changes in Coq since the last WG (Vincent, 15mn?)
• Stale Pull Requests [@ejgallego 15min]
• Coq development team communication: no official communication head, no team members page, etc... [@ejgallego 20 mins]