Stream: math-comp analysis

Topic: new package mathcomp-classical

view this post on Zulip Michael Soegtrop (Feb 27 2023 at 15:00):

Working on the Coq Platform pick for 8.17 I saw that you created a new opam package "coq-mathcomp-classical". You should think about if this should become a user visible package in Coq Platform or be a hidden dependency. I didn't look at it as yet and don't have an opinion. It is mostly a question of visibility. If the versions stay tied there is little technical difference. If you make it a user visible package, you will get independent "please pick/create tag" issues from me during package pick creation, but the effect will be the same since I guess you will always pick the same version.

view this post on Zulip Karl Palmskog (Feb 27 2023 at 15:04):

my suggestion is that it becomes a proper package, it's of interest to anyone doing MC + classical logic.

view this post on Zulip Michael Soegtrop (Feb 27 2023 at 15:09):

In this case I would require a package addition request issue - just to follow the protocol.

view this post on Zulip Pierre Roux (Feb 27 2023 at 15:31):

I'd say this should have the same status wrt coq-mathcomp-analysis that coq-mathcomp-ssreflect has wrt coq-mathcomp-algebra.

view this post on Zulip Michael Soegtrop (Feb 27 2023 at 15:45):

@Pierre Roux : one difference is, though, that mathcomp-analysis and mathcomp-classical share the same repo. But this is not unheard of for separate top level packages.

view this post on Zulip Michael Soegtrop (Feb 27 2023 at 15:46):

As I said, if it shall be a user visible package, I need an inclusion request. Cause of the repo sharing this is a formality, but I prefer to play by Coq Platform rules.

view this post on Zulip Pierre Roux (Feb 27 2023 at 16:23):

This should indeed be a user visible package. How would you prefer the inclusion request to be formalized?

view this post on Zulip Pierre Roux (Feb 27 2023 at 16:24):

Michael Soegtrop said:

Pierre Roux : one difference is, though, that mathcomp-analysis and mathcomp-classical share the same repo. But this is not unheard of for separate top level packages.

Indeed, mathcomp-ssreflect and mathcomp-algebra similarly share the same repo, that was my point.

view this post on Zulip Karl Palmskog (Feb 27 2023 at 16:24):

just follow something like this: https://github.com/coq/platform/issues/307

view this post on Zulip Pierre Roux (Feb 27 2023 at 16:29):

Thanks, here it is: https://github.com/coq/platform/issues/334

view this post on Zulip Cyril Cohen (Feb 27 2023 at 17:06):

Thanks !

Last updated: Oct 13 2024 at 01:02 UTC