We switched to Rendez-vous Renater because visio.inria.fr was not working properly
The topic list was not refreshed but "Dropping support for coq-8.10 [...]" point from the last time popped up again since Coq is not silent about attributes that do not exist and Coq 8.13 came out though, so we could drop it.
we should send the problem to Coq developers
Enrico will talk about it during the Coq call this afternoon.
Unknown attributes should at least have a configurable error message (which could be turned to warning)
Next release should happen in between 8.14+beta1 and 8.14 (rather than before)
Since we are now compatible with Coq [8.11, 8.12, 8.13] and by the time we release mathcomp 1.13, we would be compatible with four versions of Coq [8.11, ..., 8.14] we agreed to drop support for 8.10 in master and for the next release.
The only advantage -- but nonetheless critical -- is to make use of Coq's deprecation mechanism
Next release will be postponed by 1 month and will happen on June 2021.
Last release was smoother than before, because
the release process went without incident, we could even update the docker ourselves
the PR were triaged
The documentation process changed: one now has access to the documentation of several versions of mathcomp