Markdown codeblocks: `lean4` or `lean-4`?

Stream: general

[Eric Wieser]

I only just saw this message in response to the lean 4 syntax I added on github. Unfortunately, it seems that this means on github you have to write

```lean-4
abbrev some_lean := 37
```

as opposed to the Zulip

```lean4
abbrev some_lean := 37
```

I assume we want to converge on the version without the -?

[Eric Wieser]

(either we change GitHub to drop the " " which becomes a -, or we add the - in Pygments to change Zulip)

[Hanson Char]

Eric Wieser said:

(either we change GitHub to drop the " " which becomes a -, or we add the - in Pygments to change Zulip)

Seems lean4 is currently being adopted, not lean-4 by Github's markdown. See linguist/languages.yml.

[Eric Wieser]

It's quite easy to prove that wrong by pasting what I wrote above into a github comment.

[Hanson Char]

ok, in that case, I wonder where these tags are actually defined.

[Eric Wieser]

It's defined by the string "Lean 4", as described by the comment I linked at the start of my first message. (hence 'drop the " "' being my proposed fix if we want to drop the -)

[Hanson Char]

Eric Wieser said:

(either we change GitHub to drop the " " which becomes a -, or we add the - in Pygments to change Zulip)

I'd vote for fixing github to lean4.

[Eric Wieser]

/poll What name should be used in codeblocks

• lean4 (fix github-linguist)
• lean-4 (fix Pygments)

[François G. Dorais]

Is there a reason not to use just lean?

[Kevin Buzzard]

(I believe the reason is "that's already taken by lean 3")

[Hanson Char]

Kevin Buzzard said:

(I believe the reason is "that's already taken by lean 3")

Is it not possible to have one single syntax highlighting for both lean3 and lean4, so users can simply use the lean tag without worrying about versions? This also paves the way for future version upgrades, if any.

[Eric Wieser]

I think it's a good things for language models etc for code to be clearly labelled as 3 vs 4

[Hanson Char]

Eric Wieser said:

I think it's a good things for language models etc for code to be clearly labelled as 3 vs 4

That makes sense from an LLM clarity standpoint. At the same time, one could argue that a well-trained language model should be able to infer the version from context or syntax. Requiring a version suffix in the code block label places extra burden on users and could become unwieldy as the ecosystem evolves.

[Eric Wieser]

I think we can afford the cost of users typing a 4 occasionally, especially since Zulip applies lean4 automatically

[Eric Wieser]

#7434 attempts to fix this

[Kim Morrison]

This seems silly, who is ever going to type the 4? The only reasonable answer here is just lean. :woman_shrugging:

If that doesn't work somewhere, the tooling is wrong, not the user.

Verso expects just lean.

[Marc Huisinga]

Kim Morrison said:

This seems silly, who is ever going to type the 4? The only reasonable answer here is just lean. :woman_shrugging:

If that doesn't work somewhere, the timing is wrong, not the user.

Verso expects just lean.

This made me realize that the VS Code extension is also still only providing syntax highlighting for lean4 (which is an artifact from when it still supported running the Lean 3 extension alongside the Lean 4 one without disabling either one), which means that all ```lean code blocks aren't properly highlighted in hovers, but we can also fix that now by supporting both language IDs: vscode-lean4#622

[Thomas Zhu]

Is it possible to have a syntax highlighter that primarily supports Lean 4 but would still try to render Lean 3 correctly? (Analogously, Python 2 and 3 have the same highlighter in Linguist)

[Thomas Zhu]

Separately, to me, Lean 4 having the extension .lean and not .lean4 intuitively means that Lean 4 overrides Lean 3, which is now EOL. So I agree with having just ```lean instead of lean4. (Again, analogously python refers to Python 3 by default in Pygments)

[Eric Wieser]

Thomas Zhu said:

(Again, analogously python refers to Python 3 by default in Pygments)

For reference, this happened in https://github.com/pygments/pygments/pull/1262

[Eric Wieser]

(deleted)

[Hanson Char]

There is now a new option lean. Don't forget to un-vote and then re-vote above if you changed your mind/preference.

[Jz Pan]

Thomas Zhu said:

Is it possible to have a syntax highlighter that primarily supports Lean 4 but would still try to render Lean 3 correctly? (Analogously, Python 2 and 3 have the same highlighter in Linguist)

I think it's possible since the basic syntax highlighter works based on keywords list, which is mostly the same for Lean 3 and 4...