Add MathComp Analysis to the Coq Platform

[palmskog]

Analysis is a library for real analysis using the Mathematical Components library.

Real analysis is a critical ingredient in many applications of Coq for software verification and formalized mathematics. Analysis bridges the gap between Coq standard library reals and Mathematical Components structures. Hence, even though it is currently described as an experimental library, I propose that Analysis is included in the platform.

To my knowledge, the release managers of Analysis are @affeldt-aist and @CohenCyril.

[affeldt-aist]

Note that we have just released a version compatible with Coq 8.12 (https://github.com/math-comp/analysis/releases/tag/0.3.2).

[MSoegtropIMC]

@palmskog : can you please work with the authors to get some statement. Since it is still 0.X I would anyway only include it into the "extended" section, but even for this I would need some statement by the authors that they plan to bring it to release quality and maintain it then - not a commitment but at least a sincere plan.

Technically it is in with (#143) but I will remove it before release without a statement.

[CohenCyril]

Dear @MSoegtropIMC the only reason why it is still 0.X is that it has not yet reached mathcomp (or rather its 6 core packages) quality of code, but as Coq developments go, I'd say the quality is more than decent, constantly increasing and there is a sincere plan (and commitment of some of us) to maintain and eventually reach the same stability as the rest of mathcomp.

[MSoegtropIMC]

@CohenCyril : thanks for the confirmation! If mathcomp is the reference for the versioning, I agree that a 0.X might have a very high quality.

So where would you like to see it: in "full" or in "extended"? I would say in this case we can make an exception. The question is if you plan to do major incompatible changes in the future, so that users of the package might be forced to do a major refactoring of dependent code, or if you see the interface mostly stable, so that adjusting dependent projects to future changes shouldn't be a large effort.

A 0.X version number usually means that the authors expect major changes - even if the current quality is already quite high. But as you said, different projects might have a different scale for their version numbers.

[MSoegtropIMC]

@CohenCyril : I am not sure if you have seen (math-comp/analysis#437). Another thing beside the "maintainer agreement" is an example file to add to our "smoke test kit". It should compile without -Q options when the package is installed via opam, run in a few seconds (<10) and test as much of the package as possible in this time. This is mostly to test if the installation of a package is OK.

[CohenCyril]

I guess we can go for "full".

[MSoegtropIMC]

I included MathComp Analysis in the "full" level of 2021.09 8.13 and intend to also include it in 2021.09 8.14+beta.

So we are all set and I will close this issue.