https://live.lean-lang.org/

Stream: general

[Joachim Breitner]

https://live.lean-lang.org/ is neat! How is is set up to contain possibly malicious code? I see that network doesn’t work, and that all file systems are ro from the point of view of the lean process. (run_cmd is quite neat for that :-D)

[Sebastian Ullrich]

See https://github.com/leanprover-community/lean4web/blob/main/server/bubblewrap.sh :) . There may be some extra FRO configuration on top

[Utensil Song]

It makes use of Bubblewrap which is a low-level unprivileged sandboxing tool. The security policies can be configured. Lean 4 Game uses the same technology with similar setup.

[Jason Rute]

I need to update my links. I see you already changed where the link for running block code in Zulip. The Lean community webpage Try it online link probably needs to change. Also do you plan to make the code in the Lean manual (and maybe similar documentation like TPIL and FPIL) runnable via this website? I see the manual code now has greyed out namespace Ex suggesting something like this.

[Sebastian Ullrich]

Unfortunately a hardcoded playground association seems to be one of many mdBook limitations /cc @David Thrane Christiansen

[David Thrane Christiansen]

I'm definitely thinking about the best way to do this in the short and long term, but there's not an immediate plan today

[Utensil Song]

A quick css hack to make https://live.lean-lang.org dark again in case anyone is also interested: https://gist.github.com/utensil/552f47cd687290c1131da0a79cc7dff9

I use it via https://github.com/openstyles/stylus/ .

It looks like this:

image.png

I've tried to cover obvious edge cases, but sure it's not exhaustive.

[Jon Eugster]

@Utensil Song Thank you for the dark theme template! I now added a dark mode setting to the editor. The change is already live at our test-playground: lean.math.hhu.de. I assume it will make its way to live.lean-lang.org too in the next update cycle.

[Utensil Song]

I just noticed that live.lean-lang.org can't copy-paste the full infoview into comment, it will drop anything involves types(maybe widgets), leaving only text, e.g.

image.png

[Jon Eugster]

Interesting. Seems somehow specific to error messages. I opened lean4web#13, as I might not have the time to look into it myself this week.