Zulip Chat Archive

Stream: general

Topic: github syntax highlighting

Reid Barton (Oct 25 2020 at 21:57):

@Johan Commelin and I have noticed some bugs in Lean syntax highlighting on GitHub lately, for example
https://github.com/leanprover-community/mathlib/blob/d4477fa7f79beea1058f72fc3741c88a1832d9a1/src/group_theory/ore_localization.lean#L29
(where it appears that syntax highlighting tried to turn part of the UTF-8 sequence for an angle bracket red, causing my browser to display it as two Unicode replacement characters).
Anyone else noticed this, or have any idea what's going on?

Reid Barton (Oct 25 2020 at 21:58):

I've also seen two instances where it gets confused about what is or is not a comment, for no apparent reason

Reid Barton (Oct 25 2020 at 22:00):

A vague theory is that it could be processing the files in chunks somehow, causing it to see something like -/ or a left angle bracket as two tokens instead of one

Bryan Gin-ge Chen (Oct 25 2020 at 22:02):

I think GitHub uses vscode-lean's syntax highlighting as an input, so provided Johan didn't see anything wrong in VS Code, something like your theory should be correct.

Bryan Gin-ge Chen (Oct 25 2020 at 22:05):

The relevant project for GitHub's syntax highlighting is here btw. I don't know if there's enough info there to figure out what's going on though.

Mario Carneiro (Oct 25 2020 at 22:08):

I was hoping to see a suspiciously round number, but the split utf-8 character occurs at 0x3fa = 1018 bytes into the file

Reid Barton (Oct 25 2020 at 22:10):

I'm getting flashbacks of the `[...] bug.

Reid Barton (Oct 25 2020 at 22:11):

I guess someone could make a file that's, like, entirely angle brackets and see if there's any pattern to the errors, if they can be reproduced this way at all

Mario Carneiro (Oct 25 2020 at 22:13):

well you also need something keywordy because the highlighting span is involved in the bug

Eric Wieser (Oct 26 2020 at 10:21):

Have you reported this to github?

Eric Wieser (Oct 26 2020 at 10:37):

https://github.com/github/linguist/issues/5069

Kevin Buzzard (Oct 26 2020 at 10:51):

ooh

https://github.com/leanprover-community/mathlib/blob/githubtest/test.lean

Eric Wieser (Oct 26 2020 at 11:23):

https://gist.github.com/eric-wieser/caef77bc87edc0feae06bd91b0d241f2/756f85e2f06618ef2b7261e7ec3fca0aa0d73e2f

Eric Wieser (Oct 26 2020 at 15:44):

Confirmed as a bug upstream, a trivial grammar of https://gist.github.com/eric-wieser/c5a9efea2581d65fda99ec2816177fde is enough to break it

Bryan Gin-ge Chen (Oct 26 2020 at 15:48):

Thanks for following up on this!

Kevin Buzzard (Oct 26 2020 at 15:52):

so Gabriel broke it in 2017 :-)

Reid Barton (Oct 28 2020 at 02:19):

Thanks @Eric Wieser for creating the github issue.
I checked out the other weird behaviors I've seen recently and I think these are actually specific to the Lean grammar. Both involve comments and what the grammar thinks is markdown syntax. I made MWEs:
https://gist.github.com/rwbarton/3f7a17bcb11ad808db7cacb1d675e921
https://gist.github.com/rwbarton/e9cc372ace57ff71c3d13c16f1f509eb
In the first, the syntax highlighting thinks the comment block extends indefinitely. In the second, it thinks the comment block extends for one non-whitespace line (very odd).

Do these snippets show correct syntax highlighting in VSCode?

Yakov Pechersky (Oct 28 2020 at 02:21):

No, they don't. I've seen this issue before in VSCode where an aberrant comment will make it seem like the rest of my file is commented out, but it compiles fine

Yakov Pechersky (Oct 28 2020 at 02:22):

image.png

Yakov Pechersky (Oct 28 2020 at 02:22):

image.png

Reid Barton (Oct 28 2020 at 02:26):

OK, so definitely an issue with the VSCode grammar then.

Bryan Gin-ge Chen (Oct 28 2020 at 02:26):

Reid Barton (Oct 28 2020 at 02:27):

I guess that might explain why I hadn't noticed it in mathlib ever, because most people would be using VSCode and select against putting stuff in comments that causes VSCode/github syntax highlighting to go haywire.