Update GitHub syntax high-light for Lean 4

[leodemoura]

@Kha @gebner Do you know where we have to add the new keywords?
I did it once, but I forgot where we should add them.

[gebner]

The syntax highlighting is taken from the vscode-lean extension:
https://github.com/leanprover/vscode-lean/blob/master/syntaxes/lean.json
See leanprover/vscode-lean#121 for why github switched to it.

We should probably make a new syntax highlighting grammar that works for both Lean 3 and Lean 4, and then have github switch to that.

[eric-wieser]

https://github.com/github/linguist is responsible for the highlighting on github. I think the best way to do this would be:

• Tell linguist about a new language, Lean4, provided by https://github.com/leanprover-community/vscode-lean4. This involves adding it to https://github.com/github/linguist/blob/master/grammars.yml, and adding vscode-lean4 as a submodule.
• Give linguist a heuristic for distinguishing lean3 and lean4 code in https://github.com/github/linguist/blob/master/lib/linguist/heuristics.yml. An easy one I can think of is for either of the following to indicate lean 4:
  • => tokens
  • import [A-Z] since filename conventions have changed

[eric-wieser]

Although we may run into trouble with:

We try only to add new extensions once they have some usage on GitHub. In most cases we prefer that each new file extension be in use in at least 200 unique :user/:repo repositories before supporting them in Linguist.

[eric-wieser]

I did this in github-linguist/linguist#6616

[mhuisi]

@eric-wieser Nice! I put this on hold because I wanted to do an improvement pass on the vscode-lean4 textmate grammar first, but wasn't aware that linguist references the repository itself, and so there is no need to improve the grammar before the corresponding linguist PR.

[eric-wieser]

github-linguist/linguist#6616 is now merged!

[kim-em]

Does this mean we can close this issue?

[eric-wieser]

The linguist release should be tomorrow; so hopefully we'll see if it worked by the end of the week

[eric-wieser]

https://gist.github.com/eric-wieser/b41f0125324b0ba767da53e6bfdaa357 suggests this is working as intended; now we have the long tail of improving the grammar in places where it looks bad on github (since elsewhere we normally rely on the semantic highlighting anyway)

I think this issue can be closed as completed!