generalize semicolon

Stream: general

[Kenny Lau]

example : 0 = 0 := by {generalize : 0 = n, refl}

example : 0 = 0 :=
begin
  generalize : 0 = n,
  refl
end

example : 0 = 0 := by generalize : 0 = n; refl

[Kenny Lau]

somehow the last one breaks Lean

[Keeley Hoek]

Kenny, this is just because error handling in the parser monad is screwed

[Keeley Hoek]

There is a bug which never got fixed

[Kenny Lau]

what's the bug?

[Keeley Hoek]

The actually error which is being suppressed is that the semicolon is being parsed as part of the 0 = n stuff and that's throwing an error

[Keeley Hoek]

But then that is hidden from you

[Keeley Hoek]

And instead you just get that

[Keeley Hoek]

vm_check business

[Keeley Hoek]

MWE:

open tactic tactic.interactive interactive.types interactive lean.parser lean expr

private meta def some_arg : parser (pexpr × name) :=
fail "OOPSIE"

meta def tactic.interactive.oopsie (p : parse some_arg) : tactic unit
:= tactic.skip

example : 0 = 0 := by oopsie; refl

[Keeley Hoek]

In this case private meta def generalize_arg_p : parser (pexpr × name) in the definition of generalize is failing

[Keeley Hoek]

The culprit is

private meta def generalize_arg_p_aux : pexpr → parser (pexpr × name)
| (app (app (macro _ [const `eq _ ]) h) (local_const x _ _ _)) := pure (h, x)
| _ := fail "parse error"

private meta def generalize_arg_p : parser (pexpr × name) :=
with_desc "expr = id" $ parser.pexpr 0 >>= generalize_arg_p_aux

[Keeley Hoek]

That fail "parse error" is setting fire to the world and then blowing it up,
instead of just printing parse error to the console. I have a fix in mathlib for the coersion from parser to tactic, but I'd wager that doesn't fix this situation, since the parser being invoked is too deep I think (unless it works in a more hacky way than I expect, in which case importing tactic.core may just magically fix the issue).

[Keeley Hoek]

After checking, indeed it doesn't.