Gregory Malecha (Aug 01 2020 at 23:42): Gregory Malecha (Aug 01 2020 at 23:42):I had hoped that stdlib2 would provide more guiding principles and more core for people to build on. I haven't followed closely enough
Bas Spitters (Aug 02 2020 at 12:00):There does not seem to be too much progress on stdlib2.
Considering the previous discussion about coding conventions. It should be possible to write linter for this:
https://github.com/coq/stdlib2/blob/master/CONTRIBUTING.md
This script could be a start:
http://www.eelis.net/coqindent/
https://sympa.inria.fr/sympa/arc/coq-club/2009-11/msg00074.html
Notification Bot (Aug 02 2020 at 13:39):This topic was moved here from #Coq Platform devs & users > coq-ext-lib by Théo Zimmermann
Gregory Malecha (Aug 02 2020 at 14:59):I'm thinking less about naming and notation and more about core abstractions, e.g. Monad, Monoid, etc. Both ExtLib and stdpp define Monad, some form of decide, finite maps, etc in different ways and that basically means that there's no way to interface those two components. If there was a canonical definition that we could get behind, then we wouldn't need to worry so much about re-inventing each wheel :-) I probably contributed to this problem with the definitions in ExtLib because, I will admit, that I did not look closely at your past work at the time. I would be very eager to remedy this (though there are obviously time constraints on my side and the sides of other interested parties).
Last updated: Oct 13 2024 at 01:02 UTC