Zulip Chat Archive

Stream: general

Topic: memory bug?


Alex J. Best (Jun 24 2020 at 01:09):

I see the same behavior with 3.4.2.

Alex J. Best (Jun 24 2020 at 01:12):

example : true := by trivial
.
#che

works fine, and

example : true := by sorry
#che

is broken, while

example : true := sorry
#che

is okay!

Bryan Gin-ge Chen (Jun 24 2020 at 01:13):

So maybe something in the tactic parser?

Alex J. Best (Jun 24 2020 at 01:14):

Yeah looks like it:

example : true := by {sorry}
#che

is okay also.

Lucas Viana (Jun 24 2020 at 01:14):

It doesn't need to be #che, # is also broken

Lucas Viana (Jun 24 2020 at 01:15):

But it must be incomplete (#check is okay)

Mario Carneiro (Jun 24 2020 at 01:25):

How is #che lexed? I don't think # is a valid identifier character, but then I'm not sure how commands containing # work

Bryan Gin-ge Chen (Jun 24 2020 at 01:48):

More examples:

example : true := by { sorry # } -- broken
example : true := begin { sorry # } end -- broken

Mario Carneiro (Jun 24 2020 at 02:54):

Is it still broken if # is a notation, say an infix or prefix operator?

Mario Carneiro (Jun 24 2020 at 02:55):

I think in core # doesn't mean anything

Bryan Gin-ge Chen (Jun 24 2020 at 04:36):

Ah, you're onto something:

example : true :=
begin
sorry #, -- broken
end
notation # := 1
example : true :=
begin
sorry #, -- errors as expected
end

Mario Carneiro (Jun 24 2020 at 05:19):

My guess is that # doesn't fall in any lexical class, and lean bugs out

Mario Carneiro (Jun 24 2020 at 05:20):

if you declare it as a notation then it becomes a token

Bryan Gin-ge Chen (Jun 24 2020 at 05:21):

I was staring at parse_interactive_tactic and the stuff it calls a little earlier, but I wasn't able to make any progress without access to a debugger. Presumably Gabriel will be able to figure out what's going on instantaneously.

Gabriel Ebner (Jun 24 2020 at 08:12):

lean#356

Kevin Buzzard (Jun 24 2020 at 08:17):

Bryan was right :-)


Last updated: Dec 20 2023 at 11:08 UTC