fix(test/*): make sure tests produce no output (#3947)

Modify tests so that they produce no output. This also means removing all uses of `sorry`/`admit`.
Replace `#eval` by `run_cmd` consistently.
Tests that produced output before are modified so that it is checked that they roughly produce the right output
Add a trace option to the `#simp` command that turns the message of only if the expression is simplified to `true`. All tests are modified so that they simplify to `true`.
The randomized tests can produce output when they find a false positive, but that should basically never happen.
Add some docstings to `src/tactic/interactive`.

src/tactic/interactive.lean

@@ -391,7 +391,6 @@ We use this tactic for writing tests.
 meta def guard_target_strict (p : parse texpr) : tactic unit :=
 do t ← target, guard_expr_strict t p
 
-
 /--
 `guard_hyp_strict h : t` fails if the hypothesis `h` does not have type syntactically equal
 to `t`.
@@ -400,19 +399,33 @@ We use this tactic for writing tests.
 meta def guard_hyp_strict (n : parse ident) (p : parse $ tk ":" *> texpr) : tactic unit :=
 do h ← get_local n >>= infer_type >>= instantiate_mvars, guard_expr_strict h p
 
+/-- Tests that there are `n` hypotheses in the current context. -/
 meta def guard_hyp_nums (n : ℕ) : tactic unit :=
 do k ← local_context,
    guard (n = k.length) <|> fail format!"{k.length} hypotheses found"
 
+/-- Test that `t` is the tag of the main goal. -/
 meta def guard_tags (tags : parse ident*) : tactic unit :=
 do (t : list name) ← get_main_tag,
    guard (t = tags)
 
+/-- `guard_proof_term { t } e` applies tactic `t` and tests whether the resulting proof term
+  unifies with `p`. -/
+meta def guard_proof_term (t : itactic) (p : parse texpr) : itactic :=
+do
+  g :: _ ← get_goals,
+  e ← to_expr p,
+  t,
+  g ← instantiate_mvars g,
+  unify e g
+
+
 /-- `success_if_fail_with_msg { tac } msg` succeeds if the interactive tactic `tac` fails with
 error message `msg` (for test writing purposes). -/
 meta def success_if_fail_with_msg (tac : tactic.interactive.itactic) :=
 tactic.success_if_fail_with_msg tac
 
+/-- Get the field of the current goal. -/
 meta def get_current_field : tactic name :=
 do [_,field,str] ← get_main_tag,
    expr.const_name <$> resolve_name (field.update_prefix str)
@@ -649,12 +662,16 @@ add_tactic_doc
   decl_names := [`tactic.interactive.field_simp],
   tags       := ["simplification", "arithmetic"] }
 
+/-- Tests whether `t` is definitionally equal to `p`. The difference with `guard_expr_eq` is that
+  this uses definitional equality instead of alpha-equivalence. -/
 meta def guard_expr_eq' (t : expr) (p : parse $ tk ":=" *> texpr) : tactic unit :=
 do e ← to_expr p, is_def_eq t e
 
 /--
-`guard_target t` fails if the target of the main goal is not `t`.
+`guard_target' t` fails if the target of the main goal is not definitionally equal to `t`.
 We use this tactic for writing tests.
+The difference with `guard_target` is that this uses definitional equality instead of
+alpha-equivalence.
 -/
 meta def guard_target' (p : parse texpr) : tactic unit :=
 do t ← target, guard_expr_eq' t p

src/tactic/simp_command.lean

@@ -46,6 +46,9 @@ meta def simp_arg_type.replace_subexprs : simp_arg_type → list (expr × expr)
 
 setup_tactic_parser
 
+/- Turn off the messages if the result is exactly `true` with this option. -/
+declare_trace silence_simp_if_true
+
 /--
 The basic usage is `#simp e`, where `e` is an expression,
 which will print the simplified form of `e`.
@@ -100,7 +103,8 @@ do
   } ts,
 
   /- Trace the result. -/
-  trace simp_result
+  when (¬ is_trace_enabled_for `silence_simp_if_true ∨ simp_result ≠ expr.const `true [])
+    (trace simp_result)
 
 add_tactic_doc
 { name                     := "#simp",

src/tactic/squeeze.lean

@@ -185,6 +185,15 @@ namespace interactive
 
 attribute [derive decidable_eq] simp_arg_type
 
+/-- Turn a `simp_arg_type` into a string. -/
+meta instance simp_arg_type.has_to_string : has_to_string simp_arg_type :=
+⟨λ a, match a with
+| simp_arg_type.all_hyps := "*"
+| (simp_arg_type.except n) := "-" ++ to_string n
+| (simp_arg_type.expr e) := to_string e
+| (simp_arg_type.symm_expr e) := "←" ++ to_string e
+end⟩
+
 /-- combinator meant to aggregate the suggestions issued by multiple calls
 of `squeeze_simp` (due, for instance, to `;`).
 

test/README.md

@@ -0,0 +1,15 @@
+# The Mathlib Test Directory
+
+In this directory we collect various tests for the commands, tactics and metaprograms written in
+mathlib (see [the tactic folder](../src/tactic)).
+
+Tests for all tactics are highly encouraged, especially if they are used sparingly in mathlib.
+Here are some guidelines for writing a test:
+
+* Make sure that the test fails if something unexpected happens. Use `guard`, `guard_target`, `guard_hyp`, `get_decl` or similar tactics that fail if the tactic state is incorrect.
+* Make sure that the test is silent, i.e. produces no output when it succeeds. This makes it easy to spot the tests that actually failed. Furthermore, it is unlikely that anyone will notice the output changing if the test keeps succeeding.
+
+Some tips to make a test silent:
+* Instead of `trace e`, write `guard (e = expected_expression)`.
+* If you write a tactic/command that normally produces output, consider adding an option that silences it. See for example the uses of `set_option trace.silence_library_search true` in the [library_search](library_search) folder.
+* Do not prove a lemma using `admit` or `sorry`. Instead make sure that the lemma is provable, and prove it by `assumption` or `trivial` or similar.

test/continuity.lean

@@ -6,28 +6,27 @@ import analysis.special_functions.trigonometric
 example {X Y : Type*} [topological_space X] [topological_space Y]
   (f₁ f₂ : X → Y) (hf₁ : continuous f₁) (hf₂ : continuous f₂)
   (g : Y → ℝ) (hg : continuous g) : continuous (λ x, (max (g (f₁ x)) (g (f₂ x))) + 1) :=
-by show_term { continuity }
--- prints `refine ((continuous.comp hg hf₁).max (continuous.comp hg hf₂)).add continuous_const`
+by guard_proof_term { continuity } ((hg.comp hf₁).max (hg.comp hf₂)).add continuous_const
 
 example {κ ι : Type}
   (K : κ → Type) [∀ k, topological_space (K k)] (I : ι → Type) [∀ i, topological_space (I i)]
   (e : κ ≃ ι) (F : Π k, homeomorph (K k) (I (e k))) :
   continuous (λ (f : Π k, K k) (i : ι), F (e.symm i) (f (e.symm i))) :=
-by show_term { continuity }
--- prints, modulo a little bit of cleaning up the pretty printer:
---   `exact continuous_pi (λ i, ((F (e.symm i)).continuous).comp (continuous_apply (e.symm i)))`
+by guard_proof_term { continuity }
+  @continuous_pi _ _ _ _ _ (λ (f : Π k, K k) i, (F (e.symm i)) (f (e.symm i)))
+    (λ (i : ι), ((F (e.symm i)).continuous).comp (continuous_apply (e.symm i)))
 
 open real
 
 local attribute [continuity] continuous_exp continuous_sin continuous_cos
 
 example : continuous (λ x : ℝ, exp ((max x (-x)) + sin x)^2) :=
-by show_term { continuity }
--- prints
---   `exact (continuous_exp.comp ((continuous_id.max continuous_id.neg).add continuous_sin)).pow 2`
+by guard_proof_term { continuity }
+  (continuous_exp.comp ((continuous_id.max continuous_id.neg).add continuous_sin)).pow 2
 
 example : continuous (λ x : ℝ, exp ((max x (-x)) + sin (cos x))^2) :=
-by show_term { continuity }
+by guard_proof_term { continuity }
+ (continuous_exp.comp ((continuous_id'.max continuous_id'.neg).add (continuous_sin.comp continuous_cos))).pow 2
 
 -- Without `md := semireducible` in the call to `apply_rules` in `continuity`,
 -- this last example would have run off the rails:

test/doc_commands.lean

@@ -9,7 +9,7 @@ def foo := 5
 /-- ok -/
 add_decl_doc foo
 
-#eval do
+run_cmd do
 ds ← doc_string ``foo,
 guard $ ds = "ok"
 

test/general_recursion.lean

@@ -195,8 +195,7 @@ by rw roption.dom_iff_mem; apply exists_imp_exists _ (f91_spec n); simp
 
 def f91' (n : ℕ) : ℕ := (f91 n).get (f91_dom n)
 
-#eval f91' 109
--- 99
+run_cmd guard (f91' 109 = 99)
 
 lemma f91_spec' (n : ℕ) : f91' n = if n > 100 then n - 10 else 91 :=
 begin

test/library_search/exp_le_exp.lean

@@ -3,4 +3,7 @@ import analysis.special_functions.exp_log
 
 open real
 
+/- Turn off trace messages so they don't pollute the test build: -/
+set_option trace.silence_library_search true
+
 example {a b : ℝ} (h: a ≤ b) : exp a ≤ exp b := by library_search

test/library_search/filter.lean

@@ -2,6 +2,9 @@ import order.filter.basic
 
 open filter
 
+/- Turn off trace messages so they don't pollute the test build: -/
+set_option trace.silence_library_search true
+
 example {α β γ : Type*} {A : filter α} {B : filter β} {C : filter γ} {f : α → β} {g : β → γ}
   (hf : tendsto f A B) (hg : tendsto g B C) : tendsto (g ∘ f) A C :=
 calc

test/library_search/nat.lean

@@ -8,7 +8,6 @@ import data.nat.basic
 
 namespace test.library_search
 
-
 /- Turn off trace messages so they don't pollute the test build: -/
 set_option trace.silence_library_search true
 /- For debugging purposes, we can display the list of lemmas: -/

test/linarith.lean

@@ -336,10 +336,11 @@ example (a : E) (h : a = a) : 1 ≤ 2  := by nlinarith
 -- test that the apply bug doesn't affect linarith preprocessing
 
 constant α : Type
+variable [fact false] -- we work in an inconsistent context below
 def leα : α → α → Prop := λ a b, ∀ c : α, true
 
 noncomputable instance : discrete_linear_ordered_field α :=
-by refine_struct { le := leα }; admit
+by refine_struct { le := leα }; exact false.elim _inst_2
 
 example (a : α) (ha : a < 2) : a ≤ a :=
 by linarith
@@ -352,7 +353,7 @@ by nlinarith
 -- do not cause an exception
 variables {R : Type*} [ring R] (abs : R → ℚ)
 
-lemma abs_nonneg' : ∀ r, 0 ≤ abs r := sorry
+lemma abs_nonneg' : ∀ r, 0 ≤ abs r := false.elim _inst_2
 
 example (t : R) (a b : ℚ) (h : a ≤ b) : abs (t^2) * a ≤ abs (t^2) * b :=
 by nlinarith [abs_nonneg' abs (t^2)]
@@ -370,7 +371,7 @@ constant T_zero : ordered_ring T
 
 namespace T
 
-lemma zero_lt_one : (0 : T) < 1 := sorry
+lemma zero_lt_one : (0 : T) < 1 := false.elim _inst_2
 
 lemma works {a b : ℕ} (hab : a ≤ b) (h : b < a) : false :=
 begin

test/lint_coe_t.lean

@@ -18,7 +18,7 @@ end
 noncomputable instance quot_to_a {α} (R : setoid α) : has_coe (quotient R) α :=
 ⟨λ q, quot.rec_on q (λ a, classical.choice ⟨a⟩) (by cc)⟩
 
-#eval do
+run_cmd do
 decl ← get_decl ``quot_to_a,
 -- linter does not complain
 none ← linter.has_coe_variable.test decl,
@@ -29,7 +29,7 @@ section
 local attribute [instance]
 def int_to_a {α} [inhabited α] : has_coe ℤ α := ⟨λ _, default _⟩
 
-#eval do
+run_cmd do
 decl ← get_decl ``int_to_a,
 -- linter does not complain
 some _ ← linter.has_coe_variable.test decl,

test/lint_coe_to_fun.lean

@@ -16,7 +16,7 @@ instance {α β} : has_coe (sparkling_equiv α β) (equiv α β) :=
 
 -- should complain
 open tactic
-#eval do
+run_cmd do
 decl ← get_decl ``sparkling_equiv,
 res ← linter.has_coe_to_fun.test decl,
 -- linter complains
@@ -26,7 +26,7 @@ instance {α β} : has_coe_to_fun (sparkling_equiv α β) :=
 ⟨λ _, α → β, λ f, f.to_equiv.to_fun⟩
 
 -- prima!
-#eval do
+run_cmd do
 decl ← get_decl ``sparkling_equiv,
 res ← linter.has_coe_to_fun.test decl,
 -- linter doesn't complain
@@ -52,7 +52,7 @@ instance {α β} [nonempty α] : has_coe (sparkling_equiv α β) (equiv α β) :
 
 -- should complain
 open tactic
-#eval do
+run_cmd do
 decl ← get_decl ``sparkling_equiv,
 res ← linter.has_coe_to_fun.test decl,
 -- linter complains

test/lint_simp_comm.lean

@@ -6,14 +6,14 @@ import algebra.group.basic
 attribute [simp] add_comm add_left_comm
 
 open tactic
-#eval do
+run_cmd do
 decl ← get_decl ``add_comm,
 res ← linter.simp_comm.test decl,
 -- linter complains
 guard res.is_some
 
 open tactic
-#eval do
+run_cmd do
 decl ← get_decl ``add_left_comm,
 res ← linter.simp_comm.test decl,
 -- linter complains
@@ -37,7 +37,7 @@ end
 
 open tactic
 set_option pp.all true
-#eval do
+run_cmd do
 decl ← get_decl ``list.filter_congr_decidable,
 res ← linter.simp_comm.test decl,
 -- linter does not complain

test/lint_simp_nf.lean

@@ -17,7 +17,7 @@ begin
 end
 
 open tactic
-#eval do
+run_cmd do
 decl ← get_decl ``f_c,
 res ← linter.simp_nf.test decl,
 -- linter complains
@@ -45,7 +45,7 @@ begin
 end
 
 open tactic
-#eval do
+run_cmd do
 decl ← get_decl ``h_c,
 res ← linter.simp_nf.test decl,
 -- linter complains

test/lint_simp_var_head.lean

@@ -17,7 +17,7 @@ end
 
 
 open tactic
-#eval do
+run_cmd do
 decl ← get_decl ``const_zero_eq_zero,
 res ← linter.simp_var_head.test decl,
 -- linter complains

test/logic_inline.lean

@@ -9,5 +9,7 @@ meta def error_msg (s : string) : bool := @undefined_core bool $ s ++ ".decidabl
 
 meta def examine (b : Prop) [decidable b] : bool := b
 
-#eval examine $ ff ∧ (error_msg "and")
-#eval examine $ tt ∨ (error_msg "or")
+open tactic
+
+run_cmd do e ← to_expr ```(examine (ff ∧ (error_msg "and"))) >>= eval_expr bool, guard (e = ff)
+run_cmd do e ← to_expr ```(examine (tt ∨ (error_msg "or"))) >>= eval_expr bool, guard (e = tt)

test/norm_cast_int.lean

@@ -5,14 +5,14 @@ set_option pp.numerals false
 set_option pp.notation false
 -- set_option trace.simplify.rewrite true
 
-#eval norm_cast.numeral_to_coe `(0 : ℤ)
-#eval norm_cast.numeral_to_coe `(1 : ℤ)
-#eval norm_cast.numeral_to_coe `(2 : ℤ)
-#eval norm_cast.numeral_to_coe `(3 : ℤ)
+run_cmd norm_cast.numeral_to_coe `(0 : ℤ)
+run_cmd norm_cast.numeral_to_coe `(1 : ℤ)
+run_cmd norm_cast.numeral_to_coe `(2 : ℤ)
+run_cmd norm_cast.numeral_to_coe `(3 : ℤ)
 
-#eval norm_cast.coe_to_numeral `((0 : ℕ) : ℤ)
-#eval norm_cast.coe_to_numeral `((1 : ℕ) : ℤ)
-#eval norm_cast.coe_to_numeral `((2 : ℕ) : ℤ)
-#eval norm_cast.coe_to_numeral `((3 : ℕ) : ℤ)
+run_cmd norm_cast.coe_to_numeral `((0 : ℕ) : ℤ)
+run_cmd norm_cast.coe_to_numeral `((1 : ℕ) : ℤ)
+run_cmd norm_cast.coe_to_numeral `((2 : ℕ) : ℤ)
+run_cmd norm_cast.coe_to_numeral `((3 : ℕ) : ℤ)
 
 example : ((42 : ℕ) : ℤ) = 42 := by norm_cast

test/norm_cast_lemma_order.lean

@@ -10,12 +10,12 @@ set_option pp.notation false
 set_option pp.numerals false
 
 -- should work
-#eval norm_cast.numeral_to_coe `(0 : ℝ)
-#eval norm_cast.numeral_to_coe `(1 : ℝ)
-#eval norm_cast.numeral_to_coe `(2 : ℝ)
-#eval norm_cast.numeral_to_coe `(3 : ℝ)
+run_cmd norm_cast.numeral_to_coe `(0 : ℝ)
+run_cmd norm_cast.numeral_to_coe `(1 : ℝ)
+run_cmd norm_cast.numeral_to_coe `(2 : ℝ)
+run_cmd norm_cast.numeral_to_coe `(3 : ℝ)
 
-#eval norm_cast.coe_to_numeral `((0 : ℕ) : ℝ)
-#eval norm_cast.coe_to_numeral `((1 : ℕ) : ℝ)
-#eval norm_cast.coe_to_numeral `((2 : ℕ) : ℝ)
-#eval norm_cast.coe_to_numeral `((3 : ℕ) : ℝ)
+run_cmd norm_cast.coe_to_numeral `((0 : ℕ) : ℝ)
+run_cmd norm_cast.coe_to_numeral `((1 : ℕ) : ℝ)
+run_cmd norm_cast.coe_to_numeral `((2 : ℕ) : ℝ)
+run_cmd norm_cast.coe_to_numeral `((3 : ℕ) : ℝ)

test/norm_cast_sum_lambda.lean

@@ -7,13 +7,13 @@ constant series {α} (f : ℕ → α) : α
 
 @[norm_cast] axiom coe_le (a b : ℕ) : (a : ℤ) ≤ b ↔ a ≤ b
 
-#eval do
+run_cmd do
 l ← norm_cast.make_guess ``coe_series,
 guard $ l = norm_cast.label.move
 
-example (f : ℕ → ℕ) : (0 : ℤ) ≤ series (λ x, f x) :=
+example (f : ℕ → ℕ) (h : (0 : ℕ) ≤ series (λ x, f x)) : (0 : ℤ) ≤ series (λ x, f x) :=
 begin
   norm_cast,
   guard_target (0 : ℕ) ≤ series (λ x, f x),
-  sorry
+  exact h
 end