Mario Carneiro (Apr 12 2021 at 14:41):
syntax "foo" : term #eval foo -- bla -- baz
elaboration function for 'termFoo' has not been implemented foo -- bla -- baz
note the presence of the comments in the error message
Mario Carneiro (Apr 12 2021 at 14:42):
This is I guess borderline on whether this is desired behavior
Daniel Selsam (Apr 12 2021 at 16:13):
FWIW it looks weird to me. My
-- comments generally precede terms rather than follow them.
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
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