[Merged by Bors] - ci(lint-copy-mod-doc.py): add reserved notation and set_option linters, enable small_alpha_vrachy_check linter

scripts/lint-copy-mod-doc.py

@@ -9,6 +9,8 @@
 ERR_MOD = 2 # module docstring
 ERR_LIN = 3 # line length
 ERR_SAV = 4 # ᾰ
+ERR_RNT = 5 # reserved notation
+ERR_OPT = 6 # set_option
 
 exceptions = []
 
@@ -25,14 +27,79 @@
             exceptions += [(ERR_LIN, fn)]
         if errno == "ERR_SAV":
             exceptions += [(ERR_SAV, fn)]
+        if errno == "ERR_RNT":
+            exceptions += [(ERR_RNT, fn)]
+        if errno == "ERR_OPT":
+            exceptions += [(ERR_OPT, fn)]
 
 new_exceptions = False
 
+def skip_comments(enumerate_lines):
+    in_comment = False
+    for line_nr, line in enumerate_lines:
+        if "/-" in line:
+            in_comment = True
+        if "-/" in line:
+            in_comment = False
+            continue
+        if line == "\n" or in_comment:
+            continue
+        yield line_nr, line
+
+def skip_string(enumerate_lines):
+    in_string = False
+    in_comment = False
+    for line_nr, line in enumerate_lines:
+        # ignore comment markers inside string literals
+        if not in_string:
+            if "/-" in line:
+                in_comment = True
+            if "-/" in line:
+                in_comment = False
+        # ignore quotes inside comments
+        if not in_comment:
+            # crude heuristic: if the number of non-escaped quote signs is odd,
+            # we're starting / ending a string literal
+            if line.count("\"") - line.count("\\\"") % 2 == 1:
+                in_string = not in_string
+            # if there are quote signs in this line,
+            # a string literal probably begins and / or ends here,
+            # so we skip this line
+            if line.count("\"") > 0:
+                continue
+            if in_string:
+                continue
+        yield line_nr, line
+
 def small_alpha_vrachy_check(lines, fn):
-    return [ (ERR_SAV, line_nr, fn) for line_nr, line in enumerate(lines) if 'ᾰ' in line ]
+    errors = []
+    for line_nr, line in skip_string(skip_comments(enumerate(lines, 1))):
+        if 'ᾰ' in line:
+            errors += [(ERR_SAV, line_nr, fn)]
+    return errors
+
+def reserved_notation_check(lines, fn):
+    if fn == 'src/tactic/reserved_notation.lean':
+        return []
+    errors = []
+    for line_nr, line in skip_string(skip_comments(enumerate(lines, 1))):
+        if line.startswith('reserve') or line.startswith('precedence'):
+            errors += [(ERR_RNT, line_nr, fn)]
+    return errors
+
+def set_option_check(lines, fn):
+    errors = []
+    for line_nr, line in skip_string(skip_comments(enumerate(lines, 1))):
+        if line.startswith('set_option'):
+            next_two_chars = line.split(' ')[1][:2]
+            # forbidden options: pp, profiler, trace
+            if next_two_chars == 'pp' or next_two_chars == 'pr' or next_two_chars == 'tr':
+                errors += [(ERR_OPT, line_nr, fn)]
+    return errors
 
 def long_lines_check(lines, fn):
     errors = []
+    # TODO: some string literals (in e.g. tactic output messages) can be excepted from this rule
     for line_nr, line in enumerate(lines, 1):
         if "http" in line:
             continue
@@ -43,15 +110,7 @@ def long_lines_check(lines, fn):
 def import_only_check(lines, fn):
     import_only_file = True
     errors = []
-    in_comment = False
-    for line_nr, line in enumerate(lines, 1):
-        if "/-" in line:
-            in_comment = True
-        if "-/" in line:
-            in_comment = False
-            continue
-        if line == "\n" or in_comment:
-            continue
+    for line_nr, line in skip_comments(enumerate(lines, 1)):
         imports = line.split()
         if imports[0] == "--":
             continue
