diff --git a/doc/dev/commit_convention.md b/doc/dev/commit_convention.md
index 80362c175bec..9793350521a7 100644
--- a/doc/dev/commit_convention.md
+++ b/doc/dev/commit_convention.md
@@ -33,6 +33,9 @@ Format of the commit message
  - chore (maintain, ex: travis-ci)
  - perf (performance improvement, optimization, ...)
 
+Every `feat` or `fix` commit must have a `changelog-*` label, and a commit message
+beginning with "This PR " that will be included in the changelog.
+
 ``<subject>`` has the following constraints:
 
  - use imperative, present tense: "change" not "changed" nor "changes"
@@ -44,6 +47,7 @@ Format of the commit message
  - just as in ``<subject>``, use imperative, present tense
  - includes motivation for the change and contrasts with previous
    behavior
+ - If a `changelog-*` label is present, the body must begin with "This PR ".
 
 ``<footer>`` is optional and may contain two items:
 
@@ -60,17 +64,21 @@ Examples
 
 fix: add declarations for operator<<(std::ostream&, expr const&) and operator<<(std::ostream&, context const&) in the kernel
 
+This PR adds declarations `operator<<` for raw printing.
 The actual implementation of these two operators is outside of the
-kernel. They are implemented in the file 'library/printer.cpp'. We
-declare them in the kernel to prevent the following problem. Suppose
-there is a file 'foo.cpp' that does not include 'library/printer.h',
-but contains
+kernel. They are implemented in the file 'library/printer.cpp'.
 
-    expr a;
-    ...
-    std::cout << a << "\n";
-    ...
+We declare them in the kernel to prevent the following problem.
+Suppose there is a file 'foo.cpp' that does not include 'library/printer.h',
+but contains
+```cpp
+expr a;
+...
+std::cout << a << "\n";
+...
+```
 
 The compiler does not generate an error message. It silently uses the
 operator bool() to coerce the expression into a Boolean. This produces
 counter-intuitive behavior, and may confuse developers.
+
diff --git a/doc/dev/index.md b/doc/dev/index.md
index 999591a85ae5..ea626f23a453 100644
--- a/doc/dev/index.md
+++ b/doc/dev/index.md
@@ -80,3 +80,10 @@ Unlike most Lean projects, all submodules of the `Lean` module begin with the
 `prelude` keyword. This disables the automated import of `Init`, meaning that
 developers need to figure out their own subset of `Init` to import. This is done
 such that changing files in `Init` doesn't force a full rebuild of `Lean`.
+
+### Testing against Mathlib/Batteries
+You can test a Lean PR against Mathlib and Batteries by rebasing your PR
+on to `nightly-with-mathlib` branch. (It is fine to force push after rebasing.)
+CI will generate a branch of Mathlib and Batteries called `lean-pr-testing-NNNN`
+that uses the toolchain for your PR, and will report back to the Lean PR with results from Mathlib CI.
+See https://leanprover-community.github.io/contribute/tags_and_branches.html for more details.