Slow to update InfoView status

Stream: new members

[Luiz Kazuo Takei]

I am going through MIL (Mathematics in Lean) and I am enjoying it a lot.

But there's one issue that I find annoying. Every time I make a slight change to the code, the Lean InfoView starts updating the status and this can take a long time. For instance, I just added a gcongr call and it took ~5 minutes to complete the update.

Is this normal? Is there something I can do to speed up this update process?

[Michael Rothgang]

That's not normal; something's not set up right.

[Michael Rothgang]

Does just the infoview take a long time, or also your code recompiling. In VS Code, you see orange bars every time you update a proof and Lean re-checks it. Do they also take so long?

[Luiz Kazuo Takei]

Well, this issue with gcongr does not happen very often: this was an extreme case. Usually it takes a few seconds. I guess this is normal?

Also, when I open a new file (within the same MIL project), it always takes a few minutes for the Lean InfoView to finish whatever it has to do to properly display the goals. Is this normal? (So I usually ask VSCode to open it and go do something else for a bit...)

[Michael Rothgang]

No, that's not normal either.

[Michael Rothgang]

Can you provide some more details about your situation= It's hard to diagnose this remotely without knowing anything particular about your situation.

[Michael Rothgang]

For instance, what does Lean do in those few minutes? Do you see your computer running hot (as if it's building all of mathlib)? Do you get blue messages "building file X/Y", and you're slowly re-building mathlib? (That would be slow, but that can also be fixed.)

[Michael Rothgang]

Are you on windows and your anti-virus is kicking in? (If so, try disabling it on the directory of MIL and see if that fixes the issue.)

[Aaron Liu]

this happens to me too I thought it was normal

[Aaron Liu]

maybe I need to use #exit more often

[Luiz Kazuo Takei]

When I open a new file, I just see that rotating circle and if I hover my mouse over it, it just says "Updating..."

I didn't see any message saying "building file X/Y"... I am on Windows and next time I will check if the anti-virus is doing something...

I was not aware of #exit but I will certainly try that too when I have these issues again.

Thanks for the tips!