move everything contribution-related to CONTRIBUTING.md, and link to it from README

CONTRIBUTING.md

@@ -5,12 +5,47 @@ Discussion about the Iris Coq development happens on the mailing list
 in the [Iris Chat](https://mattermost.mpi-sws.org/iris).  This is also the right
 place to ask questions.  The chat requires an account at the
 [MPI-SWS GitLab](https://gitlab.mpi-sws.org/users/sign_in) (use the "Register"
-tab).
-
-If you want to report a bug, please use the
+tab).  If you want to report a bug, please use the
 [issue tracker](https://gitlab.mpi-sws.org/FP/iris-coq/issues), which also
-requires an MPI-SWS GitLab account.  To contribute code, please send your
-MPI-SWS GitLab username to [Ralf Jung](https://gitlab.mpi-sws.org/jung) to
-enable personal projects for your account.  Then you can fork the
+requires an MPI-SWS GitLab account.
+
+Below, you can find some useful resources and an FAQ.
+
+* Information on how to set up your editor for unicode input and output is
+  collected in [Editor.md](Editor.md).
+* The Iris Proof Mode (IPM) / MoSeL is documented at [ProofMode.md](ProofMode.md).
+* Naming conventions are documented at [Naming.md](Naming.md).
+
+## How to submit a pull request
+
+To contribute code, please send your MPI-SWS GitLab username to
+[Ralf Jung](https://gitlab.mpi-sws.org/jung) to enable personal projects for
+your account.  Then you can fork the
 [Iris git repository](https://gitlab.mpi-sws.org/FP/iris-coq/), make your
-changes in your fork, and create a merge request.
+changes in your fork, and create a merge request.  Please do *not* use the
+master branch of your fork, that might confuse CI.  Use a feature branch
+instead.
+
+## How to update the std++ dependency
+
+* Do the change in std++, push it.
+* Wait for CI to publish a new std++ version on the opam archive, then run
+  `opam update iris-dev`.
+* In Iris, change the `opam` file to depend on the new version.
+* Run `make build-dep` (in Iris) to install the new version of std++.
+  You may have to do `make clean` as Coq will likely complain about .vo file
+  mismatches.
+
+## How to write/update test cases
+
+The files in `tests/` are test cases.  Each of the `.v` files comes with a
+matching `.ref` file containing the expected output of `coqc`.  Adding `Show.`
+in selected places in the proofs makes `coqc` print the current goal state.
+This is used to make sure the proof mode prints goals and reduces terms the way
+we expect it to.  You can run `MAKE_REF=1 make` to re-generate all the `.ref` files;
+this is useful after adding or removing `Show.` from a test.  If you do this,
+make sure to check the diff for any unexpected changes in the output!
+
+Some test cases have per-Coq-version `.ref` files (e.g., `atomic.8.8.ref` is a
+Coq-8.8-specific `.ref` file).  If you change one of these, remember to update
+*all* the `.ref` files.

README.md

@@ -108,33 +108,6 @@ that should be compatible with this version:
 * [Iris Atomic](https://gitlab.mpi-sws.org/FP/iris-atomic/) is an experimental
   formalization of logically atomic triples in Iris.
 
-## Notes for Iris Developers
-
-* Information on how to set up your editor for unicode input and output is
-  collected in [Editor.md](Editor.md).
-* The Iris Proof Mode (IPM) / MoSeL is documented at [ProofMode.md](ProofMode.md).
-* Naming conventions are documented at [Naming.md](Naming.md).
-
-### How to update the std++ dependency
-
-* Do the change in std++, push it.
-* Wait for CI to publish a new std++ version on the opam archive, then run
-  `opam update iris-dev`.
-* In Iris, change the `opam` file to depend on the new version.
-* Run `make build-dep` (in Iris) to install the new version of std++.
-  You may have to do `make clean` as Coq will likely complain about .vo file
-  mismatches.
-
-### How to write/update test cases
-
-The files in `tests/` are test cases.  Each of the `.v` files comes with a
-matching `.ref` file containing the expected output of `coqc`.  Adding `Show.`
-in selected places in the proofs makes `coqc` print the current goal state.
-This is used to make sure the proof mode prints goals and reduces terms the way
-we expect it to.  You can run `MAKE_REF=1 make` to re-generate all the `.ref` files;
-this is useful after adding or removing `Show.` from a test.  If you do this,
-make sure to check the diff for any unexpected changes in the output!
-
-Some test cases have per-Coq-version `.ref` files (e.g., `atomic.8.8.ref` is a
-Coq-8.8-specific `.ref` file).  If you change one of these, remember to update
-*all* the `.ref` files.
+## Notes for Iris Contributors
+
+See the [contribution guide](CONTRIBUTING.md).