VSCode reclones deps before I have a chance to update

Stream: general

[Bolton Bailey]

I have noticed the following pattern in my use of how the VSCode lean extension deals with the lake dependencies of my projects as I switch between branches. I haven't been paying close attention to it until recently, but it goes something like this:

1. I on the main branch of a project, or a branch of the project with the same toolchain as main.
2. I switch to an old branch with an older lean-toolchain
3. I open a lean file

4. VSCode somehow immediately realizes that the old toolchain I am now on doesn't match the contents of .lake. It sends a message like "info: plausible: URL has changed; deleting '/Users/boltonbailey/mathlib-contribution/mathlib4/.lake/packages/plausible' and cloning again
   info: plausible: cloning" for all my dependencies

5. I now have to wait for all my dependencies to be recloned, when often I would be happy to merge main into this feature branch and use the dependencies I already have.

Is there a way I could stop this from happening? I guess it is not really an option for me to just not open any lean file before merging because I have the "Restore Git Branch Tabs" extension and that is just way too convenient to give up when I am working on PRs and need to reopen a bunch of specific files for each branch.

[Ching-Tsun Chou]

I just use different cslib clones for the different branches I work on.

[Bolton Bailey]

I guess there are a few weird things at play here:

1. Why is it saying the URL for plausible has changed? Has it really moved to a different github repo in the 2 months since this PR was made?
2. I guess if it didn't think the URL had changed it could just pull/checkout from the repo rather than clone it from scratch, so maybe that is the key issue here.
3. OTOH it would be nice if the little blue button that says "restart file" would simply change to say "refresh .lake" when that is what is necessary to restart the file, so that I can take the chance to update the toolchain first.

[Bolton Bailey]

Indeed, the docstring of the function giving this error reads

/--
Update the Git repository from `url` in `repo` to `rev?`.
If `repo` is already from `url`, just checkout the new revision.
Otherwise, delete the local repository and clone a fresh copy from `url`.
-/
def updateGitRepo ...

[Bolton Bailey]

I am a bit concerned that this is manifesting because the lakefile says the git repo is "https://github.com/leanprover-community/plausible" but git remote get-url origin, the command used by docs#updateGitRepo to compare against, gives git@github.com:leanprover-community/plausible

[Bolton Bailey]

Aha! Perhaps the culprit is that I have configured my git to use

[url "git@github.com:"]
        insteadOf = https://github.com/

[Bolton Bailey]

Indeed, changing this changes the error. But I understand that SSH is more secure than https, so I am a bit sad to remove it.

[Bolton Bailey]

Still seems to be an issue though that I am clicking "Restart file" in a branch with toolchain 4.27 and it is running /Users/boltonbailey/.elan/toolchains/leanprover--lean4---v4.29.0-rc1/bin/lake setup-file.

[Bolton Bailey]

I believe this insteadOf trick was something a previous employer asked me to do to improve security, and when I google for why https was not show up in my remote name, google suggested it might be because that exact snippet could be in my config file, so perhaps this is some kind of standard security practice?

@Mac Malone have you heard of anything like this before? Is allowing this URL/insteadOf switching something worth filing an issue over or trying to get lake to support?

[Floris van Doorn]

Ching-Tsun Chou said:

I just use different cslib clones for the different branches I work on.

With git worktree you can have a single clone but multiple worktrees. You can create a new worktree with e.g. git worktree add ../cslib_clone. They all have their own separate .lake folder, they just share their git history.
(I have 6 worktrees of Mathlib on my laptop)

[Ching-Tsun Chou]

Thanks for the tip about git worktree! I'll look into using it for new PRs. But the space saving from sharing .git is probably negligible in the case of cslib, because >99.7% of the space in a cslib repo is used by .lake anyway.

[Mac Malone]

Bolton Bailey said:

Mac Malone have you heard of anything like this before? Is allowing this URL/insteadOf switching something worth filing an issue over or trying to get lake to support?

This replacement issue has appeared before. However, it is not something Lake can feasibly support. Lake needs to ensure the URL provided in the lakefile matches that of the git remote.