Changing the default syntax highlighter to lean4

Stream: Zulip meta

[Eric Wieser]

Can an admin change the default syntax highlighter (at the bottom of https://leanprover.zulipchat.com/#organization/organization-settings) to lean4?

[Eric Wieser]

(and also the playground link at https://leanprover.zulipchat.com/#organization/playground-settings, leaving the lean3 editor on lean3 but changing the lean4 one to lean4)

[Eric Wieser]

Test:

-- lean3
abbreviation is_lean3 := sorry
abbrev is_lean4 := sorry

-- lean4
abbreviation is_lean3 := sorry
abbrev is_lean4 := sorry

-- lean
abbreviation is_lean3 := sorry
abbrev is_lean4 := sorry

-- default
abbreviation is_lean3 := sorry
abbrev is_lean4 := sorry

(this won't update when you change the settings, but you can quote it and the quoted version will)

[Kim Morrison]

It looks like the default language for code blocks is already set to lean4.

[Sebastian Ullrich]

done

Eric Wieser said:

Test:

-- lean3
abbeviation is_lean3 := sorry
abbrev is_lean4 := sorry

-- lean4
abbeviation is_lean3 := sorry
abbrev is_lean4 := sorry

-- lean
abbeviation is_lean3 := sorry
abbrev is_lean4 := sorry

-- default
abbeviation is_lean3 := sorry
abbrev is_lean4 := sorry

(this won't update when you change the settings, but you can quote it and the quoted version will)

[Sebastian Ullrich]

...so why did the Lean 3 highlighting change :)

[Sebastian Ullrich]

And the Lean 3 playground didn't seem to trigger before or after? I guess it's not really important anymore

[Eric Wieser]

It didn't, I made a typo and fixed it while you were quoting

[Eric Wieser]

What I don't get is why the lean3 playground links don't work

[Eric Wieser]

Maybe it needs "lean" instead of "lean3" as the language name

[Eric Wieser]

(our messages are crossing because I am on lousy internet)

[Eric Wieser]

Can we try changing this to "lean" and see if that makes the playground work? It's occasionally useful to compare to lean3 behavior, so if it's an easy fix I think we should make it work with Zulip.

image.png

[Kim Morrison]

Okay, done. I'll let you test. :-)

[Eric Wieser]

Yep, it works!

[Eric Wieser]

(on the previous messages above)

[Eric Wieser]

I wonder what this does to old messages...

[Eric Wieser]

Answer: old messages now link to the lean3 playground, which isn't what we want. Maybe the answer here is to list both playgrounds for Lean, and list only the lean4 playground for lean4. Old messages will present the user with a choice, but I think that's fine - especially as many really old messages really are lean3!

[Eric Wieser]

If you edit the old message, it will of course switch to the new highlighting and new playground link

[Kim Morrison]

Like so?

[Eric Wieser]

Yep, looks good: thanks!