Coq Call 2021 10 27

• October 27th 2021, 4pm-5pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• https://github.com/coq/coq/pull/13861 use / in -print-mod-uid as dir separator on windows. (Gaëtan)
• https://github.com/coq/coq/pull/14857 move most ml code to core/ (Gaëtan)
• when to update the website with respect to a new release (need to wait for a platform release / announcement)? (Théo, follow-up of discussion at https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs.20.26.20plugin.20devs/topic/Coq.20Website).
• https://github.com/coq/coq/pull/14898 Debugger: Support setting line number and begin of line offset when calling parser (Jim)
• https://github.com/coq/coq/issues/15062 Remove "Add LoadPath"? (Jim)
• https://github.com/coq/coq/pull/14644 Debugger: discussion (if needed) (Jim)
• https://github.com/coq/coq/issues/14423 (How to/should we) allow this (Ali)

Notes

Regarding the issue of release announcements, it was decided to amend the process as follows. When a release candidate is tagged, a public announcement should be made, along the following lines: "Release candidate has been tagged. It can be experimented using core-dev. Library maintainers are encouraged to test and upgrade their libraries so that they are ready by the time of the actual release. In particular, maintainers of libraries that are part of the Coq platform should eagerly release compatible versions, so as to not delay the release of the Coq platform." When the actual release is tagged, no announcement is made; it is still delayed until the Coq platform is ready, as per the CEP.

• https://github.com/coq/coq/issues/15062 would break coqrc users that use Add LoadPath there. Before removing it we should fine another way to cater for this need. Put in .coqrc a -I ..., -Q ... could give the same functionality.

  => survey the users for this

  => the alternative of using _CoqProject / coq_makefile should be mature in combination with dune before we do anything