@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.

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

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

@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"?

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.

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

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.

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.

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

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).

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.

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 ...

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

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

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 ;-)

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: Apr 20 2024 at 23:01 UTC