download repository

Stream: new members

[Alex Zhang]

I accidentally deleted my original copy for PR #8289; how can I redownload this repository and link the download one to this one?
@eric-wieser

[Johan Commelin]

@Alex Zhang I any random copy of mathlib, write: git pull, and then git checkout your-branch-name

[Alex Zhang]

Thanks, Johan! I will try.

[Alex Zhang]

Why am I experiencing endless "loading" after doing these steps? @Johan Commelin
My branch name is matrix_lz by the way.
image.png

[Alex Zhang]

Is there any looped import? I don't think I changed any import command.

[Bryan Gin-ge Chen]

Did you run leanproject get-cache? If you only use git you will not have the compiled version of mathlib corresponding to the commit, only the source files.

[Alex Zhang]

image.png
It reports this.
Perhaps I should delete or update the local one?

[Johan Commelin]

@Alex Zhang can you try opening VScode again? My hope/guess is that the problem will be gone.

[Bryan Gin-ge Chen]

If you hit control+shift+P and search for "restart Lean", the orange bars should go away quickly.

[Alex Zhang]

Indeed! Thanks a lot to Johan and Bryan!!