Lean InfoView loads too slow

Stream: general

[Aishwarya S]

Even for a simple file with a couple of lines of code (importing Mathlib), Lean InfoView takes quite long (like 5-10 minutes) to show the messages. Even after it shows the messages, it again takes the same amount of time to show the messages if I do either Restart Server or Restart File. When VS Code is opened and a file is tried to run, I first see the error: "Error updating: Error fetching goals: No connection to Lean" for about 5-10 minutes, and then it runs fine and shows the messages. What might be the issue?

[Sham S]

not an expert but try a clean build using these commands, maybe the mathlib download is not complete or corrupt. Execute this commands
lake clean lake exe cache get lake build

[Aishwarya S]

Executed these; but still having the same issues. Anyways, thanks for your suggestion.

[Kim Morrison]

Please show us (ideally via a cloneable git repo) your current setup, and exactly what you are doing.

[Aishwarya S]

I am just getting started with Lean and have only a few trial files in my project folder. The files I have in my project folder have been uploaded at this repository: https://github.com/AishwaryaS-561/Lean-setup.git
Lean InfoView takes too long to load and show messages for each of the .lean files in this folder, when I try to run them in VS Code. I really appreciate any help. Thanks in advance!

[Sebastian Ullrich]

What is your operating system? If you have a virus scanner, try disabling it temporarily

[Michael Rothgang]

Are you on Windows? If I understand correctly, a known issue is that loading the infoview for the first time can take a while on windows. (After it's loaded, opening a second file is fast, however.)

[Aishwarya S]

Yes. I am using Windows. It does take a while to load for the first time. However it also takes long whenever I open a file. I see the rotating symbol (spinner) which says "Updating ..." if I take the cursor near it. It takes too long to go away.

[Marc Huisinga]

I tried to reproduce this on a Windows machine with your repository, but no luck unfortunately (everything loads after a couple of seconds).

Some more questions:

• Are you using an anti-virus of some kind?
• Are you on a university machine by any chance, or using a setup with a networked drive?
• Is your project folder connected to a cloud provider (e.g. OneDrive, Google Drive, Dropbox, etc.)?

I'd also be interested in the output of the 'Show Setup Information' command (Forall menu > Show Setup Information).
image.png

[Aishwarya S]

My PC has McAfee Security Scan Plus, which seems to be installed by my university since they manage it remotely through IT policy. I could neither find an option to disable it nor uninstall it. When I try to uninstall, it gives a pop-up message "We couldn't create the data directory". Need to see what can be done about it.
I am not using any setup with a networked drive. Also, my project folder is not connected to a cloud provider.
I get the following output for 'Show Setup Information':
Operating system: Windows_NT (release: 10.0.26200)
CPU architecture: x64
CPU model: 4 x 11th Gen Intel(R) Core(TM) i5-1135G7 @ 2.40GHz
Available RAM: 8.25 GB

VS Code version: Reasonably up-to-date (version: 1.106.3)
Lean 4 extension version: 0.0.221
Curl installed: true
Git installed: true
Elan: Reasonably up-to-date (version: 4.1.2)
Lean: Reasonably up-to-date (version: 4.26.0-rc2)
Project: Valid Lean project (path: c:\Users\s.aishwarya\Desktop\Desktop Folder\My Lean Projects\MyFirstLeanProject)
Active Lean version: leanprover/lean4:v4.26.0-rc2 (set by file://%3F/c%3A/Users/s.aishwarya/Desktop/Desktop%20Folder/My%20Lean%20Projects/MyFirstLeanProject/lean-toolchain)
Installed Lean versions: leanprover/lean4:v4.19.0, leanprover/lean4:v4.20.0-rc5, leanprover/lean4:v4.22.0-rc3, leanprover/lean4:v4.26.0-rc2

Thanks!

[Shreyas Srinivas]

The antivirus is almost certainly the problem

[Kevin Buzzard]

Can you tell the antivirus not to scan the directories containing your lean project and where windows puts the lean binaries?

[Alfredo Moreira-Rosa]

Ask your IT department if there is a whitelisted directory for your anti virus scanner, or at least one where there is a policy to scan on schedule instead of live (like at lunch time).
The answer is usually no, but i know some companies that do it, so it's not out of hope.

[Emilio Jesús Gallego Arias]

Would it be feasible for Lean to detect that it is over a slow filesystem (virus scanner, network) and provide a warning to the user?

[Henrik Böving]

We did investigate detection of networked drives in the past. While it seems somewhat feasible at linux our friends at apple told us there is no real way to do it consistently for every provider and its even less clear on Windows. So the only thing we could do here is likely exhaustive enumeration of providers.

Similarly for virus scanners they all have unique means. Note that virus scanners might in particular be a little suspicious of a program that starts to poke around for a virus scanner.

[Aishwarya S]

Even after changing the scan schedule in McAfee Security Scan Plus to Weekly, the problem did not go away. So McAfee could not have been causing the issue.
Later I saw that there is also Sophos Endpoint Agent which could have been causing the issue. I tried running one of the simple .lean files again, while keeping a watch on Sophos in Task Manager. I noticed that Sophos was running for quite long (about 10 minutes) and then Lean InfoView finished loading just a couple of seconds after Sophos almost finished its job. Looks like Sophos must have led to the issue. Will try to exclude Lean related files from Sophos scan and will update on this matter.
Thank you very much everyone for the suggestions.