From 315f417e1338473d4d1ff13f49bb0e44c5049544 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 13 Feb 2019 17:46:18 +0100 Subject: Refresh contributing guide. --- CONTRIBUTING.md | 128 ++++++++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 97 insertions(+), 31 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index bb0e388cdd..3a8d469a05 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -1,29 +1,60 @@ # Contributing to Coq -Thank you for your interest in contributing to Coq! There are many ways to contribute, and we appreciate all of them. +Thank you for your interest in contributing to Coq! There are many ways to +contribute, and we appreciate all of them. ## Bug Reports -Bug reports are enormously useful to identify issues with Coq; we can't fix what we don't know about. To report a bug, please open an issue in the [Coq issue tracker](https://github.com/coq/coq/issues) (you'll need a GitHub account). You can file a bug for any of the following: - -- An anomaly. These are always considered bugs, so Coq will even ask you to file a bug report! -- An error you didn't expect. If you're not sure whether it's a bug or intentional, feel free to file a bug anyway. We may want to improve the documentation or error message. -- Missing documentation. It's helpful to track where the documentation should be improved, so please file a bug if you can't find or don't understand some bit of documentation. -- An error message that wasn't as helpful as you'd like. Bonus points for suggesting what information would have helped you. -- Bugs in CoqIDE should also be filed in the [Coq issue tracker](https://github.com/coq/coq/issues). Bugs in the Emacs plugin should be filed against [ProofGeneral](https://github.com/ProofGeneral/PG/issues), or against [company-coq](https://github.com/cpitclaudel/company-coq/issues) if they are specific to company-coq features. - -It would help if you search the existing issues before reporting a bug. This can be difficult, so consider it extra credit. We don't mind duplicate bug reports. - -When it applies, it's extremely helpful for bug reports to include sample code, and much better if the code is self-contained and complete. It's not necessary to minimize your bug or identify precisely where the issue is, since someone else can often do this if you include a complete example. We tend to include the code in the bug description itself, but if you have a very large input file then you can add it as an attachment. - -If you want to minimize your bug (or help minimize someone else's) for more extra credit, then you can use the [Coq bug minimizer](https://github.com/JasonGross/coq-tools) (specifically, the bug minimizer is the `find-bug.py` script in that repo). +Bug reports are enormously useful to identify issues with Coq; we can't fix +what we don't know about. To report a bug, please open an issue in the +[Coq issue tracker](https://github.com/coq/coq/issues) (you'll need a GitHub +account). You can file a bug for any of the following: + +- An anomaly. These are always considered bugs, so Coq will even ask you to + file a bug report! +- An error you didn't expect. If you're not sure whether it's a bug or + intentional, feel free to file a bug anyway. We may want to improve the + documentation or error message. +- Missing documentation. It's helpful to track where the documentation should + be improved, so please file a bug if you can't find or don't understand some + bit of documentation. +- An error message that wasn't as helpful as you'd like. Bonus points for + suggesting what information would have helped you. +- Bugs in CoqIDE should also be filed in the + [Coq issue tracker](https://github.com/coq/coq/issues). + Bugs in the Emacs plugin should be filed against + [ProofGeneral](https://github.com/ProofGeneral/PG/issues), or against + [company-coq](https://github.com/cpitclaudel/company-coq/issues) if they are + specific to company-coq features. + +It would help if you search the existing issues before reporting a bug. This +can be difficult, so consider it extra credit. We don't mind duplicate bug +reports. + +When it applies, it's extremely helpful for bug reports to include sample +code, and much better if the code is self-contained and complete. It's not +necessary to minimize your bug or identify precisely where the issue is, +since someone else can often do this if you include a complete example. We +tend to include the code in the bug description itself, but if you have a +very large input file then you can add it as an attachment. + +If you want to minimize your bug (or help minimize someone else's) for more +extra credit, then you can use the +[Coq bug minimizer](https://github.com/JasonGross/coq-tools) (specifically, +the bug minimizer is the `find-bug.py` script in that repo). ## Pull requests **Beginner's guide to hacking Coq: [`dev/doc/README.md`](dev/doc/README.md)** \ **Development information and tools: [`dev/README.md`](dev/README.md)** -If you want to contribute a bug fix or feature yourself, pull requests on the [GitHub repository](https://github.com/coq/coq) are the way to contribute directly to the Coq implementation. We recommend you create a fork of the repository on GitHub and push your changes to a new "topic branch" in that fork. From there you can follow the [GitHub pull request documentation](https://help.github.com/articles/about-pull-requests/) to get your changes reviewed and pulled into the Coq source repository. +If you want to contribute a bug fix or feature yourself, pull requests on +the [GitHub repository](https://github.com/coq/coq) are the way to contribute +directly to the Coq implementation. We recommend you create a fork of the +repository on GitHub and push your changes to a new "topic branch" in that +fork. From there you can follow the +[GitHub pull request documentation](https://help.github.com/articles/about-pull-requests/) +to get your changes reviewed and pulled into the Coq source repository. Documentation for getting started with the Coq sources is located in various files in [`dev/doc`](dev/doc) (for example, [debugging.md](dev/doc/debugging.md)). @@ -41,10 +72,10 @@ get one—, and the year of your contribution). It's helpful to run the Coq test suite with `make test-suite` before submitting your change. Our CI runs this test suite and lots of other tests, including -building external Coq developments, on every pull request, but these results +building external Coq projects, on every pull request, but these results take significantly longer to come back (on the order of a few hours). Running the test suite locally will take somewhere around 10-15 minutes. Refer to -[`dev/ci/README.md`](dev/ci/README.md#information-for-developers) for more +[`dev/ci/README-developers.md`](dev/ci/README-developers.md) for more information on CI tests, including how to run them on your private branches. If your pull request fixes a bug, please consider adding a regression test as @@ -53,19 +84,30 @@ well. See [`test-suite/README.md`](test-suite/README.md) for how to do so. If your pull request fixes a critical bug (a bug allowing a proof of `False`), please add an entry to [`dev/doc/critical-bugs`](/dev/doc/critical-bugs). -Don't be alarmed if the pull request process takes some time. It can take a few days to get feedback, approval on the final changes, and then a merge. Coq doesn't release new versions very frequently so it can take a few months for your change to land in a released version. That said, you can start using the latest Coq `master` branch to take advantage of all the new features, improvements, and fixes. +Don't be alarmed if the pull request process takes some time. It can take a +few days to get feedback, approval on the final changes, and then a merge. +Do not hesitate to ping the reviewers if it takes longer than this. +Coq doesn't release new versions very frequently so it can take a few months +for your change to land in a released version. That said, you can start using +the latest Coq `master` branch to take advantage of all the new features, +improvements, and fixes. -Whitespace discipline (do not indent using tabs, no trailing spaces, text files end with newlines) is checked by the `lint` job on GitLab CI (using `git diff --check`). We ship a [`dev/tools/pre-commit`](/dev/tools/pre-commit) git hook which fixes these errors at commit time. `configure` automatically sets you up to use it, unless you already have a hook at `.git/hooks/pre-commit`. +Whitespace discipline (do not indent using tabs, no trailing spaces, text +files end with newlines) is checked by the `lint` job on GitLab CI (using +`git diff --check`). We ship a [`dev/tools/pre-commit`](/dev/tools/pre-commit) +git hook which fixes these errors at commit time. `configure` automatically +sets you up to use it, unless you already have a hook at `.git/hooks/pre-commit`. -Here are a few tags Coq developers may add to your PR and what they mean. In general feedback and requests for you as the pull request author will be in the comments and tags are only used to organize pull requests. +Here are a few tags Coq developers may add to your PR and what they mean. In +general feedback and requests for you as the pull request author will be in +the comments and tags are only used to organize pull requests. - [needs: rebase][rebase-label] indicates the PR should be rebased on top of the latest base branch (usually `master`). See the [GitHub documentation](https://help.github.com/articles/about-git-rebase/) for a brief introduction to using `git rebase`. - This label will be automatically added if you open or synchronize your PR and - it is not up-to-date with the base branch. So please, do not forget to rebase - your branch every time you update it. + We generally ask you to rebase only when there are merge conflicts or if + the PR has been opened for a long time and we want a fresh CI run. - [needs: fixing][fixing-label] indicates the PR needs a fix, as discussed in the comments. - [needs: benchmarking][benchmarking-label] and [needs: testing][testing-label] indicate the PR needs testing beyond what the test suite can handle. @@ -78,13 +120,28 @@ To learn more about the merging process, you can read the ## Documentation -Currently the process for contributing to the documentation is the same as for changing anything else in Coq, so please submit a pull request as described above. +Currently the process for contributing to the documentation is the same as +for changing anything else in Coq, so please submit a pull request as +described above. + +Our issue tracker includes a flag to mark bugs related to documentation. +You can view a list of documentation-related bugs using a +[GitHub issue search](https://github.com/coq/coq/issues?q=is%3Aopen+is%3Aissue+label%3A%22kind%3A+documentation%22). +Many of these bugs can be fixed by contributing writing, without knowledge +of Coq's OCaml source code. -Our issue tracker includes a flag to mark bugs related to documentation. You can view a list of documentation-related bugs using a [GitHub issue search](https://github.com/coq/coq/issues?q=is%3Aopen+is%3Aissue+label%3A%22kind%3A+documentation%22). Many of these bugs can be fixed by contributing writing, without knowledge of Coq's OCaml source code. +The sources for the [Coq reference manual](https://coq.inria.fr/distrib/current/refman/) +are at [`doc/sphinx`](/doc/sphinx). These are written in reStructuredText +and compiled to HTML and PDF with [Sphinx](http://www.sphinx-doc.org/). -The sources for the [Coq reference manual](https://coq.inria.fr/distrib/current/refman/) are at [`doc/sphinx`](/doc/sphinx). These are written in reStructuredText and compiled to HTML and PDF with [Sphinx](http://www.sphinx-doc.org/). +You will find information on how to build the documentation in +[`doc/README.md`](doc/README.md) and information about the specificities of +the Coq Sphinx format in [`doc/sphinx/README.rst`](doc/sphinx/README.rst). -You may also contribute to the informal documentation available in [Cocorico](https://github.com/coq/coq/wiki) (the Coq wiki), and the [Coq FAQ](https://github.com/coq/coq/wiki/The-Coq-FAQ). Both of these are editable by anyone with a GitHub account. +You may also contribute to the informal documentation available in +[Cocorico](https://github.com/coq/coq/wiki) (the Coq wiki), and the +[Coq FAQ](https://github.com/coq/coq/wiki/The-Coq-FAQ). Both of these are +editable by anyone with a GitHub account. ## Following the development @@ -102,13 +159,22 @@ GitHub web notifications using a tool such as [Octobox](http://octobox.io/). ## Contributing outside this repository -There are many useful ways to contribute to the Coq ecosystem that don't involve the Coq repository. +There are many useful ways to contribute to the Coq ecosystem that don't +involve the Coq repository. -Tutorials to teach Coq, and especially to teach particular advanced features, would be much appreciated. Some tutorials are listed on the [Coq website](https://coq.inria.fr/documentation). If you would like to add a link to this list, please make a pull request against the Coq website repository at https://github.com/coq/www. +Tutorials to teach Coq, and especially to teach particular advanced features, +are much appreciated. Some tutorials are listed on the +[Coq website](https://coq.inria.fr/documentation). If you would like to add +a link to this list, please make a pull request against the Coq website +repository at . -External plugins / libraries contribute to create a successful ecosystem around Coq. If your external development is mature enough, you may consider submitting it for addition to our CI tests. Refer to [`dev/ci/README.md`](/dev/ci/README.md) for more information. +External plugins / libraries contribute to create a successful ecosystem +around Coq. If your external development is mature enough, you may consider +submitting it for addition to our CI tests. Refer to +[`dev/ci/README-users.md`](dev/ci/README-users.md) for more information. -Ask and answer questions on [Stack Exchange](https://stackexchange.com/filters/299857/questions-tagged-coq-on-stackexchange-sites) which has a helpful community of Coq users. +Ask and answer questions on [Stack Exchange](https://stackexchange.com/filters/299857/questions-tagged-coq-on-stackexchange-sites) +which has a helpful community of Coq users. Hang out on the Coq IRC channel, `irc://irc.freenode.net/#coq`, and help answer questions. -- cgit v1.2.3 From fe3def270fd0f601cdccfa4c5f443cee028c3f03 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 13 Feb 2019 17:49:49 +0100 Subject: Document how to add people to the contributors team. --- CONTRIBUTING.md | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 3a8d469a05..cc3af05845 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -43,6 +43,13 @@ extra credit, then you can use the [Coq bug minimizer](https://github.com/JasonGross/coq-tools) (specifically, the bug minimizer is the `find-bug.py` script in that repo). +### Triaging bug reports + +Triaging bug reports (adding labels, closing outdated / resolved bugs) +requires to be granted some permissions. You may request members of the +**@coq/core** team to add you to the contributors team. They can do so using +this link: . + ## Pull requests **Beginner's guide to hacking Coq: [`dev/doc/README.md`](dev/doc/README.md)** \ -- cgit v1.2.3 From 370b66eb8698ec7c2ebee985a5ec807271171c9f Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 13 Feb 2019 17:54:35 +0100 Subject: Mention coq-community in the contributing guide. --- CONTRIBUTING.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index cc3af05845..9af4e10a38 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -180,6 +180,14 @@ around Coq. If your external development is mature enough, you may consider submitting it for addition to our CI tests. Refer to [`dev/ci/README-users.md`](dev/ci/README-users.md) for more information. +Some Coq packages are not maintained by their authors anymore even if they +were useful (for instance because they changed jobs). The coq-community +organization is a place for people to take over the maintenance of such +useful packages. If you want to contribute by becoming a maintainer, you can +find a list of packages waiting for a maintainer [here](https://github.com/coq-community/manifesto/issues?q=is%3Aissue+is%3Aopen+label%3Amaintainer-wanted). +You can also propose a package that is not listed. Find out more about +coq-community in [the manifesto's README](https://github.com/coq-community/manifesto). + Ask and answer questions on [Stack Exchange](https://stackexchange.com/filters/299857/questions-tagged-coq-on-stackexchange-sites) which has a helpful community of Coq users. -- cgit v1.2.3 From 6d71db62424b942991d967dfaced75fb886fa2d8 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 13 Feb 2019 21:03:11 +0100 Subject: Advertise code of conduct in contributing guide. --- CONTRIBUTING.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 9af4e10a38..7ce1817fc1 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -1,7 +1,8 @@ # Contributing to Coq Thank you for your interest in contributing to Coq! There are many ways to -contribute, and we appreciate all of them. +contribute, and we appreciate all of them. Please make sure you read and +abide by the [Code of Conduct](CODE_OF_CONDUCT.md). ## Bug Reports -- cgit v1.2.3 From e83f3121c07f3f942410fdf4123a8aa017c9a007 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 13 Feb 2019 21:07:35 +0100 Subject: Suggest asking on Discourse or Gitter. Co-authored-by: Emilio Jesus Gallego Arias --- CONTRIBUTING.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 7ce1817fc1..ce211be897 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -30,7 +30,8 @@ account). You can file a bug for any of the following: It would help if you search the existing issues before reporting a bug. This can be difficult, so consider it extra credit. We don't mind duplicate bug -reports. +reports. If unsure, you are always very welcome to ask on Discourse or Gitter +before, after, or while writting a bug report When it applies, it's extremely helpful for bug reports to include sample code, and much better if the code is self-contained and complete. It's not -- cgit v1.2.3 From 2533f5ca0eea4ceb7d1cae3b91be3be2eb525ede Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 13 Feb 2019 21:40:17 +0100 Subject: Mention Discourse in contributing guide. --- CONTRIBUTING.md | 33 +++++++++++++++++++++------------ 1 file changed, 21 insertions(+), 12 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index ce211be897..05f01e4a97 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -67,8 +67,6 @@ to get your changes reviewed and pulled into the Coq source repository. Documentation for getting started with the Coq sources is located in various files in [`dev/doc`](dev/doc) (for example, [debugging.md](dev/doc/debugging.md)). -For further help with the Coq sources, feel free to join -the [Coq Gitter chat](https://gitter.im/coq/coq) and ask questions. Please make pull requests against the `master` branch. @@ -127,6 +125,13 @@ the comments and tags are only used to organize pull requests. To learn more about the merging process, you can read the [merging documentation for Coq maintainers](dev/doc/MERGING.md). +[rebase-label]: https://github.com/coq/coq/pulls?utf8=%E2%9C%93&q=is%3Aopen%20is%3Apr%20label%3A%22needs%3A%20rebase%22 +[fixing-label]: https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+fixing%22 +[benchmarking-label]: https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+benchmarking%22 +[testing-label]: https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+testing%22 + +[jenkins-doc]: https://github.com/coq/coq/wiki/Jenkins-(automated-benchmarking) + ## Documentation Currently the process for contributing to the documentation is the same as @@ -152,6 +157,15 @@ You may also contribute to the informal documentation available in [Coq FAQ](https://github.com/coq/coq/wiki/The-Coq-FAQ). Both of these are editable by anyone with a GitHub account. +## Where to get help (with the Coq source code, or anything else) + +We have a Discourse forum (see in particular the [Coq development category][]) +and a [Gitter chat][]. Feel free to join any of them and ask questions. +People are generally happy to help and very reactive. + +[Coq development category]: https://coq.discourse.group/c/coq-development +[Gitter chat]: https://gitter.im/coq/coq + ## Following the development If you want to follow the development activity around Coq, you are encouraged @@ -190,14 +204,9 @@ find a list of packages waiting for a maintainer [here](https://github.com/coq-c You can also propose a package that is not listed. Find out more about coq-community in [the manifesto's README](https://github.com/coq-community/manifesto). -Ask and answer questions on [Stack Exchange](https://stackexchange.com/filters/299857/questions-tagged-coq-on-stackexchange-sites) -which has a helpful community of Coq users. - -Hang out on the Coq IRC channel, `irc://irc.freenode.net/#coq`, and help answer questions. - -[rebase-label]: https://github.com/coq/coq/pulls?utf8=%E2%9C%93&q=is%3Aopen%20is%3Apr%20label%3A%22needs%3A%20rebase%22 -[fixing-label]: https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+fixing%22 -[benchmarking-label]: https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+benchmarking%22 -[testing-label]: https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+testing%22 +Ask and answer questions on our [Discourse forum][], on [Stack Exchange][], +and on the [Coq IRC channel][]. -[jenkins-doc]: https://github.com/coq/coq/wiki/Jenkins-(automated-benchmarking) +[Discourse forum]: https://coq.discourse.group/ +[Stack Exchange]: https://stackexchange.com/filters/299857/questions-tagged-coq-on-stackexchange-sites +[Coq IRC channel]: irc://irc.freenode.net/#coq -- cgit v1.2.3 From 0e82d6b1a3006ad260e91c06be9151bfdd406f8e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 16 Feb 2019 19:44:39 +0100 Subject: Fix English grammar. Co-Authored-By: Zimmi48 --- CONTRIBUTING.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 05f01e4a97..ce057677bf 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -48,7 +48,7 @@ the bug minimizer is the `find-bug.py` script in that repo). ### Triaging bug reports Triaging bug reports (adding labels, closing outdated / resolved bugs) -requires to be granted some permissions. You may request members of the +requires you to be granted some permissions. You may request members of the **@coq/core** team to add you to the contributors team. They can do so using this link: . -- cgit v1.2.3 From 355f6eceb666964ad060caf557903d8f82ec1755 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Sat, 16 Feb 2019 20:02:06 +0100 Subject: Add links for all mentions of Gitter and Discourse. Update the part about following the development. Remove the reference to Coqdev. --- CONTRIBUTING.md | 38 ++++++++++++++++++-------------------- 1 file changed, 18 insertions(+), 20 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index ce057677bf..31fa3d2c4a 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -8,7 +8,7 @@ abide by the [Code of Conduct](CODE_OF_CONDUCT.md). Bug reports are enormously useful to identify issues with Coq; we can't fix what we don't know about. To report a bug, please open an issue in the -[Coq issue tracker](https://github.com/coq/coq/issues) (you'll need a GitHub +[Coq issue tracker][] (you'll need a GitHub account). You can file a bug for any of the following: - An anomaly. These are always considered bugs, so Coq will even ask you to @@ -22,7 +22,7 @@ account). You can file a bug for any of the following: - An error message that wasn't as helpful as you'd like. Bonus points for suggesting what information would have helped you. - Bugs in CoqIDE should also be filed in the - [Coq issue tracker](https://github.com/coq/coq/issues). + [Coq issue tracker][]. Bugs in the Emacs plugin should be filed against [ProofGeneral](https://github.com/ProofGeneral/PG/issues), or against [company-coq](https://github.com/cpitclaudel/company-coq/issues) if they are @@ -30,8 +30,8 @@ account). You can file a bug for any of the following: It would help if you search the existing issues before reporting a bug. This can be difficult, so consider it extra credit. We don't mind duplicate bug -reports. If unsure, you are always very welcome to ask on Discourse or Gitter -before, after, or while writting a bug report +reports. If unsure, you are always very welcome to ask on our [Discourse forum][] +or [Gitter chat][] before, after, or while writting a bug report When it applies, it's extremely helpful for bug reports to include sample code, and much better if the code is self-contained and complete. It's not @@ -159,26 +159,23 @@ editable by anyone with a GitHub account. ## Where to get help (with the Coq source code, or anything else) -We have a Discourse forum (see in particular the [Coq development category][]) +We have a [Discourse forum][] (see in particular the [Coq development category][]) and a [Gitter chat][]. Feel free to join any of them and ask questions. People are generally happy to help and very reactive. [Coq development category]: https://coq.discourse.group/c/coq-development -[Gitter chat]: https://gitter.im/coq/coq - -## Following the development -If you want to follow the development activity around Coq, you are encouraged -to subscribe to the [Coqdev mailing list](https://sympa.inria.fr/sympa/info/coqdev). -This mailing list has reasonably low traffic. +## Watching the repository -You may also choose to use GitHub feature to -["watch" this repository](https://github.com/coq/coq/subscription), but be -advised that this means receiving a very large number of notifications. -GitHub gives [some advice](https://blog.github.com/2017-07-18-managing-large-numbers-of-github-notifications/#prioritize-the-notifications-you-receive) -on how to configure your e-mail client to filter these notifications. -A possible alternative is to deactivate e-mail notifications and manage your -GitHub web notifications using a tool such as [Octobox](http://octobox.io/). +["Watching" this repository](https://github.com/coq/coq/subscription) +can result in a very large number of notifications. We advise that if +you do, either [confifure your mailbox](https://blog.github.com/2017-07-18-managing-large-numbers-of-github-notifications/#prioritize-the-notifications-you-receive) +to handle incoming notifications efficiently, or you read your +notifications within a web browser. You can configure how you receive +notifications in [your GitHub settings](https://github.com/settings/notifications), +you can use the GitHub interface to mark as read, save for later or +mute threads. You can also manage your GitHub web notifications using +a tool such as [Octobox](http://octobox.io/). ## Contributing outside this repository @@ -205,8 +202,9 @@ You can also propose a package that is not listed. Find out more about coq-community in [the manifesto's README](https://github.com/coq-community/manifesto). Ask and answer questions on our [Discourse forum][], on [Stack Exchange][], -and on the [Coq IRC channel][]. +and on the Coq IRC channel (`irc://irc.freenode.net/#coq`). +[Coq issue tracker]: https://github.com/coq/coq/issues [Discourse forum]: https://coq.discourse.group/ +[Gitter chat]: https://gitter.im/coq/coq [Stack Exchange]: https://stackexchange.com/filters/299857/questions-tagged-coq-on-stackexchange-sites -[Coq IRC channel]: irc://irc.freenode.net/#coq -- cgit v1.2.3 From c5ea163f16392e230c6791275fc192da9c524dcb Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 28 Feb 2019 15:55:32 +0100 Subject: Refresh README. --- README.md | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/README.md b/README.md index f332bf5db0..ef80736e1a 100644 --- a/README.md +++ b/README.md @@ -68,25 +68,25 @@ and the [Coq FAQ](https://github.com/coq/coq/wiki/The-Coq-FAQ), for additional user-contributed documentation. ## Changes + There is a file named [`CHANGES.md`](CHANGES.md) that explains the differences and the incompatibilities since last versions. If you upgrade Coq, please read it carefully. -## The Coq Club -The Coq Club moderated mailing list is meant to be a standard way -to discuss questions about the Coq system and related topics. The -subscription link can be found at [coq.inria.fr/community](http://coq.inria.fr/community). +## Questions and discussion + +We have a number of channels to reach the user community and the +development team: -The topics to be discussed in the club should include: +- Our [Discourse forum](https://coq.discourse.group). +- Our mailing list, the [Coq-Club](https://sympa.inria.fr/sympa/info/coq-club). +- Our [Gitter channel][gitter-link], which is a good way to reach + developers for quick chat and development questions. -* technical problems; -* questions about proof developments; -* suggestions and questions about the implementation; -* announcements of proofs; -* theoretical questions about typed lambda-calculi which are - closely related to Coq. +See also [coq.inria.fr/community](https://coq.inria.fr/community.html). ## Bugs report + Please report any bug / feature request in [our issue tracker](https://github.com/coq/coq/issues). To be effective, bug reports should mention the OCaml version used -- cgit v1.2.3