web editor questions

Stream: general

[Kevin Buzzard]

So now we have https://lean.math.hhu.de/ , a lean 4 web editor. I am currently on mobile and I would love to be able to just click on something which jumps me from code posted in Zulip directly to the same code in the web editor on my phone. On the desktop app there is a link on every code block which might do this (I haven't clicked on one on them in years because when I'm on desktop I just cut and paste into lean locally). Can this be made to work for mobile?

Will the web editor stay at this German link or will it be adopted by lean-lang? Or will there be rival editors like in the lean 3 days (one mathlib compatible and one not :-/ )?

Finally, I just tried to run some lean code posted on Zulip, on mobile, by manually copying the entire message into the web editor and I got a "read only file system" error with import Mathlib. Is something broken?

[Yaël Dillies]

It has already been adopted, right? https://live.lean-lang.org/

[Kevin Buzzard]

Oh nice, that answers two questions. Now can I click on code in Zulip and jump straight there? I am excited about basic lean and mathlib functionality on mobile

[Mario Carneiro]

Maybe this thread should move to #Zulip meta since that's a zulip feature suggestion

[Mario Carneiro]

well, at least one part is - you asked 3 different questions there

[Kevin Buzzard]

Yes but the other two are now moot. I'm not sure if I can move it on mobile, I'll ask again.

[Mario Carneiro]

lol that's another feature suggestion

[Jon Eugster]

Kevin Buzzard said:

Will the web editor stay at this German link or will it be adopted by lean-lang? Or will there be rival editors like in the lean 3 days (one mathlib compatible and one not :-/ )?

Adding to Yael's answer, we will keep our version at lean.math.hhu.de up and running and use it as a dev-server to test new features (for example it has now dark mode), but the official playgroud is live.lean-lang.org and if there are any links to our server remaining, they should probably be adapted.

[Jon Eugster]

Kevin Buzzard said:

Finally, I just tried to run some lean code posted on Zulip, on mobile, by manually copying the entire message into the web editor and I got a "read only file system" error with import Mathlib. Is something broken?

Can you try to file an issue on github.com/leanprover-community/lean4web/issues so I can try to reproduce this? Did you copy more than just the code? I think Zulip mobile only copies the entire message.

[Alexander Bentkamp]

I could reproduce the "read only file system" error. It should work now.