Zulip Chat Archive

Stream: general

Topic: parser.of_tactic is broken when the tactic fails

view this post on Zulip Mario Carneiro (Aug 30 2018 at 23:36):

I just stumbled on the following issue:

open tactic
meta def test : tactic unit := failed
meta def tac (_ : interactive.parse test) := skip
run_cmd add_interactive [`tac]
example : true := by tac.
-- vm check failed: is_closure(o) (possibly due to incorrect axioms, or sorry)

The problem appears to be that nothing catches an error thrown in a tactic when it is passed through the of_tactic builtin function

Last updated: May 13 2021 at 05:21 UTC