doc: contribution guidelines & README update

.github/CONTRIBUTING.md

@@ -1,34 +0,0 @@
-# Contributing to Lean
-
-Thank you for choosing to contribute to Lean. This document is intended as a brief guide
-for new contributors to help streamline the process and make it as easy as possible
-for you (the contributors) and us (the maintainers).
-
-### Writing Code
-
-- [Coding Style](../doc/coding_style.md)
-- [Library Style Conventions](../doc/lean/library_style.org)
-- [Git Commit Conventions](../doc/commit_convention.md)
-- [Automatic Builds](../doc/make/travis.md)
-
-# Opening Issues
-
--  Checked that your issue isn't [already filed](https://github.com/leanprover/lean/issues).
-- Specifically look over:
-  * the [wishlist](https://github.com/leanprover/lean/issues?q=is%3Aissue+is%3Aopen+label%3AI-wishlist),
-  * open [RFCs](https://github.com/leanprover/lean/issues?q=is%3Aissue+is%3Aopen+label%3ARFC),
-  * open [feature requests](https://github.com/leanprover/lean/issues?q=is%3Aissue+is%3Aopen+label%3AFeature).
-- Reduce the issue to a self-contained, reproducible test case.
-
-# Opening Pull Requests
-
-The core developers have to maintain Lean. Thus, they need to read all PRs, and make sure they can maintain them.
-So, here are some guidelines for submitting PRs:
-- Small bug fixes are always welcome.
-- Before implementing a major feature or refactoring the code, please ask whether the change is welcome or not.
-  The worst kind of PR is the "unwanted one". That is, we don’t want it, but we have to explain why we will not merge it.
-- Ensure all tests work before submitting a PR. You can run the test suite (after building Lean and the Lean library) by calling `ctest` in your build directory.
-- Ensure your Pull Request meets the coding and commit conventions documented above.
-- Ensure your Pull Request contains tests for the behavior, for both features or
-  bug fixes.
-- If you are not proficient in C++, do not submit PRs with C++ code.

.github/ISSUE_TEMPLATE.md

@@ -1,9 +1,7 @@
 ### Prerequisites
 
 * [ ] Put an X between the brackets on this line if you have done all of the following:
-    * Checked that your issue isn't already [filed](https://github.com/leanprover/lean/issues).
-        * Specifically, check out the [wishlist](https://github.com/leanprover/lean/issues?q=is%3Aissue+is%3Aopen+label%3AI-wishlist), open [RFCs](https://github.com/leanprover/lean/issues?q=is%3Aissue+is%3Aopen+label%3ARFC),
-        or [feature requests](https://github.com/leanprover/lean/issues?q=is%3Aissue+is%3Aopen+label%3AFeature).
+    * Checked that your issue isn't already [filed](https://github.com/leanprover/lean4/issues).
     * Reduced the issue to a self-contained, reproducible test case.
 
 ### Description

.github/PULL_REQUEST_TEMPLATE.md

@@ -1,7 +0,0 @@
-# Pull Request Description
-
-Ensure you have read the contribution guide before filling in a description of the
-pull request, regardless of whether it is complete or a work in progress.
-All Pull Requests should include test case(s) which demonstrates the intended
-behavior of a feature, or a regression test demonstrating that the fix resolves
-the issue.

CONTRIBUTING.md

@@ -0,0 +1,15 @@
+# Contribution Guidelines
+
+## What to Contribute
+
+* **Bug reports** as new issues are always welcome, but nitpicking issues are not (e.g., the error message is confusing). Please check the existing issues first. Reduce the issue to a self-contained, reproducible test case.
+* Simple fixes for **typos and clear bugs** are welcome if they don't increase maintenance.
+* Extensions to **docs & docstrings** are welcome if you are relatively sure about their correctness; if you need to guess, it can often take longer to correct the content than for us to write it ourselves.
+* Other PRs regarding **non-trivial features** are **not welcome** without prior communication. We don't want to waste your time by you implementing a feature and then us not being able to merge it because of the reasons mentioned in [Should I use Lean?](https://leanprover.github.io/lean4/doc/faq.html). If you have an idea for a feature that is clearly in line with Lean's direction and want to implement it, please open an issue for it first. If you are not sure about compatibility with our plans, the `#lean4` channel on Zulip is a good way to gauge initial interest & feasibility. In either case, be prepared for us not to respond or to reject the proposal with only a brief comment.
+
+## How to Contribute
+
+* Always follow the [commit convention](https://leanprover.github.io/lean4/doc/commit_convention.html).
+* Follow the style of the surrounding code. When in doubt, look at other files using the particular syntax as well.
+* New features or bug fixes should come with appropriate tests.
+* Ensure all tests work before submitting a PR; see [Development Setup](https://leanprover.github.io/lean4/doc/make/index.html#development-setup) and [Fixing Tests](https://leanprover.github.io/lean4/doc/fixing_tests.html).

README.md

@@ -1,9 +1,20 @@
-We are currently developing Lean 4. The [Lean 4 manual](https://leanprover.github.io/lean4/doc/) (work in progress) will give you an overview of the language.
+This is the repository for **Lean 4**, which is currently being released as milestone releases towards a first stable release.
+[Lean 3](https://github.com/leanprover/lean) is still the latest stable release.
 
-[Lean 3](https://github.com/leanprover/lean) is still the latest official release.
-This repository contains work in progress.
+# About
 
-**Important**. Unless you are one of our collaborators
-- We strongly suggest you use Lean 3.
-- Pull requests are not welcome.
-- New issues are not welcome, and will be closed without any feedback.
+- [Homepage](https://leanprover.github.io)
+- [Manual](https://leanprover.github.io/lean4/doc/)
+- [FAQ](https://leanprover.github.io/lean4/doc/faq.html)
+
+# Installation
+
+See [Setting Up Lean](https://leanprover.github.io/lean4/doc/setup.html).
+
+# Contributing
+
+Please read our [Contribution Guidelines](CONTRIBUTING.md) first.
+
+# Building from Source
+
+See [Building Lean](https://leanprover.github.io/lean4/doc/make/index.html).