@@ -121,6 +180,10 @@ def format_errors(errors):
             print("{} : line {} : ERR_LIN : Line has more than 100 characters".format(fn, line_nr))
         if errno == ERR_SAV:
             print("{} : line {} : ERR_SAV : File contains the character ᾰ".format(fn, line_nr))
+        if errno == ERR_RNT:
+            print("{} : line {} : ERR_RNT : Reserved notation outside tactic.core".format(fn, line_nr))
+        if errno == ERR_OPT:
+            print("{} : line {} : ERR_OPT : Forbidden set_option command".format(fn, line_nr))
 
 def lint(fn):
     with open(fn) as f:
@@ -133,6 +196,12 @@ def lint(fn):
             return
         errs = regular_check(lines, fn)
         format_errors(errs)
+        errs = small_alpha_vrachy_check(lines, fn)
+        format_errors(errs)
+        errs = reserved_notation_check(lines, fn)
+        format_errors(errs)
+        errs = set_option_check(lines, fn)
+        format_errors(errs)
 
 for fn in fns:
     lint(fn)

src/algebra/module/linear_map.lean

@@ -303,7 +303,7 @@ end
 attribute [nolint doc_blame] linear_equiv.to_linear_map
 attribute [nolint doc_blame] linear_equiv.to_add_equiv
 
-infix ` ≃ₗ `:25 := linear_equiv _
+infix ` ≃ₗ ` := linear_equiv _
 notation M ` ≃ₗ[`:50 R `] ` M₂ := linear_equiv R M M₂
 
 namespace linear_equiv

src/linear_algebra/basic.lean

@@ -57,8 +57,6 @@ linear algebra, vector space, module
 open function
 open_locale big_operators
 
