The purpose of this project is to design and implement a new standard library for Coq. It will follow a clean slate approach, not aiming at compatibility with the current library, which will be maintained separately.
This project is coordinated by @maximedenes and can be discussed and followed at: coq/coq#7711 and https://github.com/orgs/coq/projects/1
We foresee several stages:
- Preliminary clean-up and infrastructure work
- Implementation of prelude and basic tactics
- Enhancement of the core of the library.
- First release.
- Implementation of the first components of the library
- Extensions of the library
The project is currently (February 2019) in its second phase (starting the actual implementation).
Questions and discussions are welcome at this stage. In particular, the wiki and issues (as opposed to code reviews) can be used to share and discuss opinions.
External code contribution will be integrated during the last two phases. See the contributing guide.