Coq Call 2020 04 22

• April 22th 2020, 4pm-5pm Paris Time
• The call will be on rendez-vous: https://rendez-vous.renater.fr/coq-call
• Add your topics below

Topics

Notes (from Matthieu)

• 8.12 release schedule

  Target: freeze May 15th, beta release early June, final release in July (ideally before the Coq Workshop) https://github.com/coq/coq/wiki/Release-Plan-for-Coq-8.12

• About the platform: Théo tried to get an intern but not possible currently. Michael Soegtrop is working on the platform, which will come some months after the 8.12 release. Current issues of 8.12 segfaulting on windows builds, currently investigated by Jason.

• 8.13 release manager(s)?

  Ideally should be chosen before branching, let's make it a point for the next Coq WG.

• Call for discussion on #12076 (coqchk, axioms and functors)

  It would be best to backport the Print Assumptions code in the checker instead of hacking the coqchk version (we have code duplication here). That would provide a better fix to the issue (in particular solving Ralf Jung's issue).

  PMP still points out that Parameter Inline is still broken w.r.t. tracking the use of typing flags that are not stable by unfolding/substitution. E.g., unfolding a type-in-type definition in a Parameter Inline instance? Jason has a test case for this.

• Preparing June's meeting on proof assistants?

  We don't have any news yet. Hugo suggests discussion of libraries, especially with the users. Problem of disparity of libraries and how to federate contributions. Funding question: with a clearer roadmap we might get specific funding, e.g. on the treatment of reals. => Recalls the question of clarifying the features we want and how to publicize them. Waiting for Alain Giraut's answer on the status of the meeting.

• if time permits, cry for help to univ masters: lifetime of a universe variable (Enrico asking)

  API issue here, we should warn that Evd.merge does not work when universes have been declared elsewhere (by side-effect).