lake exe cache get on downstream projects

Stream: mathlib4

[Aaron Liu]

I am on my fork of the combinatorial games repo. I want to get the mathlib cache so I don't have to build mathlib myself.
I ran lake exe cache get and it printed the error

info: mathlib: checking out revision '3675c9af6ec591616ef1e99f6046fd8e52d133eb'
error: external command 'git' exited with code 128

I ran lake clean and it printed the error

error: external command 'git' exited with code 128

I deleted the .lake file and ran lake exe cache get again and got

info: mathlib: URL has changed; you might need to delete 'C:\Users\aaron\lean\combinatorial-games\.lake/packages\mathlib' manually
info: mathlib: checking out revision '3675c9af6ec591616ef1e99f6046fd8e52d133eb'
error: external command 'git' exited with code 128

I ran lake clean again and got

info: mathlib: URL has changed; you might need to delete 'C:\Users\aaron\lean\combinatorial-games\.lake/packages\mathlib' manually
info: mathlib: checking out revision '3675c9af6ec591616ef1e99f6046fd8e52d133eb'
error: external command 'git' exited with code 128

At this point I'm really not sure what to do so I go the my local copy of mathlib and checkout 3675c9af6ec591616ef1e99f6046fd8e52d133eb so I can run lake exe cache get there, and it works. I then go back to combinatorial games and do lake exe cache get again and get

info: mathlib: cloning https://github.com/leanprover-community/mathlib4
info: mathlib: checking out revision '3675c9af6ec591616ef1e99f6046fd8e52d133eb'
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision 'fde3fc21dd68a10791dea22b6f5b53c5a5a5962d'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision '6c62474116f525d2814f0157bb468bf3a4f9f120'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision '856a8cb8908af109aac3ce13e2b4f866f3d75199'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '2d6d124aedc3023506a67e50bfd5582384d6bd17'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision 'a1b5d59f433c6ec2b318192bd910c257a3c62be8'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision '56047303fce0d07dcae7e3e91b17eef67d11f6f4'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '3613427d66262c4e25e19b40a6a49242e94ba072'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '1604206fcd0462da9a241beeac0e2df471647435'
Current branch: HEAD
Warning: Some Mathlib ecosystem tools assume that the git remote for `leanprover-community/mathlib4` is named `upstream`. You have named it `origin` instead. We recommend changing the name to `upstream`. Moreover, `origin` should point to your own fork of the mathlib4 repository. You can set this up with `git remote add upstream https://github.com/leanprover-community/mathlib4.git`.
`git for-each-ref --contains 3675c9af6ec591616ef1e99f6046fd8e52d133eb refs/remotes/origin/pr/* --format=%(refname)` returned:
         with exit code 0 and stderr: .
`git for-each-ref --contains 3675c9af6ec591616ef1e99f6046fd8e52d133eb refs/remotes/origin/pr/* --format="%(refname)"` returned:
         with exit code 0 and stderr: .
Is origin a remote URL? false
Extracted repo from remote URL:
Using cache from origin: leanprover-community/mathlib4
No files to download
Decompressing 6895 file(s)
Unpacked in 131015 ms
Completed successfully!

In the end I didn't have to build mathlib myself but that really could have been easier. What have I been doing wrong?

[Matthew Ballard]

What does git remote -v print in your state?

[Aaron Liu]

origin  https://github.com/plp127/combinatorial-games.git (fetch)
origin  https://github.com/plp127/combinatorial-games.git (push)
upstream        https://github.com/vihdzp/combinatorial-games.git (fetch)
upstream        https://github.com/vihdzp/combinatorial-games.git (push)

[Aaron Liu]

Seems very normal

[Damiano Testa]

Does this mean that you are not using ssh?

[Aaron Liu]

I don't know why I should use ssh

[Aaron Liu]

It works fine on my copy of mathlib

[Damiano Testa]

Ok, whenever something changes my remotes to https, I get in a confusing state and I only get back to what feels normal by going back to ssh.

[Aaron Liu]

I don't know how to do that

[Damiano Testa]

Anyway, I don't know if this should affect anything here, I was just surprised.

[Matthew Ballard]

Current branch: HEAD this is not handled at all at the moment

[Aaron Liu]

What does that mean?

[Matthew Ballard]

Ok, it really means that there should better checks to handle detached head. But the current workaround is to use lake exe cache --repo=owner/repoName get

[Damiano Testa]

(In case you want to set up ssh, this is probably what you should do:

git remote set-url origin git@github.com:plp127/combinatorial-games.git

and I imagine similarly for upstream. But, if it worked for you before, maybe keep your original setup!)

[Aaron Liu]

Matthew Ballard said:

Ok, it really means that there should better checks to handle detached head. But the current workaround is to use lake exe cache --repo=owner/repoName get

I don't think I was on detached head though?

[Matthew Ballard]

Hmm. Give me a short list of steps to get into this state and I will look into it.

Also, the behavior would depend on the version of cache in the project.

[Joseph Tooby-Smith]

I'm having a similar issue to Aaron here, I cloned a new copy of nomeata/loogle, and every time I run lake update I get

info: mathlib: cloning https://github.com/leanprover-community/mathlib4
error: external command 'git' exited with code 128

I've also had similar problems with PhysLean - everything appears really slow and temperamental all of a sudden, and it seems to be independent of the wifi I'm on.

[Joseph Tooby-Smith]

(I actually kept running lake update and it finally worked)