fix(init/meta/converter/interactive): Do not allow rw to create ⊢ goals in conv mode

[eric-wieser]

This is an attempt at the approach described at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Closing.20.60.E2.8A.A2.60.20goals.20in.20.60conv.60.20mode/near/212702071

A contrived example where this applies:

import algebra.ring
variables {α : Type*} [ring α] {a b c : α}

lemma obvious : c = 1 → (a * b) * c = a * b := λ h, by {rw [h, mul_one]}

example (hc : c = 1) (hb : b = 1) : (a * b) * c = a := begin
  conv_lhs {
    rw obvious,  -- this now fails, as it creates goals that can't be closed
    -- TODO: allow a tactic block to be passed as a trailing argument
  },
  rw [hb, mul_one],
end

[eric-wieser]

I don't know how to let a tactic block be passed in here

[bryangingechen]

Could you add some tests showing the desired new behavior?

[eric-wieser]

Where would you like the test to go? https://github.com/leanprover-community/lean/tree/master/tests/lean/interactive/conv.lean?

[eric-wieser]

At any rate, this doesn't work yet, and I need help to make it work.

[bryangingechen]

There are a few types of tests:

• Lean files in tests/lean should generate the corresponding .lean.expected.out file.
• Lean files in tests/lean/run should run without creating any output
• Lean files in tests/lean/fail should fail

See also doc/fixing_tests.md.