From 48385b78d435e1c6204e5c84ce93a199f1d614da Mon Sep 17 00:00:00 2001
From: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Date: Sat, 13 Jun 2020 21:45:57 -0400
Subject: [PATCH] add info about authorship, recommend putting imports on their
 own lines

---
 templates/contribute/doc.md   | 11 +++++++----
 templates/contribute/style.md | 17 ++++++++++++-----
 2 files changed, 19 insertions(+), 9 deletions(-)

diff --git a/templates/contribute/doc.md b/templates/contribute/doc.md
index 68c2022f53..8f1971e023 100644
--- a/templates/contribute/doc.md
+++ b/templates/contribute/doc.md
@@ -10,8 +10,8 @@ using the [Lean doc preview page](https://observablehq.com/@bryangingechen/githu
 ## Header comment
 
 Each mathlib file should start with:
-* a header comment with copyright information;
-* the list of imports;
+* a header comment with copyright information (see the [recommendations in our style guidelines](style.html#header-and-imports));
+* the list of imports (one on each line);
 * a module docstring containing general documentation, written using Markdown.
 
 (See the example below.)
@@ -43,8 +43,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Y. Lewis
 -/
 
-import data.rat algebra.gcd_domain algebra.field_power
-import ring_theory.multiplicity tactic.ring
+import data.rat
+import algebra.gcd_domain
+import algebra.field_power
+import ring_theory.multiplicity
+import tactic.ring
 import data.real.cau_seq
 import tactic.norm_cast
 
diff --git a/templates/contribute/style.md b/templates/contribute/style.md
index c2b82b35ab..4c4d7103aa 100644
--- a/templates/contribute/style.md
+++ b/templates/contribute/style.md
@@ -30,9 +30,10 @@ easier to read, especially on a small screen or in a small window.
 ### Header and imports ###
 
 The file header should contain copyright information, a list of all
-the authors who have worked on the file, and a description of the
-contents. Do all `import`s right after the header, without a line
-break. You can also open namespaces in the same block.
+the authors who have made significant contributions to the file, and
+a description of the contents. Do all `import`s right after the header,
+without a line break, on separate lines. You can also open namespaces
+in the same block.
 
 ```lean
 /-
@@ -41,13 +42,19 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Joe Cool.
 -/
 
-import data.nat algebra.group
+import data.nat
+import algebra.group
 open nat eq.ops
 ```
 
 (Tip: If you're editing mathlib in VS Code, you can write `copy`
 and then press <kbd>TAB</kbd> to generate a skeleton of the copyright header.)
 
+Regarding the list of authors: we don't have strict rules on what
+contributions qualify for inclusion there. The general idea is that
+the people listed there should be the ones we would reach out to if we had
+questions about the design or development of the Lean code.
+
 ### Module docstrings
 
 After the copyright header and the imports,
@@ -59,7 +66,7 @@ please add a module docstring containing
 - references to the literature (if any)
 
 In total, the module docstring should look something like this:
-```
+```markdown
 # Foos and bars
 
 In this file we introduce `foo` and `bar`,