Zulip Chat Archive

Stream: lean4

Topic: elab not implemented picks up comments


view this post on Zulip Mario Carneiro (Apr 12 2021 at 14:41):

syntax "foo" : term
#eval foo
-- bla
-- baz

prints

elaboration function for 'termFoo' has not been implemented
  foo
    -- bla
    -- baz

note the presence of the comments in the error message

view this post on Zulip Mario Carneiro (Apr 12 2021 at 14:42):

This is I guess borderline on whether this is desired behavior

view this post on Zulip Daniel Selsam (Apr 12 2021 at 16:13):

FWIW it looks weird to me. My -- comments generally precede terms rather than follow them.

view this post on Zulip Sebastian Ullrich (Apr 12 2021 at 16:28):

Yes, there is a separate pass from parsing that associates whitespace/comments to the "correct" token. https://github.com/leanprover/lean4/blob/5fc1a86274369d69171f6db5096e98bb43d0a78a/src/Lean/Syntax.lean#L139-L154
We don't currently run it before elaboration, but I also think this error message is one of the few/the only one that actually prints out input syntax

view this post on Zulip Sebastian Ullrich (Apr 12 2021 at 16:31):

I think there are much bigger issues with this error message and how to debug it (when complex syntax pattern matches are involved) than showing unexpected comments. I'm not even sure if it shouldn't just show the raw syntax tree by default. Definitely not something a user not implementing their own syntax should ever see.


Last updated: May 07 2021 at 13:21 UTC