editing lower level files

Stream: general

[Jireh Loreaux]

I recently went to edit a file which is (presumably) lower in the mathlib hierarchy, namely group_theory/group_action/units. Even though I had downloaded the mathlib cache, as soon as I edited this file vscode (more precisely OSS Code) started a live rebuild of mathlib, which quickly runs me out of memory (8 GB). I understand that vscode is trying to rebuild all of the files which depend on this. So, how can I both edit the file and get more timely response from Lean? Is there a way to prevent it rebuilding everything and only check that the present file compiles (based on the existing oleans on which it depends from the cache)?

[Kalle Kytölä]

I have had similar issues recently, so would also appreciate advice!

In #9430 I moved a few lemmas to topology.metric.basic, and I had to commit, push, pull, get cache (and close and reopen editor) to get back to normal. I then moved another lemma to topology.continuous_function.bounded, and I'm yet to restore a working cache.

Is there something that I or both of us are doing wrong or could be doing differently when editing these files that are imported in many others?

[Kalle Kytölä]

Just in case this is relevant information regarding the problem, after pushing the most recent commit moving a lemma, I got an error in build mathlib check:

Build succeeded, but the following files were noisy:
src/measure_theory/measure/finite_measure_weak_convergence.lean

[Frédéric Dupuis]

What I usually do in this situation is to close all files except for the low-level one I'm working on. Then, when that file compiles, I would execute lean --make src/path/to/high/level/file.lean to compile back up to the high level file I want (this is usually quite a bit faster than a full rebuild), and only then reopen the high-level file in VSCode.

[Kalle Kytölä]

Thank you very much for the advice!

(I didn't yet get to try it out --- I was in the middle of another commit, push, pull, get cache, reopen editor solution. It also worked again, but Frédéric's solution looks much better.)

[Jireh Loreaux]

I get this problem even if the low-level file is the only one open, and the only one edited. This is reproducible for me. Checkout master, get cache, edit low level file, attempts to rebuild all of mathlib.

[Kalle Kytölä]

For me the orange side bar moves quite fast in the files lower in the import hierarchy. My understanding was that Frédéric's solution can be applied as soon as one knows that the lower level file is without errors. (My "solution" also works in that case, but is probably not the recommended one: it indeed builds all of mathlib, although not locally.)

[Rob Lewis]

Jireh Loreaux said:

I get this problem even if the low-level file is the only one open, and the only one edited. This is reproducible for me. Checkout master, get cache, edit low level file, attempts to rebuild all of mathlib.

At the bottom of VSCode there's something like "Lean: :check: (checking visible files)". If this says "project files" instead, there's your problem.

[Jireh Loreaux]

I think, despite my insistence that I only had that file open, that I also had the higher level file open in a separate vscode instance. So likely @Frédéric Dupuis has the solution for me, but thanks for that tip also!

[Yury G. Kudryashov]

Another tip: if you use --old option in your lean command line, then it will not recompile all the files between the changed one and the opened one.