Lean in Visual studio code using Math Lib perfromance

Stream: new members

[Leo Shine]

I've been working trhough the exercices in the Mathematics in Lean book (which imports Mathlib) but every so often the whole thing gets stuck and I have to restart the lean server, it seems to take multiple minutes to get this all working again. What do people think the performance of e.g. restarting the lean server in this sort of file should be? Am I missing something that I should have done to make this faster. I can't find any logs that are doing anything in VS code and the lean.exe process doesn't seem to be doing anything with CPU but is reading something from the disk

[Shreyas Srinivas]

This issue is a problem with some runaway processes and threads which will hopefully be fixed in the near future. See this github issue and linked threads: https://github.com/leanprover/vscode-lean4/issues/305

[Leo Shine]

Does the startup time seem reasonable? It sometimes also have messages like "info: [798/1637] Building Mathlib.GroupTheory.Subsemigroup.Basic" or whatever so I'm wondering if I've missed something that would cache the build of MathLib or something like that

[Leo Shine]

Also are there any workarounds that make this more reliable somehow?

[Alex J. Best]

That doesn't sounds good. Try closing vscode and ending all lean processes running, then run lake exe cache get from the terminal within the Mathematics in lean directory

[Alex J. Best]

This should download cached build files that are stored online so your computer doesnt need to build them

[Leo Shine]

hmm it says "
No files to download
Decompressing 3678 file(s)
unpacked in 57589 ms
"
Does that mean it thinks it has already downloaded them? Or does it mean it can't find them?

[Kyle Miller]

Here's what I do when everything seems to be going very wrong. First I do the Lean 4: stop server command from within VS Code. After that, in the terminal:

killall lean # or pkill if you in an environment like Gitpod
killall lake # not sure if this is necessary, but I don't want it to feel left out
lake clean
lake exe cache get! # the ! is probably not necessary after a clean

Sometimes at this point I do lake build to be sure that the cache is actually picked up. This might build a couple things, but it should be at most a minute. Only after all of this do I do Lean 4: restart server in VS Code.

[Leo Shine]

Also could this be caused by using a nightly version of lean

[Kyle Miller]

Yes, depending on what you mean. Could you give the contents of the lean-toolchain file and the output of lean --version from within the project root?

[Kyle Miller]

(You might have nightly lean installed, but the lean-toolchain file is meant to control which version actually gets used for your project. If you use lean/elan installed by your OS package manager, you can end up in a situation where the OS lean always gets used, which is not good.)

[Leo Shine]

both seem to say "leanprover/lean4:nightly-2023-08-23" and "Lean (version 4.0.0-nightly-2023-08-23, commit 216d2460e0ad, Release)"

[Leo Shine]

lake exe cache get doesn't seem to have made this sort itself out quick so going to try your thing

[Leo Shine]

Hmm wonder what I've done wrong, this seems significantly better in gitpod

[Kevin Buzzard]

What does git status report?

[Leo Shine]

Okay it's definitely better having cleaned the cache

[Leo Shine]

git status just shows a 5 or so of the modified exercise files I've been doing

[Kevin Buzzard]

(although I think the recommended workflow is to copy all the exercise files and work on the copied files)

[Shreyas Srinivas]

One of the 4.1 release candidates had a buggy cache. This should be fixed with 4.2
Leo Shine said:

Also could this be caused by using a nightly version of lean

[Kyle Miller]

(@Shreyas Srinivas Leo appears to be using a nightly for 4.0 that MIL wants -- does this buggy cache issue apply pre-4.1?)

[Shreyas Srinivas]

Probably not. I used this toolchain and had no trouble with cache. I see two separate complaints in what Leo is saying.

1. Start up time because vscode is building mathlib from scratch. In that version the most likely reason is that the lean-toolchain mismatch between mathlib and the project. But once the cache is messed up, it is best to clean ~/.cache/mathlib. I am not sure lake clean does that or get! has any effect on that folder.
2. The extension grinding to a halt while being used. This is about the runaway threads and processes when one types in imports (this one is about processes). We discussed this before and the thread is in the issue I linked.

[Mario Carneiro]

use lake exe cache clean or lake exe cache clean! to clean up ~/.cache/mathlib

[Leo Shine]

Thanks everyone, definitely feels like the lake exe cache clean has helped, but yes also a separate issue with why it grinds to a halt and for whatever reason the gitpod thing is definitely significantly faster than whatever I've got set up on my local machine

[Shreyas Srinivas]

Leo Shine said:

Thanks everyone, definitely feels like the lake exe cache clean has helped, but yes also a separate issue with why it grinds to a halt and for whatever reason the gitpod thing is definitely significantly faster than whatever I've got set up on my local machine

It is possible that gitpod kills off excessively resource consuming processes to maintain resource limits.