memory issue

Stream: maths

[Arthur Paulino]

@Kyle Miller Hello! How much memory should I expect for some of those simple_graph files to consume? 3.5Gb+? Or am I doing something wrong?

[Yaël Dillies]

Oh no! Certainly not!

[Yaël Dillies]

Did you download caches using leanproject get-cache and then restart the server?

[Arthur Paulino]

I did. This one, for instance, is already at 1.6Gb and going up image.png

[Arthur Paulino]

reached 2.6Gb and I killed it

[Yaël Dillies]

Did you avoid modifying files far earlier in the import tree?

[Arthur Paulino]

Yeah, files are intact

$ git status
No ramo walks_and_trees
Your branch is up to date with 'origin/walks_and_trees'.

nothing to commit, working tree clean

[Mario Carneiro]

what does leanproject check say?

[Arthur Paulino]

$ leanproject check
Some mathlib oleans files seem older than their source.
Do you want to set their modification time to now (y/n) ?

[Mario Carneiro]

that's bad

[Arthur Paulino]

maybe because I did get-cache on master?

[Yaël Dillies]

Ah yes!

[Yaël Dillies]

You need to do get-cache on the branch you want. Oleans files differ from branch to branch.

[Mario Carneiro]

note that you should not follow check's advice and change the modification times on the oleans, this is basically lying to lean about the olean files and can cause files to have missing theorems and such

[Mario Carneiro]

it's an okay thing to do if you just want to get out of orange bar hell but it has side effects

[Arthur Paulino]

I had done get-cache on master, but then I did get-cache on this branch

[Patrick Massot]

Mario Carneiro said:

note that you should not follow check's advice and change the modification times on the oleans, this is basically lying to lean about the olean files and can cause files to have missing theorems and such

This is actually an outdated advice, from the time when Lean was using timestamps to decide what to recompile

[Patrick Massot]

Ths whole check command is outdated.

[Mario Carneiro]

It's using hashes now, I guess? Is there an analogous check to do?

[Mario Carneiro]

the analogous override would be lean --old I guess

[Arthur Paulino]

I'm cloning mathlib again. won't call leanproject build this time and will go straight to the branch and call leanproject get-cache

[Arthur Paulino]

I will eventually understand these things

[Arthur Paulino]

Was get-cache supposed to solve any of these issues related to olean files out of sync though?

[Yaël Dillies]

Yup, that's what it does. But you need to do it on the correct commit (it looks automatically for the latest commit on a branch) and restart the server afterwards.

[Arthur Paulino]

Okay, then something went wrong. I will try again and see what happens. I'm starting from a clean clone of mathlib

[Arthur Paulino]

This seems to be something related to some specific lean files