Zulip Chat Archive

Stream: Zulip meta

Topic: Lean3 codeblocks open the lean4 web editor

Eric Wieser (Dec 18 2023 at 00:56):

This is marked as lean3:

#check 1

but the link goes to the wrong live editor

Eric Wieser (Dec 18 2023 at 00:57):

However, the Zulip config looks correct:

image.png

Eric Wieser (Dec 18 2023 at 01:14):

I think this is probably because Zulip is resolving aliases, but it would be helpful here if it didn't...

Eric Wieser (Jan 17 2024 at 13:59):

This will be fixed by the next Pygments release, where lean4 is no longer an alias

Last updated: May 02 2025 at 03:31 UTC