Orange bars never disappear in VSCode

Stream: new members

[Donald Sebastian Leung]

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]

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]

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

[Kevin Buzzard]

Check your leanproject version, it should be 0.0.6.

[Kevin Buzzard]

Wait

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

Thanks - doing:

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

solved the issue for me.

[ROCKY KAMEN-RUBIO]

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]

4. 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]

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

[ROCKY KAMEN-RUBIO]

Jalex Stark said:

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

Yes! Thank you!