Coq Call 2020 06 03 - coq/coq GitHub Wiki

• June 3rd 2020, 4pm-5pm Paris Time
• The link to the visio room will be provided on Zulip the day of the call: https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs.20.26.20plugin.20devs/topic/Coq.20Call
• Add your topics below

Topics

• Coq workshop: presentation of the preliminary schedule (panels, invited talks) to get feedback (Emilio, Hugo and Théo)
• Releasing the beta (will we get a release summary?) (Emilio and Théo)
• Upgrading Jenkins on the bench (it's mostly automated, but there's a chance something might be broken afterwards), maybe also integrating coqbot with the bench (is there anything blocking https://github.com/coq/coq-bench/pull/85 ?) (Jason Gross)
• Integrating Unicoq to Coq? (Beta and Emilio?)
• Inductive-inductive types and "recursive-recursive" fixpoints update. (5min, Matthieu)

Notes (from Matthieu)

• Coq workshop: presentation of the preliminary schedule (panels, invited talks) to get feedback (Emilio, Hugo and Théo) Online 5-6th July. 13 talks, special session for the 35th birthday of Coq.

  Additional talks:

  • Coq dev session as usual
  • 3 panels/round-tables (1 hour each):

    • Libraries (Bas Spitters moderating) Potential participants: Cyril Cohen (math-comp), Gregory Malecha (extlib), Robbert Krebbers (stdpp), Guillaume Melquiond. Michael Soegtrup.

      • stdlib2 / coq-platform. Learning from the math-lib experience?

      Quite a wide subject that needs to be directed to focused points certainly. Polling for the questions/points of interest beforehand should help.

    • Automation and tactic languages Potential participants: Arthur Charguéraud moderating. Chantal Keller (SMTCoq), Cezary Kalinsky (coq-hammer?), Yann Régis-Gianas (MTac2), Jason Gross.

      Maybe focusing on a specific point, e.g. how to develop automation, rather than such a large topic?

      Adding decision procedure developers maybe?

    • Stabilization vs Evolution? Participants: Xavier Leroy, Nicolas Tabareau, Adam Chlipala. Dealing with technical debt, management of changes.

      Maxime: Maybe that should rather be the topic.

Overall we need a bit more precise information on the kind of information that we want to be gathered.

• Releasing the beta (will we get a release summary?) (Emilio and Théo)

  Well on its way. Release summary upcoming.

• Upgrading Jenkins on the bench (it's mostly automated, but there's a chance something might be broken afterwards), maybe also integrating coqbot with the bench (is there anything blocking https://github.com/coq/coq-bench/pull/85 ?) (Jason Gross)

  Needs some help from Maxime.

• Integrating Unicoq to Coq? (Beta and Emilio?)

  Should first move to a stack machine presentation before we can merge together with evarconv.