@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
With the stdlib becoming more open would it make sense to integrate ext-lib more into it (or into stdlib2)
that sounds like a sizable integration effort, at least the Coq Platform exists right now in some form
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
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.
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.
@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.
This topic was moved here from #coq-community devs & users > coq-ext-lib : No proof for FMapTwoThreeK by Théo Zimmermann
This topic was moved by Théo Zimmermann to #coq/stdlib2 devs > Guiding principles
Last updated: Jan 29 2023 at 19:02 UTC