## Stream: new members

### Topic: Orange bars never disappear in VSCode

#### Donald Sebastian Leung (May 12 2020 at 08:53):

Not sure if this is just me or due to, e.g. the latest update to VSCode for Lean, but I've just encountered an issue where the orange bars disappear after a second or two when I first load a file in VSCode, but then upon making any modification to the file whatsoever, the orange bars re-appear (as expected) but then don't go away even after a minute or two. I've tried re-running leanproject build via the command line which usually solves the issue by (re-)compiling any mathlib files as necessary, but this time, it doesn't re-compile anything (from mathlib) and doing so doesn't seem to help at all.

For reference, here is my leanpkg.toml:

[package]
name = "lean-kata"
version = "0.1"
lean_version = "leanprover-community/lean:3.7.2"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "ecdb13831d4671eb304c41e78adb5b280c2fc365"}


And my (only) Lean file Solution.lean, under src/:

import group_theory.subgroup algebra.pi_instances

-- This is in Preloaded.lean, so delete before submitting and import Preloaded instead
def Δ (G : Type*) : set (G × G) := { g : G × G | g.fst = g.snd }

instance subgroup_Δ (G : Type*) [group G] : is_subgroup (Δ G) :=
sorry

theorem normal_Δ_iff_comm (G : Type*) [group G] : normal_subgroup (Δ G) ↔ ∀ g h : G, g * h = h * g :=
sorry


#### Johan Commelin (May 12 2020 at 08:57):

I think this sometimes happens if there is a .olean present that doesn't belong to a .lean file. At least I've had such crazy behaviour in the past. I fixed it with

find . | grep '[.]olean' | xargs rm
leanproject get-cache


#### Donald Sebastian Leung (May 12 2020 at 08:58):

That's weird - for the second command (leanproject get-cache), I'm getting "Failed to fetch mathlib oleans"

#### Kevin Buzzard (May 12 2020 at 09:00):

Check your leanproject version, it should be 0.0.6.

Wait

#### Kevin Buzzard (May 12 2020 at 09:01):

Shouldn't it be leanproject get-mathlib-cache?

#### Kevin Buzzard (May 12 2020 at 09:02):

Did all this change recently? You want to get your mathlib oleans. Look at the help for the version you're using and type the appropriate commands to get mathlib oleans without updating the version of mathlib

#### Donald Sebastian Leung (May 12 2020 at 09:04):

Thanks - doing:

$find . | grep '[.]olean' | xargs rm$ leanproject get-mathlib-cache


solved the issue for me.

#### ROCKY KAMEN-RUBIO (May 12 2020 at 15:44):

Glad you worked out the issue!

For anyone else struggling with a similar problem, I just want to add this has happened to me in the following cases:

1. I tried to run a tactic that infinite loops, like ‘’’repeat {rw add_comm}’’’

2. I have too many other errors in my file. This can cause anomalous behavior. There’s a good blog post about this someone linked to that I will try to find.

3. I applied a tactic like ‘’’simp’’’ that takes a REALLY long time to decide it failed, or I’m importing several very large packages and just need to wait a few minutes.

#### Mario Carneiro (May 12 2020 at 16:21):

1. you forgot to compile mathlib or download oleans, or the oleans that are there are out of date, so lean has decided to compile mathlib on the spot. This is always a bad idea because it's a lot of work and the oleans that result from compilation are not even saved for next time

#### Jalex Stark (May 12 2020 at 18:01):

@ROCKY KAMEN-RUBIO I think you mean kevin's post no errors

#### ROCKY KAMEN-RUBIO (May 12 2020 at 18:08):

Jalex Stark said:

ROCKY KAMEN-RUBIO I think you mean kevin's post no errors

Yes! Thank you!

Last updated: May 08 2021 at 04:14 UTC