docs#conv.interactive.for squashes errors

Stream: general

[Eric Wieser]

This example succeeds with no diagnostics:

import algebra.ring

example {α : Type*} [ring α] {a b c : α} : (a * b) * c = (a * b) * c :=  begin
  conv {
    for (_ * _) [1] {
      rw add_mul,  -- no error message?
    },
  },
  refl,
end

because docs#conv.interactive.for is implemented in terms of docs#tactic.ext_simplify_core, and ext_simplify_core discards all monadic errors in its pre callback.

[Eric Wieser]

(https://leanprover-community.github.io/mathlib_docs/tactics.html#conv:%20for, since the link above doesn't go there)

[Eric Wieser]

I think I know how to fix this, but to do it I need some way to convert a tactic unit into a tactic_result unit, and I don't know enough about monads

[Eric Wieser]

Specifically, I want the lean equivalent of the python:

try:
    new_e, pr =  c.convert e r
except Exception as e:
    return (e, ...)  # how do I get `e` here?
else:
    return (None, ...)

[Eric Wieser]

Worked it out: https://github.com/leanprover-community/lean/pull/476

[Eric Wieser]

The docs#conv.interactive.find command has a similar problem, where an incorrect "pattern was not found" message is emitted