Inclusion in the Coq Platform

[MSoegtropIMC]

Dear Xavier,

@palmskog requested here: (coq/platform#17) to include your development into the Coq Platform, which is the standard user facing distribution of Coq.

Coq Platform has a "full" and "extended" level. Inclusion in the "full" level requires an explicit statement by the maintainers, that they agree to the charter of the Coq Platform and intend to publish compatible releases for each release of Coq in a reasonable time frame. For the "extended" level the rules are more relaxed. For developments in the "full" level, users should be able to rely on that the package is maintained, so that they can base their own development on it without a large risk that they have to factor it out again later cause of maintenance issues.

Can you please comment in the Coq Platform issue mentioned above if you do want your package included in the Coq Platform in agreement to the Coq Platform charter, and if so which level you would prefer?

Best regards,

Michael

[xavierleroy]

For the record (see coq/platform#17): now that there's some official documentation for the .glob format, I'm confident that coq2html can be maintained in the future without too much effort, so I'd be happy to have it included in the Coq Platform, maybe at the Extended level originally, while I'm trying to attract other developers to join me on maintaining coq2html in a timely manner, so as to meet the Full level requirements later.

[palmskog]

@affeldt-aist @yoshihiro503 maybe it makes sense to integrate MathComp-friendly changes upstream rather than in forks then, if coq2html could join the Platform?

(cf. https://github.com/yoshihiro503/coq2html https://github.com/affeldt-aist/coq2html https://math-comp.github.io/analysis/htmldoc_0_6_7/)

[xavierleroy]

I just mentioned this possibility to @affeldt-aist. Don't leave me alone maintaining this tool!