max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: incorporate feedback

Browse source
This commit is contained in:
Leonardo de Moura 2021-05-13 15:52:31 -07:00
parent 5c101d056a
commit 51c324ce21
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
CONTRIBUTING.md
View file

@ -6,10 +6,8 @@ Thank you for your interest in contributing to Lean! There are many ways to cont
Bug reports as new issues are always welcome. Please check the existing [issues](https://github.com/leanprover/lean4/issues) first.
Reduce the issue to a self-contained, reproducible test case.
If you have the chance, before reporting a bug, please search existing issues, as it's possible that
someone else has already reported your error.
If you're not sure if something is a bug or not, feel free to file a bug anyway. You may also want to discuss it with the Lean
community using the [lean4 Zulip channel](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4).
@ -22,11 +20,13 @@ Simple fixes for **typos and clear bugs** are welcome.
Tutorial-like examples are very welcome.
They are useful for finding rough edges and bugs in Lean 4, for highlighting new features, and for showing how to use Lean.
If you want to store your tutorial in the Lean 4 repository to make sure future changes will not break it, we suggest the following workflow:
* Contact one of the Lean developers in Zulip, and check whether your tutorial is a good match for the Lean 4 repository.
* Contact one of the Lean developers on Zulip, and check whether your tutorial is a good match for the Lean 4 repository.
* Send bug reports and report rough edges. We will work with you until the tutorial looks great.
* Add plenty of comments and make sure others will be able to follow it.
* Create a pull request in the Lean 4 repository. After merging, we will link it to the official documentation and make sure it becomes part of our test suite.
You can use `.lean` or `.md` files to create your tutorial. The `.md` files are ideal when you want to format your prose using markdown. For an example, see [this `.md` file](https://github.com/leanprover/lean4/blob/master/doc/lean3changes.md).
Contributions to the reference manual are also welcome, but since Lean 4 is changing rapidly, please contact us first using Zulip
to find out which parts are stable enough to document. We will work with you to get this kind of
pull request merged. We are also happy to meet using Zoom, Skype or Google hangout to coordinate this kind of effort.
@ -35,16 +35,16 @@ As Lean 4 matures, other forms of documentation (e.g., doc-strings) will be welc
## "Help wanted"
For issues marked as [`help wanted`](https://github.com/leanprover/lean4/issues?q=is%3Aissue+is%3Aopen+label%3A%22help+wanted%22), pull requests (PR) are welcome and we will work with you to get a PR merged. Some of these issues are nontrivial. If you are interested, please consider adding comments to the PR and/or messaging the Lean developers in [Zulip](https://leanprover.zulipchat.com/#).
For issues marked as [`help wanted`](https://github.com/leanprover/lean4/issues?q=is%3Aissue+is%3Aopen+label%3A%22help+wanted%22), pull requests (PR) are welcome and we will work with you to get a PR merged. Some of these issues are nontrivial. If you are interested, please consider adding comments to the issue and/or messaging the Lean developers in [Zulip](https://leanprover.zulipchat.com/#).
## Unexpected Pull Requests
We have very few core developers, and we cannot review arbitrary pull requests (PR).
So, please contact the core developers before investing your time on a nontrivial modification.
We suggest the following workflow:
* Discuss with the Lean community it Zulip whether there is interest.
* Discuss with the Lean community on Zulip what the trade-offs are, whether the community is interested in your feature, and broadly supports it.
* Create an issue on the [Lean 4 repository at GitHub](https://github.com/leanprover/lean4/issues), tag it with RFC.
* Ask the community to help documenting the requirements, collecting examples and concerns.
* Ask the community for help documenting the requirements, and for collecting examples and concerns.
* Wait for one of the core developers to give you a "go ahead". At this point, the core developers will work with you to make sure your PR gets merged.
We don't want to waste your time by you implementing a feature and then us not being able to merge it.