CoqWG 2020 05 04

Organization

This Coq Working Group was held from 2pm to 5pm (Paris time) on May 4th, 2020.

The WG has been recorded and is available here (note the menu on the left that allows to quickly jump somewhere into the video based on the current slide).

A video capture of the BBB recording above is available on YouTube at https://www.youtube.com/watch?v=foRHeEtORsM.

Topics

• Choosing the 8.13 release manager(s).
• Report on the status of MetaCoq and a technical point on subject reduction and primitive projections (Matthieu, 30-45 min)
• The state of the reference manual (Théo, 30 minutes)
• Maybe doing a tour de table on our objectives and priorities?

Participants

We will be using videoconferencing software to allow presentations that requires private registration, so please add your email to this list of participants if you intend to participate: send an e-mail to theo at irif dot fr if you want to register late.

• Matthieu Sozeau (matthieu dot sozeau at inria.fr)
• Théo Zimmermann (theo at irif dot fr)
• Richard Ford (richardlford at gmail dot com)
• Gaëtan Gilbert (gaetan.gilbert@skyskimmer.net)
• Anton Trunov (anton dot a dot trunov at gmail dot com)
• Enrico Tassi (enrico dot tassi at inria.fr)
• Simon Boulier (simon dot boulier at inria.fr)
• Karl Palmskog (palmskog at kth.se)
• Guillaume Melquiond (guillaume.melquiond@inria.fr)
• Jim Fehrle (jim dot fehrle at gmail.com)
• Cyril Cohen (cyril.cohen@inria.fr)
• Pierre-Marie Pédrot (pierre dash marie dot pedrot at inria dot fr)
• Jason Gross (jasongross9@gmail.com), conditional on him being awake early enough
• Hugo Herbelin (hugo dot herbelin at inria dot fr)
• Emilio Gallego (e at x80.org / emilio-jesus.gallego-arias at inria.fr)
• Yves Bertot (at inria fr)
• Kazuhiko Sakaguchi (sakaguchi@coins.tsukuba.ac.jp)

Visio details

We will use the Big Blue Button from IRIF. Details have been sent by e-mail to registered participants.

Notes (from Matthieu)

8.13 Release Management

• Enrico agrees to take the role, but not alone. Now checking with Maxime if he agrees to pair up :)

Reference Manual / doc update

• doc_grammar tool by Jim to check the grammar vs reference manual consistency

  Documented and usable with both make and dune. Can and should be used by developers but not currently a requirement.

• Clément is working on improvements of the sphinx doc. Théo mentions odoc's work. The CNRS engineer proposal is a bit unclear.

  Generally, we feel a lack of cross referencing the code and refman, e.g. pointing to documentation when raising a warning. Dually, pointing to the stdlib from the reference manual examples.

8.12

Dune not the main build system yet for 8.12. Still remains obstacles besides native_compute.

quick mode not supported yet (different build strategy)? vos and vok also not supported yet. Not necessary for Coq itself though.

Roundtable

• PMP working on side-effects/delayed proof terms. Removing technical debt (in which parts?)

• Théo: CEP 42. Moving platform and Coq Community.

• Hugo: Primitive projections and global fixpoints: how to make progress.

• Jim: Working on the syntax and the doc and the grammar tool.

• Enrico: Working on ELPI as an extension for Coq. In particular the hierarchy builder which might become

• Maxime: Document manager and VSCode improvements and work on stdlib2. Much infrastructure work in the architecture of VSCode and the protocol.

  Hugo asks about having improvements on IDEs shared. Common infrastructure document manager and protocol for all IDEs with minimal information about the document.

• Yves: not so much Coq-related stuff. But demonstrating Flocq + CompCert + Gappa and floating point computations (IIUC).

• Michael and Vincent Semeria: work on computation with constructive reals.

• Gaëtan: working on getting UIP integrated (as a flag, Lean importer). Coercion import path.

• Matthieu: working on completing MetaCoq/CertiCoq. Need a CEP on shelving / goal management to unblock https://github.com/coq/coq/pull/7825