Zulip Chat Archive

Stream: general

Topic: generalize semicolon


view this post on Zulip Kenny Lau (Jul 23 2019 at 13:29):

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

view this post on Zulip Kenny Lau (Jul 23 2019 at 13:29):

somehow the last one breaks Lean

view this post on Zulip Keeley Hoek (Jul 23 2019 at 13:52):

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

view this post on Zulip Keeley Hoek (Jul 23 2019 at 13:52):

There is a bug which never got fixed

view this post on Zulip Kenny Lau (Jul 23 2019 at 13:52):

what's the bug?

view this post on Zulip Keeley Hoek (Jul 23 2019 at 13:53):

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

view this post on Zulip Keeley Hoek (Jul 23 2019 at 13:53):

But then that is hidden from you

view this post on Zulip Keeley Hoek (Jul 23 2019 at 13:53):

And instead you just get that

view this post on Zulip Keeley Hoek (Jul 23 2019 at 13:53):

vm_check business

view this post on Zulip Keeley Hoek (Jul 23 2019 at 13:54):

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

view this post on Zulip Keeley Hoek (Jul 23 2019 at 13:54):

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

view this post on Zulip Keeley Hoek (Jul 23 2019 at 13:55):

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

view this post on Zulip Keeley Hoek (Jul 23 2019 at 13:55):

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).

view this post on Zulip Keeley Hoek (Jul 23 2019 at 13:58):

After checking, indeed it doesn't.


Last updated: May 13 2021 at 04:21 UTC