[Merged by Bors] - fix(init/meta/converter/interactive): Do not ignore errors and tactic state changes in for and find

[eric-wieser]

An example of the type of code that used to work and now fails:

import algebra.ring

example {a b c : ℕ} : (a * b) * c = (a * b) * c :=  begin
  conv {
    for (_ * _) [1] {
      rw this_isnt_a_lemma,  -- no error message?
    },
  },
end

example {a b c : ℕ} : (a * b) * c = (a * b) * c :=  begin
  conv {
    find (_ * _) {
      rw this_isnt_a_lemma,  -- no error message?
    },  -- error: pattern not found (not true!)
  },
end

Without this PR, users like me get no information on why their tactic failed, which is a very frustrating experience.

The problem here is that ext_simplify_core ignores all failures in its pre and post arguments - failures are treated as "there was nothing to simplify here, move on to the next one". In find and for, we need to distinguish the cases of failing due to the pattern not matching and failuring due to an error in the user-provided tactic.

This PR adds three new tactic primitives, tactic.capture, tactic.unwrap, and tactic.resume, the first two of which are inspired by the python functions from the trio-outcome package with the same name. capture can be used to run the user-provided tactic and keep track of any errors that occured. unwrap is then used to re-throw the error once ext_simplify_core is done.

It turns out that not only does ext_simplify_core ignore all failures, but it resets the tactic state after it completes - which clears populated metavariables. To preserve the tactic state, we need resume.

---

A replacement for #476, since that PR does not have CI runs

[gebner]

Could you please add the other test case from #476 (comment) and copy the PR description from #476 (bors uses it in the commit message).

Otherwise LGTM.

bors d+

[bors]

✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[eric-wieser]

Where should the passing test-cases go?

[gebner]

Oh, I didn't look where you put the test case. Typically these test cases (where the error message is important) go into tests/lean. You can then also put the passing test case in the same file.

Some explanation here: https://github.com/leanprover-community/lean/blob/master/doc/fixing_tests.md

[eric-wieser]

bors r+

[eric-wieser]

Thanks for the review, and for pointing me towards the better fix!

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build emscripten
• Build linux Debug
• Build linux Release
• Build macos Debug
• Build macos Release
• Build windows Release