Stream: Coq Platform devs & users

Topic: Package categories


view this post on Zulip Michael Soegtrop (Sep 29 2021 at 13:10):

@Enrico Tassi @Karl Palmskog @Théo Zimmermann : can you please review the package categories (the comments over groups of packages) in packages-8.13.sh? I plan to use the same also for the overview pages.

Especially for mathcomp I don't understand the purpose of all packages and this might be done more fine grain. Also the automation group might be split up.

view this post on Zulip Karl Palmskog (Sep 29 2021 at 14:00):

we used another categorization completely in Coq-community, which nevertheless could be relevant: https://coq-community.org

view this post on Zulip Karl Palmskog (Sep 29 2021 at 14:08):

math-classes is not restricted to constructive mathematics, even though it doesn't use classic. So I think that categorization is misleading. It should either be viewed as a general-purpose library or a mathematics library

view this post on Zulip Michael Soegtrop (Sep 29 2021 at 15:20):

@Karl Palmskog : thanks for pointing out the Coq community categories. I think they are not that different. I will have a deeper look - maybe I just adopt these categories.

Regarding math-classes: I think not using classical axioms is a distinguishing feature which should be emphasized - IMHO it is obvious that you can use constructive results in non constructive works. @Bas Spitters : what is your opinion on the grouping of "math-classes"? Would you prefer "Constructive mathematics" or "General mathematics"?

view this post on Zulip Théo Zimmermann (Sep 29 2021 at 15:28):

I disagree on it being obvious that constructive results are useful for everyone. People with math background will often be very suspicious at constructive mathematics. Furthermore, the term "constructive mathematics" sometimes encompasses things that are highly incompatible with classical mathematics.

view this post on Zulip Pierre-Marie Pédrot (Sep 29 2021 at 15:30):

I confirm from experience that when the "constructive" curse word is uttered, most mathematicians will start hissing and flee away.

view this post on Zulip Théo Zimmermann (Sep 29 2021 at 15:31):

A further issue in putting math-classes under constructive mathematics is that mathcomp is just as constructive, and yet it has been put under general mathematics.

view this post on Zulip Théo Zimmermann (Sep 29 2021 at 15:32):

I suggest splitting the category "general mathematics" into "general mathematics" (for mathematical libraries which do not use classical axioms) and "classical mathematics" (coquelicot, mathcomp-analysis). Coq users will be very interested in this distinction as some of them might not want to use them.

view this post on Zulip Théo Zimmermann (Sep 29 2021 at 15:35):

OTOH, HoTT could very well go under the constructive mathematics category instead of being its own category.

view this post on Zulip Théo Zimmermann (Sep 29 2021 at 15:37):

SerAPI does not communicate with coqtop, it introduces its own protocol to communicate with Coq (bypassing any existing toplevel, it does provide its own alternative toplevel).

view this post on Zulip Ali Caglayan (Sep 29 2021 at 15:38):

While we are generally constructive in HoTT, we aren't forced to be. It's just that assuming classical axioms when necessary in a constructive setting is more convenient than the converse.

I am weary for the reasons PMP mentioned of putting HoTT in "constructive mathematics". In general, the nature of Coq makes everybody reason a bit more constructively if I am not mistaken.

view this post on Zulip Michael Soegtrop (Sep 29 2021 at 16:03):

Looks like I opened a can of worms. As engineer I am a constructive math fan - IMHO number which don't compute don't qualify as numbers ...

view this post on Zulip Michael Soegtrop (Sep 29 2021 at 16:05):

So I will need some help to find the least controversial categorization.

view this post on Zulip Michael Soegtrop (Sep 29 2021 at 16:05):

@Théo Zimmermann : I didn't know math-comp doesn't use classical axioms - I was only aware that math-comp analysis does.

view this post on Zulip Bas Spitters (Sep 29 2021 at 17:11):

I agree with what was said about. MC and HoTT do not assume anti-classical axioms, so they qualify as general mathematics.
Perhaps, more general mathematics ;-)

view this post on Zulip Michael Soegtrop (Sep 29 2021 at 17:42):

OK, I will rework the structure - likely adopting the structure from coq-community as @Karl Palmskog suggested. I will then ask for another review.


Last updated: Jan 30 2023 at 10:03 UTC