Hugo Herbelin (May 29 2020 at 21:25): Hugo Herbelin (May 29 2020 at 21:25):A crazy idea about the platform: would it make sense to relabel what is in the platform as "Coq standard library".
Théo Zimmermann (May 29 2020 at 21:26):What's the point?
Théo Zimmermann (May 29 2020 at 21:27):For sure the platform will be "a standard set of tools and libraries" but usually a "standard library" is meant to designate a more consistent thing developed by a core team.
Hugo Herbelin (May 29 2020 at 21:42):I see two objectives:
Note incidentally that the different packages of the "standard library" are already an assemblage of packages which actually don't necessarily come from a "core team".
Théo Zimmermann (May 29 2020 at 21:45):To make looser the border between standard library and other libraries, because there is no reason that the so-called "standard library" is put more in exergue than other interesting standard-library-relevant contents.
That's indeed one of the goals of the platform.
To incite developers of standard library contents to work together in the direction of a thematically organised library rather than team-based libraries. It is a pity that interesting similar definitions and lemmas are dispersed while the rule (from a user point of view) should be to organize them according to their purpose. (Libraries on reals or on lists are good examples of such dispersion which does not help the external users.)
This would be nice but is not going to happen simply because you name things differently.
Hugo Herbelin (May 29 2020 at 21:49):This would be nice but is not going to happen simply because you name things differently.
Of course, but if we accompany it of a statement that our intention is to provide users with a unified view at all standard-library-relevant content (as some other proof assistants do, and as we try to do currently with reals), and that this is an explicit mid-term objective, this would help.
Théo Zimmermann (May 29 2020 at 21:52):Again, I don't think making statements is enough. However, proving that coordination can happen, like you are doing with the reals library, can really help. I think the ongoing emulation around the reals libraries should be further highlighted and examplified.
Hugo Herbelin (May 29 2020 at 21:56):Yes, making statements is not enough, but as this kind of work is by nature a collective work, it also goes by already gathering a number of people to adhere to (the principle of) the project.
Hugo Herbelin (May 29 2020 at 22:00):My feeling is that today, many people would like to go in the direction of a project of this kind but that what is missing is precisely the formulation of a "framework" (reusing incidentally the word) and of a list of concrete objectives supporting this direction.
Hugo Herbelin (May 29 2020 at 22:09):Of course, there are many difficult questions (a difficult one being typically the question of an algebraic hierarchy) but there also relatively easy ones (such as naming conventions, choice of implicit arguments, notations based on type classes or not, ... which are of a more local nature). For the list library in particular, I'm sure a convergence could be obtained, because, this is not about taking the less but really more about collecting and organising, and at the end getting the more.
Last updated: Jun 03 2023 at 05:01 UTC