Constantly compiling in VSCode

Stream: new members

[Yakov Pechersky]

I've had an issue recently that a project (actually several) have been constantly in "blue squiggly state" if they import any mathlib file. I even purged a project, did leanproject get ... again, and still have this. I've restarted Lean, did leanproject get-m, checked that the subrepo matches the toml commit hash, not sure what else to do.

[Yakov Pechersky]

image.png

[Bryan Gin-ge Chen]

What message is it reporting, if any?

[Yakov Pechersky]

parsing at line 1 [1, 1]

[Yakov Pechersky]

I take it it is recompliing mathlib, given that mem usage is above 10G now

[Bryan Gin-ge Chen]

What's the structure of your repo? Do you have it on github so we can try to reproduce your issue?

[Yakov Pechersky]

https://github.com/Julian/lean-across-the-board

[Yakov Pechersky]

but I think this might a "my system" issue because I am having this for other repos as well. Not sure what changed.

[Julian Berman]

(I don't currently have the issue, so whatever is happening yeah may be tricky to reproduce just from cloning)

[Julian Berman]

The other thing I was gonna say is I think when I was in similar states before I ran leanpkg build maybe?

[Julian Berman]

Not sure if that' s a thing you're "supposed" to do or not (maybe leanproject build instead?) but yeah does that do anything? At least show you explicitly what it's building?

[Yakov Pechersky]

In my main mathlib clone, git checkout master; git pull; leanproject get-cache has it without blue squiggles

[Yakov Pechersky]

I think what might have happened is a that mix of using msys git bash and wsl bash has made the mathlib oleans live somewhere unexpected for the VSCode extension.

[Yakov Pechersky]

But I am not sure how to fix that

[Yakov Pechersky]

Seems to be "fixed" if I use VSCode in WSL Remote mode.