Live button

Stream: Zulip meta

[Gabriel Ebner]

There used to be a button on every code block to open it in the javascript version of Lean. Does anybody know what happened to it?

#eval "hello, world"

[Mario Carneiro]

the same thing happened on the rust zulip recently. Maybe zulip changed their API and lost the settings?

[Julian Berman]

Probably it's related to https://github.com/zulip/zulip/pull/18212

[Julian Berman]

Which says amusingly:

(Though we'll want to also do some communication with the Lean/Rust communities).

[Julian Berman]

Maybe the fix is now the Lean playground isn't hardcoded in the Zulip codebase and someone just needs to configure it specifically for this one in the Settings pane?

[Mario Carneiro]

Ah, perfect. Indeed the old settings were in the PR, so I copied those into the new settings menu and things should be working.

def zulip := "fancy"

[Eric Wieser]

After refreshing it works on Gabriel's message too. Thanks!