Zulip Chat Archive

Stream: new members

Topic: Orange bars everywhere


view this post on Zulip Bhavik Mehta (Jun 03 2020 at 02:58):

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?

view this post on Zulip Bhavik Mehta (Jun 03 2020 at 02:58):

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

view this post on Zulip Mario Carneiro (Jun 03 2020 at 02:59):

Most likely the trigger is a hover request

view this post on Zulip Bhavik Mehta (Jun 03 2020 at 02:59):

Why would that make things recompile?

view this post on Zulip Mario Carneiro (Jun 03 2020 at 03:00):

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

view this post on Zulip Mario Carneiro (Jun 03 2020 at 03:00):

which it needs to provide some precise location information

view this post on Zulip Kevin Buzzard (Jun 03 2020 at 07:08):

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

view this post on Zulip Kevin Buzzard (Jun 03 2020 at 07:08):

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

view this post on Zulip Bhavik Mehta (Jun 03 2020 at 12:22):

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

view this post on Zulip Kevin Buzzard (Jun 03 2020 at 16:27):

And are you using a mouse and hovered accidentally?

view this post on Zulip Bhavik Mehta (Jun 03 2020 at 16:29):

Nope, I was in the middle of typing


Last updated: May 11 2021 at 14:11 UTC