Stream: Coq users

Topic: Contributing to stdlib


view this post on Zulip Andrej Dudenhefner (Mar 18 2021 at 09:02):

Say there are a couple of List lemmas that are missing from the stdlib, and I would like to contribute those. The contributing documentation is somewhat sketchy on the details. For example, do I need to compile the master branch for this? Does the refactoring 12567 change/simplify the workflow?

view this post on Zulip Enrico Tassi (Mar 18 2021 at 12:46):

Yes, you have to submit your patch against master, but if you have troubles compiling the sources of Coq it may not be needed (you can use Coq 8.13 to prepare your lemmas on Lists, and let CI check they also compile against master, which is very likely, when you open the pull request).

That refactory is not moving the stdlib away, it's about the opam packaging.


Last updated: Jan 28 2023 at 05:02 UTC