Zulip Chat Archive

Stream: new members

Topic: Constantly compiling in VSCode


view this post on Zulip Yakov Pechersky (Sep 29 2020 at 20:47):

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.

view this post on Zulip Yakov Pechersky (Sep 29 2020 at 20:48):

image.png

view this post on Zulip Bryan Gin-ge Chen (Sep 29 2020 at 20:52):

What message is it reporting, if any?

view this post on Zulip Yakov Pechersky (Sep 29 2020 at 20:52):

parsing at line 1 [1, 1]

view this post on Zulip Yakov Pechersky (Sep 29 2020 at 20:53):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 29 2020 at 21:00):

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

view this post on Zulip Yakov Pechersky (Sep 29 2020 at 21:00):

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

view this post on Zulip Yakov Pechersky (Sep 29 2020 at 21:00):

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

view this post on Zulip Julian Berman (Sep 29 2020 at 21:01):

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

view this post on Zulip Julian Berman (Sep 29 2020 at 21:01):

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

view this post on Zulip Julian Berman (Sep 29 2020 at 21:01):

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?

view this post on Zulip Yakov Pechersky (Sep 29 2020 at 21:02):

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

view this post on Zulip Yakov Pechersky (Sep 29 2020 at 21:04):

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.

view this post on Zulip Yakov Pechersky (Sep 29 2020 at 21:04):

But I am not sure how to fix that

view this post on Zulip Yakov Pechersky (Sep 29 2020 at 21:30):

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


Last updated: May 16 2021 at 05:21 UTC