Zulip Chat Archive

Stream: Zulip meta

Topic: Lean playground link dead

Eric Wieser (Mar 12 2023 at 21:10):

The "View in Lean playground" link in this code block is dead

-- click the arrow in the top right

should we just remove it?

Scott Morrison (Mar 13 2023 at 05:18):


Kevin Buzzard (Mar 13 2023 at 11:25):

Works for me: sends me to https://lean.math.hhu.de/#code=--%20click%20the%20arrow%20in%20the%20top%20right%0A or https://leanprover-community.github.io/lean-web-editor/#code=--%20click%20the%20arrow%20in%20the%20top%20right%0A, both of which seem to be working fine. What's the problem here?

Kevin Buzzard (Mar 13 2023 at 11:27):

-- click the arrow in the top right

Sebastian Ullrich (Mar 13 2023 at 11:27):

Scott removed a third option linking to leanprover.github.io that was broken

Last updated: Dec 20 2023 at 11:08 UTC