live.lean-lang.org usage

Stream: Lean for teaching

[Sebastian Ullrich]

Hey everyone, in the recent weeks we've seen increased concurrent use of our live server, usually from a single place such as a university. We are happy of course if it is useful to you! But we are also seeing that about 50 concurrent users slowly get use to some resource limits. To understand how we can improve this service, I'd like to understand better:

• Are you making use of live.lean-lang.org for teaching, or do you know from someone else doing that? If it's more than ~a dozen students, could you let me know the timing of the class so I can correlate it with our logs?
• If so, what is your experience with its performance/stability?

Any other feedback is welcome as well of course!

[Sebastian Ullrich]

In case you're curious, these are the metrics I'm currently looking at, all times UTC:
image.png

The red stuff is not great :), but so far it just means that the server may just run a little slower for each individual user and some sessions may error out and restart when memory is sparse.

[Jireh Loreaux]

@Sebastian Ullrich I'm not sure how many eyes you will get in this stream (despite this being the most natural place for it). You may want to cross-post in general with a link here.

[Sebastian Ullrich]

I didn't want to emphasize the issue too much, let's see if there's enough input here

[Shreyas Srinivas]

I am guilty of using it a lot. But I am not teaching with it. I did get a lot of frequent crashes last week

[Shreyas Srinivas]

A small typo => crash

[Sebastian Ullrich]

Yeah I'm not worried about individual users' resource consumption :)

[Sebastian Ullrich]

But do you feel the crashes are random, and if so could you note down the time of the next occurrence?

[Shreyas Srinivas]

I think I posted quickly after one of those crashes in #lean4

[Shreyas Srinivas]

I don't have a record of times otherwise. My usage usually has two peaks. 21:00-2:00 and 14:00-17:00 German time

[Shreyas Srinivas]

The go to definition feature triggered crashes back to back. But otherwise it was non-deterministic.

[Claudio Sacerdoti Coen]

I must be one of the culprits. My class runs every Wednesday from 13:00 to 17:30 Rome time and we have up to 50 students connected at once.

So far (we started the 25th of September, today is the second week) the experience has been super-good. Very very rarely we get some server issue on a single connection.

My class does not depend on MathLib, so the memory footprint is limited.

[Claudio Sacerdoti Coen]

In case it becomes unbearable on your side I can try to install Lean 4 Web on some local server

[Sebastian Ullrich]

@Claudio Sacerdoti Coen I just realized I never replied to you, we are very happy with having it used in such a way! See https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Using.20Lean.20Live.20for.20a.20tutorial.20session/near/481729302