identifiers don't round-trip through pretty-printing

Stream: lean4

[Eric Wieser]

Is there any way to guard against this?

variable («forall» : Nat)

#check «forall» + 1 -- forall + 1 : Nat

-- paste what we got from the goal view
#check forall + 1 -- syntax error

[Eric Wieser]

This looks like a rare case where even pp.all true isn't enough to make things roundtrip

[Damiano Testa]

The pretty-printer seems to do the right thing if the identifier contains a space, though.

[Eric Wieser]

Yes, I think it knows about invalid identifiers, but not about ones that clash with syntax

[Eric Wieser]

I guess a pp.alwaysEscapeNames would be an ugly fix here

[Damiano Testa]

That is what happens with new projects in the lakefile, right?

[Eric Wieser]

Oh that's a fun test, is lake new forall broken? (answer: no, it escapes any name you use)

[Damiano Testa]

I do not know, but I know that I saw a lot of (unneeded) « when I created new projects.

[Eric Wieser]

Yes, I think this is probably why

[Kyle Miller]

Could you please create an issue? The syntax formatter just uses docs#Lean.Name.toString to print identifiers, and it's not aware of the current list of keywords yet.

[Eric Wieser]

lean4#4686