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):
Kevin Buzzard (Jun 24 2020 at 08:17):
Bryan was right :-)
Last updated: Dec 20 2023 at 11:08 UTC