slowdown on initial use

Stream: general

[Kenny Lau]

I don't know how to diagnose this, but basically I observe that on the initial use of a file (i.e. compiling the "import" lines) it is slower than the web editor, even though the rest of the time it's way faster than the web editor. I read Kevin's thread and thought maybe it's to do with windows defender so I turned it off for the folder but initial loading is still slow. Maybe I need to restart to see if it has any effect? How else do I diagnose the problem?

[Robin Arnez]

One hypothesis I have is that reading olean files is a bottleneck

[Malvin Gattinger]

Maybe the web editor is running Lean with some optimization tricks, such as always keeping the .oleans of all of Mathlib in RAM instead of reading from a disk?

[Kevin Buzzard]

Did you try turning Windows Defender off for not just the folder but for your entire home directory? Turning it off for the repo alone was not enough for me and I didn't do any experiments with seeing exactly what I could get away with, my experiments have been focussed on trying and failing to make the problem come back after I did this. Note that I can quite imagine that lake build is accessing files in e.g. .elan (for sure) and for all I know .cache/mathlib too.

[Kenny Lau]

I could do that, but I imagine it would be also helpful to know which folders exactly does Lean use?

[Kevin Buzzard]

Hmm, I just tried to be helpful by seeing if just telling Windows Defender to ignore /Users/buzzard/.elan instead of /Users/buzzard would still leave me in my state of ecstasy, but I am sufficiently incompetent with macs to know how to tell windows defender to ignore a hidden directory.

[Henrik Böving]

Malvin Gattinger said:

Maybe the web editor is running Lean with some optimization tricks, such as always keeping the .oleans of all of Mathlib in RAM instead of reading from a disk?

The Linux kernel does that trick for you without help from us.

[Henrik Böving]

I would hope windows has a file cache as well but I don't know

[Alfredo Moreira-Rosa]

Windows has memory mapped files, but i don't know if lean code takes advantage of that.

[Henrik Böving]

Memory mapped files is not the topic here but yes we do make use of them.