Data.List.Basic is a server stress test

Stream: lean4 dev

[Mario Carneiro]

I've been working on Mathlib.Data.List.Basic which is a 5000 line lean file, and it might be helpful to use it as a test case for the server interactivity. The current issue that I am running into is that if you make a modification in the middle of the file like #print foo, there is approximately a 3 second pause before anything happens, after which point the command is executed and the loading indicator runs off to start processing later commands. So I'm guessing this is the cost of parsing the file?

[Sebastian Ullrich]

Interesting. Parsing is incremental, so that shouldn't be it.

[Kevin Buzzard]

I was observing the same thing earlier today with Mathlib.Data.Set.Lattice, a meagre 2500 lines long. I'd change something, there would be a short pause with no orange bars, and then all of a sudden the change would magically kick in. The file compiles super-fast because it's very low-level stuff. I just got used to it.

[Gabriel Ebner]

there is approximately a 3 second pause before anything happens

I've also noticed this, and I believe it started with lean4#1884. We now sleep 200ms before producing the header snapshot for the next document version, and the next time we process a change we need to wait for the header snapshot from the previous version AFAICT. So (delay = 200ms * number of changes within 200ms) or something.

[Johan Commelin]

So if you type fast you get extra punishment? :wink:

[Sebastian Ullrich]

I thought I had considered this scenario... perhaps I hadn't thought hard enough