Orange bars everywhere

Stream: new members

[Bhavik Mehta]

Recently I've been getting more orange bars than I used to, and it's not consistent or reproducible - but every now and then while I'm in the middle of a proof I'll get orange bars on every file in my project, which take the usual compilation time to go away. Any ideas what's going on?

[Bhavik Mehta]

It's usually when I'm in tactic mode writing a proof - no changes to any other files or mathlib, but other files which this one depends on also recompile

[Mario Carneiro]

Most likely the trigger is a hover request

[Bhavik Mehta]

Why would that make things recompile?

[Mario Carneiro]

I'm not entirely sure, but I believe this is Lean switching from the olean version to the in memory version of the dependent file

[Mario Carneiro]

which it needs to provide some precise location information

[Kevin Buzzard]

There has been some chat about this, with comments such as "can be fixed by closing all the lean files you have open in your VS code apart from the one you're working on" (a workflow-breaking solution) or "works as expected". Kenny asked how to open a file in notepad mode at some stage, by which he meant how to look at a file without triggering a risk of orange bars. I agree that something is wrong but I haven't worked out how to reproduce or what I'm doing to cause it

[Kevin Buzzard]

I am a bit scared that some people think nothing is wrong

[Bhavik Mehta]

I didn't have any other lean files open when this happened, and I wasn't trying to look at a different file! I was just writing a proof like normal

[Kevin Buzzard]

And are you using a mouse and hovered accidentally?

[Bhavik Mehta]

Nope, I was in the middle of typing