Karl Palmskog (Aug 01 2020 at 14:49): Karl Palmskog (Aug 01 2020 at 14:49):@Gregory Malecha to get increased exposure/users and hopefully more volunteers, may I suggest that you open an issue about including coq-ext-lib in the Coq platform? https://github.com/MSoegtropIMC/coq-platform/issues
Bas Spitters (Aug 01 2020 at 17:06):With the stdlib becoming more open would it make sense to integrate ext-lib more into it (or into stdlib2)
Karl Palmskog (Aug 01 2020 at 17:11):that sounds like a sizable integration effort, at least the Coq Platform exists right now in some form
Bas Spitters (Aug 01 2020 at 17:14):Agreed
Karl Palmskog (Aug 01 2020 at 17:24):to be honest, I wish there were more incentives for research into library integration. For example, I'm not sure if a paper describing some clever way of integrating Stdlib and ext-lib would stand a chance at CPP, much less POPL
Gregory Malecha (Aug 01 2020 at 23:41):I would love to move part or all of ext-lib into the platform, and would be happy to open an issue for it. Unfortunately, there is a non-trivial amount of overlap with stdpp and not all choices are compatible, e.g. both have monad libraries, both have different reasoning principles for finite maps, etc.
Karl Palmskog (Aug 01 2020 at 23:51):there is not really any criterion for non-overlap with other parts of Coq Platform. For example, MathComp and stdpp are in my view quite strongly overlapping, and they will both be included. Specifically, mathcomp-finmap is an obvious "competitor" to stdpp's finite maps.
Michael Soegtrop (Aug 02 2020 at 09:24):@Gregory Malecha : there is not need to be orthogonal. The Coq platform is more a collection of packages with let's say a more dependable maintenance contract. So if ext-lib is included in the platform the deal is that you promise to put reasonable efforts in making a compatible release for each Coq release in a reasonable amount of time. The idea is not to tell users "this is the best library for that". The idea is to have an easy way to install an over Coq releases consistent set of libraries and to allow users to experiment and choose. But if they made a choice, they should be able to rely on that this choice is still supported a year later.
This is not as trivial as it might sound. E.g. currently it is quite common that if you want to try 3 different libraries for the same purpose - say a monad library - and you want to install them via opam, opam might tell you that you have to up/downgrade 5 other packages for each of these 3 packages which influence other parts of your developments. So while the platform does not guarantee that packages are orthogonal, it does guarantee that they share the same versions of dependencies.
See (https://github.com/MSoegtropIMC/coq-platform/blob/master/charter.md) for more details.
Notification Bot (Aug 02 2020 at 13:38):This topic was moved here from #coq-community devs & users > coq-ext-lib : No proof for FMapTwoThreeK by Théo Zimmermann
Notification Bot (Aug 02 2020 at 13:39):This topic was moved by Théo Zimmermann to #coq/stdlib2 devs > Guiding principles
Last updated: Apr 18 2024 at 02:01 UTC