Why is Coq’s standard library “batteries not included”-style? I just saw this page for the first time, seeing the entire library represented so concisely is surprising: Standard Library | The Coq Proof Assistant. I’d categorize every item on this list into one of:
Tactics
Data structures
Relations on data structures
Alternate logics
Domain-specific proof/programming languages
This is a nice start, but I’d expect a mature system to also include
It seems very counter-productive for the community to rely on third parties for anything interesting - these should be first-class, standardized representations that a default install has access to. My guess is that at least one of the following is in the way:
Lack of maintainers
Failure to agree on what to add
~exists a standard representation for an above topic
An above topic is actually an umbrella term (category theory)
Desire to be similar to OCaml (I have similar qualms there)
Are any of these accurate? And is there hope for a batteries-included, first-party Coq standard library in the future?
There is the Coq Platform that provides an installation of Coq with a curated and large set of packages.
But beyond that, if you’re looking something even more first-class, what would be the motivation? What is the benefit of a batteries-included stdlib?
In earlier times, installing libraries was a wonky process for lack of a proper packaging mechanism. A large stdlib would palliate to that issue. Nowadays:
third-party libraries are just an opam install away;
besides Coq Platform, there are also Coq CI and coq-community as big initiatives helping ensure that a significant chunk of the ecosystem remains buildable with new versions of Coq, improving the reliability of opam install.
Maybe naively, I would say there are a bunch of reasons to link to what you mention:
First, when it comes to formalizing, the space of design choices is huge and crucial choices comes right at the beginning. For instance, for classical math you want your equality in Prop but for univalent one you would need to put it Type. There are many other choices like that which are not so clear, like which definition of the reals do you want ? Do you want to use type classes or canonical structures ? and it goes on. Moreover, often there are no best choice, and it depends on what you want to do. Also formalization is a research field so we don’t always know the answer either. Hopefully, with the new features currently developed for Coq like algebraic universes, Sort Poly, etc… it should make it either to get a nice stdlib.
Second, the current stdlib is old, in Coq’s repo which doesn’t help, and doesn’t have much people on it and could be improved. Though, it would probably be simpler to have a stdlib2 but for the reasons mentioned above it would require a work just to agree and understand what should be in the stdlib
Thank you, I was unfamiliar with the Coq Platform, it seems like exactly what I want.
On motivation, more first-class libraries means that a user has to spend less time+effort researching the available representations, weighing their pros and cons, considering whether the repo will remain maintained over time, etc.
Right now, if I want FFI between Coq and OCaml, my options are either to downgrade from 8.19 and use one of many libraries that haven’t had an update in at least a few months, or to manually write the axiom/header file. This seems like something that should be included in the default Extraction library, but instead I have to decide between many libraries that have different features and support. This same issue is echoed in each item of the list of wants I wrote above.
I’m not saying we shouldn’t have extra third-party libraries for things stdlib has - this flexibility is crucial for edge cases, but to have some default functionality ready out-of-the-box would make Coq vastly more usable for programmers, not just researchers.
This all makes sense. How would a big change, such as moving stdlib to its own repository, be decided among the community? Are there votes among active maintainers? Is it an open forum, after which one person makes a decision?
Big decision are discussed through Coq Enhancement Proposal GitHub - coq/ceps: Coq Enhancement Proposals during Coq Calls every Tuesday or so, and during the different Coq workshops for the devs etc…
It is always a bit of an issue, but unless you are requiring new features or developing a library you rarely need to work with the upstream, and there is a release basically every 6 months of Coq and the platform, so it is easy to stay up to date.
Note also that you do not need to work with the version of the coq platform. You can use opam directly to get the latest version or work with the upstream if needed. It is not as easy as using the platform but it is not hard either. After all the platform is here to help users not devs, so it is normal to use opam in this case.