Michael Soegtrop (Sep 29 2021 at 13:10): 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.
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
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
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"?
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.
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.
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.
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.
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.
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).
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.
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 ...
Michael Soegtrop (Sep 29 2021 at 16:05):So I will need some help to find the least controversial categorization.
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.
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 ;-)
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: Oct 13 2024 at 01:02 UTC