What is the expected memory consumption

Stream: general

[Johannes C. Mayer]

When I load data.real.basic I get already around 4GB of memory consumption. When I browse some files I get even more. I just tried to open the LTE (with no other projects open) and lean says excessive memory consumption when I open the condensed/ab.lean file. My system tells me that LEAN now uses over 20GB of RAM. Is the fix really to just increase the memory limit even further? Right now it is set to 16GB. This is in the VS-code extension with the setting checking visible files, and only condensed/ab.lean is visible (the only open file in fact).

[Johannes C. Mayer]

This is in LEAN3 on linux.

[Mario Carneiro]

do you have mathlib oleans downloaded? That sounds excessive

[Johannes C. Mayer]

I did run leanproject get leanprover-community/lean-liquid. Does this get me the oleans?

[Mario Carneiro]

for LTE I don't know if they are shipping oleans so you probably have to lean --make src in the project

[Johannes C. Mayer]

Ok, I will try this. Is it normal to get 4GB of RAM full by importing data.real.basic though?

[Mario Carneiro]

browsing a big project when there are no oleans on disk is usually a bad idea because lean will compile everything on the spot and not save the results, meaning wasted work and huge memory consumption

[Johannes C. Mayer]

But for data.real.basic I should have the oleans probably right (when I just create a new project with leanproject new NAME)? How can I check this?

[Mario Carneiro]

I just tried opening data.real.basic without anything else open and with precompiled mathlib oleans. I'm seeing 1108M virtual memory and 602M resident memory in htop

[Mario Carneiro]

Opening it in vscode should take about 1 second load time. It's usually really obvious when something is not compiled because this jumps to more like 40 seconds

[Mario Carneiro]

or potentially hours if it's something really deep in the hierarchy

[Mario Carneiro]

There is leanproject check which can be used to check for uncompiled oleans, but I think @Patrick Massot mentioned that it doesn't work anymore because lean changed its caching strategy

[Johannes C. Mayer]

Ok, actually it seems to only take long in one of the projects that I have. So somehow the oleans probably got messed up there, and I just need to just build them again. I assume that lean --make src would reuse already existing oleans from what you were saying.

[Mario Carneiro]

yes, lean --make src will exit immediately if everything is compiled so that's another way to check for uncompiled stuff

[Johannes C. Mayer]

It seems that the .olean files are put in the same directory as the source code. So I guess you could just try to find .lean files, that do not have a .olean file in their directory. Or can some .olean get into an invalid state, where they are there, but no longer used?

[Anne Baanen]

Yes, if you change a .lean file, the .olean file, and also the .olean file for all the files depending on the changed .lean file, is out of date and can't be used.

[Patrick Massot]

leanproject check simply checks that olean files are not older than the corresponding lean files.

[Johannes C. Mayer]

For example, what happens when I put a #check into a mathlib lean file? I think I have done that, that was probably the problem right?

[Patrick Massot]

Oh yes!

[Patrick Massot]

That would definitely create huge problems

[Johannes C. Mayer]

Ok, now everything seems to make sense :sweat_smile:

[Patrick Massot]

We would love if Lean could be smarter when deciding what to recompile. But this is a very tricky issue because a lot of things are very non-local.

[Johannes C. Mayer]

I guess that would be good. Although for me the issue was that I just did not know how the compiler handles things. Probably that was mentioned somewhere and I missed it. But if not maybe it makes sense to mention it more explicitly that changing anything in the _target folder is a bad idea, or at least that they should run lean --make src afterward. I know at least one other person who also very likely ran into this issue.

[Mario Carneiro]

If you add a #check and then delete it or undo to before you added it, I think the cache will still be good

[Mario Carneiro]

although you might need to restart the server to make it reload the cache from disk

[Johannes C. Mayer]

What if I add whitespace or a newline. That might be hard to detect.

[Mario Carneiro]

what I said applies to any textual change

[Mario Carneiro]

if you restore the file to be byte-wise identical to the original, then the file hash will come out the same and the cache will not be invalidated

[Mario Carneiro]

whitespace changes will invalidate the cache just as much as anything else

[Mario Carneiro]

unless it's a trailing whitespace and you have trim whitespace on save in vscode (which is enabled by default in mathlib)

[Johannes C. Mayer]

Ok, so I guess undo would work always, and trying to delete it would fail often when you make large changes because you would likely miss some whitespace. Good to know.

[Alex J. Best]

There is a discussion about this on zulip from a couple of weeks back, @Johan Commelin wanted to make target read only or at least add some warning to the extension when you edit (I can't find the link right now when I'm on mobile). I definitely think an alert message when you start editing target warning not to save any changes and to close the tab and restart lean when done #checking would help people avoid this

[Alex J. Best]

Of course this message should have a "never show again" checkbox so people who want to edit _target files don't get annoyed by it every time!

[Johannes C. Mayer]

That seems like a very good idea.

[Johannes C. Mayer]

At least for new people, it could save them some headaches.

[Johannes C. Mayer]

The pernicious thing that happened to me actually seems especially bad. I actually thought that it was normal for data.real.basic to load so long, because although I invalidated some .orlean files related to it, it was still not so slow that it was obviously not intentional. (It took like 15s or so I think).

[Johannes C. Mayer]

And only when I tried to open the LTE did I run against the wall of nonunderstanding hard enough to realize that it exists.

[Stuart Presnell]

Is there a general troubleshooting page for questions like this? The main advice I’ve seen on the mathlib web pages is “ask on Zulip”.