Lean running very slowly

Stream: new members

[Fingy Soupy]

I recently divided a large file I have into several smaller files and now Lean is running very slowly and often times out. It also frequently consumes a large amount of memory 4gb+
I'm wondering if there are some common performance pitfalls or an easy way to profile to find out what change led to the drastic decrease in performance

Some notes:

• I am using mathlib, installed with leanproject
• I have Lean set to "check visible files and above"

[Kyle Miller]

One thing you can do is compile olean files, which are caches of pre-processed Lean code. For example, lean --make src if src is the directory containing all your lean files, or lean --make path/to/specific/file.lean.

[Yaël Dillies]

The most important question is "Was it a leaf file (not imported much) or a basic file (imported by a big proportion of mathlib?", or maybe the auxiliary question "Is it one of your files or is it in mathlib?".

[Kyle Miller]

I find I usually need to restart the editor's Lean process for it to pick up the new olean files, rather than it trying to recursively process every file itself.

[Fingy Soupy]

I will try recompiling, thanks.
I'm only editing files in my own project, I haven't changed mathlib