search

math-comp / analysis

Mathematical Components compliant Analysis Library
Other
206 stars 47 forks source link

Inclusion in the Coq Platform #437

Open MSoegtropIMC opened 3 years ago

MSoegtropIMC commented 3 years ago

Dear math-comp Team,

@palmskog requested here: (https://github.com/coq/platform/issues/21) 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

MSoegtropIMC commented 3 years ago

P.S.: I just saw that the opam package has a 0.X version number, which suggests it should go into the extended level.

MSoegtropIMC commented 3 years ago

P.P.S.: can you suggest an example file using this package for the Coq Platform "smoke test kit"?

CohenCyril commented 3 years ago

We do not have a "smoke test kit" file for now. When do you need it?

MSoegtropIMC commented 3 years ago

We do not have a "smoke test kit" file for now. When do you need it?

For the time being any file which is in your source tree and compiles iff the analysis package is installed would do. Typically math-comp components have proper module qualification, so I guess any quick compiling file in your source tree would do. For some math-comp components I simply use the "main include file", say "finmap.v" or "all_character.v", which is usually a reasonable check that the files of the package are where they should be.

We can later have something more fancy.

MSoegtropIMC commented 3 years ago

P.S.: I plan to create issues on all platform projects to provide a dedicated smoke test kit file, but I didn't finish the concept as yet, because some projects would need a smoke test script (say CompCert) and it is not so obvious how one should do this such that it works on macOS, Windows and Linux. Another issue is finding the smoke test kit file in projects where one source tree contains multiple projects (like math-comp). Ideally I would like to say "please provide a file smoke_test.v" which I can find in your source tree with find, but for math-comp this won't work.

Suggestions welcome!