-reserve infix ` ≃ₗ `:25
-
 universes u v w x y z u' v' w' y'
 variables {R : Type u} {K : Type u'} {M : Type v} {V : Type v'} {M₂ : Type w} {V₂ : Type w'}
 variables {M₃ : Type y} {V₃ : Type y'} {M₄ : Type z} {ι : Type x}
@@ -1517,8 +1515,8 @@ end field
 
 end linear_map
 
-lemma submodule.sup_eq_range [semiring R] [add_comm_monoid M] [semimodule R M] (p q : submodule R M) :
-  p ⊔ q = (p.subtype.coprod q.subtype).range :=
+lemma submodule.sup_eq_range [semiring R] [add_comm_monoid M] [semimodule R M]
+  (p q : submodule R M) : p ⊔ q = (p.subtype.coprod q.subtype).range :=
 submodule.ext $ λ x, by simp [submodule.mem_sup, submodule.exists]
 
 namespace is_linear_map
@@ -1549,7 +1547,8 @@ namespace submodule
 
 section add_comm_monoid
 
-variables {T : semiring R} [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂]
+variables {T : semiring R} [add_comm_monoid M] [add_comm_monoid M₂]
+variables [semimodule R M] [semimodule R M₂]
 variables (p p' : submodule R M) (q : submodule R M₂)
 include T
 open linear_map
@@ -1925,7 +1924,8 @@ end add_comm_monoid
 
 section add_comm_group
 
-variables [semiring R] [add_comm_group M] [add_comm_group M₂] [add_comm_group M₃] [add_comm_group M₄]
+variables [semiring R]
+variables [add_comm_group M] [add_comm_group M₂] [add_comm_group M₃] [add_comm_group M₄]
 variables {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂}
 variables {semimodule_M₃ : semimodule R M₃} {semimodule_M₄ : semimodule R M₄}
 variables (e e₁ : M ≃ₗ[R] M₂) (e₂ : M₃ ≃ₗ[R] M₄)
@@ -2035,21 +2035,24 @@ rfl
 rfl
 
 lemma arrow_congr_comp {N N₂ N₃ : Sort*}
-  [add_comm_group N] [add_comm_group N₂] [add_comm_group N₃] [module R N] [module R N₂] [module R N₃]
+  [add_comm_group N] [add_comm_group N₂] [add_comm_group N₃]
+  [module R N] [module R N₂] [module R N₃]
   (e₁ : M ≃ₗ[R] N) (e₂ : M₂ ≃ₗ[R] N₂) (e₃ : M₃ ≃ₗ[R] N₃) (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) :
   arrow_congr e₁ e₃ (g.comp f) = (arrow_congr e₂ e₃ g).comp (arrow_congr e₁ e₂ f) :=
 by { ext, simp only [symm_apply_apply, arrow_congr_apply, linear_map.comp_apply], }
 
 lemma arrow_congr_trans {M₁ M₂ M₃ N₁ N₂ N₃ : Sort*}
-  [add_comm_group M₁] [module R M₁] [add_comm_group M₂] [module R M₂] [add_comm_group M₃] [module R M₃]
-  [add_comm_group N₁] [module R N₁] [add_comm_group N₂] [module R N₂] [add_comm_group N₃] [module R N₃]
+  [add_comm_group M₁] [module R M₁] [add_comm_group M₂] [module R M₂]
+  [add_comm_group M₃] [module R M₃] [add_comm_group N₁] [module R N₁]
+  [add_comm_group N₂] [module R N₂] [add_comm_group N₃] [module R N₃]
   (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : N₁ ≃ₗ[R] N₂) (e₃ : M₂ ≃ₗ[R] M₃) (e₄ : N₂ ≃ₗ[R] N₃) :
   (arrow_congr e₁ e₂).trans (arrow_congr e₃ e₄) = arrow_congr (e₁.trans e₃) (e₂.trans e₄) :=
 rfl
 
 /-- If `M₂` and `M₃` are linearly isomorphic then the two spaces of linear maps from `M` into `M₂`
 and `M` into `M₃` are linearly isomorphic. -/
-def congr_right (f : M₂ ≃ₗ[R] M₃) : (M →ₗ[R] M₂) ≃ₗ (M →ₗ M₃) := arrow_congr (linear_equiv.refl R M) f
+def congr_right (f : M₂ ≃ₗ[R] M₃) : (M →ₗ[R] M₂) ≃ₗ (M →ₗ M₃) :=
+arrow_congr (linear_equiv.refl R M) f
 
 /-- If `M` and `M₂` are linearly isomorphic then the two spaces of linear maps from `M` and `M₂` to
 themselves are linearly isomorphic. -/
@@ -2107,7 +2110,8 @@ end
 def to_span_nonzero_singleton (x : M) (h : x ≠ 0) : K ≃ₗ[K] (submodule.span K ({x} : set M)) :=
 linear_equiv.trans
   (linear_equiv.of_injective (to_span_singleton K M x) (ker_to_span_singleton K M h))
-  (of_eq (to_span_singleton K M x).range (submodule.span K {x}) (span_singleton_eq_range K M x).symm)
+  (of_eq (to_span_singleton K M x).range (submodule.span K {x})
+    (span_singleton_eq_range K M x).symm)
 
 lemma to_span_nonzero_singleton_one (x : M) (h : x ≠ 0) : to_span_nonzero_singleton K M x h 1
   = (⟨x, submodule.mem_span_singleton_self x⟩ : submodule.span K ({x} : set M)) :=
@@ -2175,7 +2179,8 @@ variables (q : submodule R M)
 /-- Quotienting by equal submodules gives linearly equivalent quotients. -/
 def quot_equiv_of_eq (h : p = q) : p.quotient ≃ₗ[R] q.quotient :=
 { map_add' := by { rintros ⟨x⟩ ⟨y⟩, refl }, map_smul' := by { rintros x ⟨y⟩, refl },
-  ..@quotient.congr _ _ (quotient_rel p) (quotient_rel q) (equiv.refl _) $ λ a b, by { subst h, refl } }
+  ..@quotient.congr _ _ (quotient_rel p) (quotient_rel q) (equiv.refl _) $
+    λ a b, by { subst h, refl } }
 
 end submodule
 

src/logic/basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura
 -/
 import tactic.doc_commands
+import tactic.reserved_notation
 
 /-!
 # Basic logic properties
@@ -498,7 +499,8 @@ by rw [@iff_def a, @iff_def b]; exact and_congr imp_not_comm decidable.not_imp_c
 theorem iff_not_comm : (a ↔ ¬ b) ↔ (b ↔ ¬ a) := decidable.iff_not_comm
 
 -- See Note [decidable namespace]
-protected theorem decidable.iff_iff_and_or_not_and_not [decidable b] : (a ↔ b) ↔ (a ∧ b) ∨ (¬ a ∧ ¬ b) :=
+protected theorem decidable.iff_iff_and_or_not_and_not [decidable b] :
+  (a ↔ b) ↔ (a ∧ b) ∨ (¬ a ∧ ¬ b) :=
 by { split; intro h,
      { rw h; by_cases b; [left,right]; split; assumption },
      { cases h with h h; cases h; split; intro; { contradiction <|> assumption } } }
@@ -575,7 +577,8 @@ by rw [← not_or_distrib, decidable.not_not]
 theorem or_iff_not_and_not : a ∨ b ↔ ¬ (¬a ∧ ¬b) := decidable.or_iff_not_and_not
 
 -- See Note [decidable namespace]
-protected theorem decidable.and_iff_not_or_not [decidable a] [decidable b] : a ∧ b ↔ ¬ (¬ a ∨ ¬ b) :=
+protected theorem decidable.and_iff_not_or_not [decidable a] [decidable b] :
+  a ∧ b ↔ ¬ (¬ a ∨ ¬ b) :=
 by rw [← decidable.not_and_distrib, decidable.not_not]
 
 theorem and_iff_not_or_not : a ∧ b ↔ ¬ (¬ a ∨ ¬ b) := decidable.and_iff_not_or_not
@@ -875,7 +878,8 @@ theorem Exists.snd {p : b → Prop} : ∀ h : Exists p, p h.fst
 @[simp] theorem exists_prop_of_true {p : Prop} {q : p → Prop} (h : p) : (∃ h' : p, q h') ↔ q h :=
 @exists_const (q h) p ⟨h⟩
 
-@[simp] theorem forall_prop_of_false {p : Prop} {q : p → Prop} (hn : ¬ p) : (∀ h' : p, q h') ↔ true :=
+@[simp] theorem forall_prop_of_false {p : Prop} {q : p → Prop} (hn : ¬ p) :
+  (∀ h' : p, q h') ↔ true :=
 iff_true_intro $ λ h, hn.elim h
 
 @[simp] theorem exists_prop_of_false {p : Prop} {q : p → Prop} : ¬ p → ¬ (∃ h' : p, q h') :=

src/logic/relator.lean

@@ -6,11 +6,11 @@ Authors: Johannes Hölzl
 Relator for functions, pairs, sums, and lists.
 -/
 
+import tactic.reserved_notation
+
 namespace relator
 universe variables u₁ u₂ v₁ v₂
 
-reserve infixr ` ⇒ `:40
-
 /- TODO(johoelzl):
  * should we introduce relators of datatypes as recursive function or as inductive
 predicate? For now we stick to the recursor approach.

src/order/lattice.lean

@@ -23,8 +23,6 @@ section
 end
 
 /- TODO: automatic construction of dual definitions / theorems -/
-reserve infixl ` ⊓ `:70
-reserve infixl ` ⊔ `:65
 
 /-- Typeclass for the `⊔` (`\lub`) notation -/
 class has_sup (α : Type u) := (sup : α → α → α)
@@ -367,7 +365,8 @@ by simp only [sup_inf_left, λy:α, @sup_comm α _ y x, eq_self_iff_true]
 
 theorem inf_sup_left : x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z) :=
 calc x ⊓ (y ⊔ z) = (x ⊓ (x ⊔ z)) ⊓ (y ⊔ z)       : by rw [inf_sup_self]
-             ... = x ⊓ ((x ⊓ y) ⊔ z)             : by simp only [inf_assoc, sup_inf_right, eq_self_iff_true]
+             ... = x ⊓ ((x ⊓ y) ⊔ z)             : by simp only [inf_assoc, sup_inf_right,
+                                                                 eq_self_iff_true]
              ... = (x ⊔ (x ⊓ y)) ⊓ ((x ⊓ y) ⊔ z) : by rw [sup_inf_self]
              ... = ((x ⊓ y) ⊔ x) ⊓ ((x ⊓ y) ⊔ z) : by rw [sup_comm]
              ... = (x ⊓ y) ⊔ (x ⊓ z)             : by rw [sup_inf_left]