cache not working

Stream: mathlib4

[Jakob von Raumer]

This has probably been asked before, but I can't really find my mistake. The cached build for #26490 isn't downloading for me, this is my remotes:

➜  mathlib4 git:(Truncated.inital_inclusion) ✗ git remote -v
javra   git@github.com:javra/mathlib4.git (fetch)
javra   git@github.com:javra/mathlib4.git (push)
origin  git@github.com:javra/mathlib4.git (fetch)
origin  git@github.com:javra/mathlib4.git (push)
upstream    https://github.com/leanprover-community/mathlib4.git (fetch)
upstream    https://github.com/leanprover-community/mathlib4.git (push)

Shouldn't this be working?

[Kenny Lau]

What is the error message?

[Kevin Buzzard]

I tried getting cache today for a PR and I had to run lake exe cache get twice shrug

[Jakob von Raumer]

@Kenny Lau I'm just getting a

Downloaded: 0 file(s) [attempted 279/279 = 100%] (0% success)

[Kevin Buzzard]

yeah I got that the second time and then everything worked for me

[Kevin Buzzard]

OK so I'm having difficulty reviewing #25872 . My local set-up looks like this:

buzzard@IC-HWDXTW69VR Mathlib % git remote --v
origin  git@github.com:kbuzzard/mathlib4.git (fetch)
origin  git@github.com:kbuzzard/mathlib4.git (push)
upstream    git@github.com:leanprover-community/mathlib4.git (fetch)
upstream    git@github.com:leanprover-community/mathlib4.git (push)

and I typed

buzzard@IC-HWDXTW69VR Mathlib % gh pr checkout 25872
Switched to branch 'arlcohlesrefactor'
buzzard@IC-HWDXTW69VR Mathlib % lake exe cache get

and I get

Current branch: arlcohlesrefactor
uncaught exception: Failed to run Git to determine Mathlib's repository from git@github.com:101damnations/mathlib4.git remote (exit code: 2).
Ensure Git is installed and the 'git@github.com:101damnations/mathlib4.git' remote points to its GitHub repository.
Stdout:

Stderr:
error: No such remote 'git@github.com:101damnations/mathlib4.git'

and now I'm completely stuck. I tried rm -rf .lake and I get the same error. Can someone else reproduce? Have I got things set up wrong? Yesterday I typed gh repo set-default git@github.com:leanprover-community/mathlib4.git and I don't really know what I'm doing but it seemed to work for the PR I reviewed yesterday...

NB this fork https://github.com/101damnations/mathlib4 does exist.

[Kevin Buzzard]

aargh having resorted to building mathlib from scratch so I could review the PR before I meet the author tomorrow, I have now moved onto #25873 with gh pr checkout 25873 and I have exactly the same problem. I've tried on two machines (one mac one ubuntu) and it's the same problem in both. Can anyone else reproduce?

[Sébastien Gouëzel]

I can reproduce:

gh pr checkout 25872
lake exe cache get

is broken from my fork.

This is due to #26419: on https://github.com/leanprover-community/mathlib4/blob/308445d7985027f538e281e18df29ca16ede2ba3/Cache/Requests.lean#L179, what I get as an output is https://github.com/101damnations/mathlib4.git, so already an URL, and then the line

let repo ← getRepoFromRemote mathlibDepPath remoteName

is confused because it is not expecting an URL, but a repo name. One could use extractRepoFromUrl instead here. There are many ways to fix this, I'm sure @Kim Morrison would know how to do this cleanly.

[Kevin Buzzard]

Is there a workaround? I have also had to compile from source to review this second PR (2000 files)

[Sébastien Gouëzel]

Yes. Once you have done gh pr checkout ...., you can copy the file Cache/Requests.lean from the branch https://github.com/leanprover-community/mathlib4/tree/SG_dirty. Then lake exe cache get should work.

[Sébastien Gouëzel]

Or (simpler, but you have to identify the origin of the branch yourself)

 lake exe cache --repo="101damnations/mathlib4" get

[Kevin Buzzard]

Thanks so much! I can confirm that you just saved me 30 minutes and a lot of laptop battery.

[Jakob von Raumer]

Thanks, that also solved it for me!

[Jakob von Raumer]

But I don't get whether this should actually be working without specifying the repo, if I named my own one origin?

[Sébastien Gouëzel]

This should be working, but cache is partly broken for now. Hopefully, the above workaround won't be needed in a few days.

[Matthew Ballard]

Sébastien Gouëzel said:

I can reproduce:

gh pr checkout 25872
lake exe cache get

is broken from my fork.

Can a non-maintainer invoke these commands from their fork?

[Joscha Mennicken]

These exact commands result in this error message on my fork (like already seen above):

Current branch: arlcohlesrefactor
uncaught exception: Failed to run Git to determine Mathlib's repository from git@github.com:101damnations/mathlib4.git remote (exit code: 2).
Ensure Git is installed and the 'git@github.com:101damnations/mathlib4.git' remote points to its GitHub repository.
Stdout:

Stderr:
error: No such remote 'git@github.com:101damnations/mathlib4.git'

[Matthew Ballard]

Thanks.

[Matthew Ballard]

#26551 should minimally affect the existing logic while handling the url remotes. Note that the logic is unchanged in the current PR. There is an additional print statement to help with testing.

[Yakov Pechersky]

I tried this after gh repo set-default leanprover-community/mathlib4; gh pr checkout 26538. I cherry-picked the #26551 changes onto my checked-out branch.
It didn't work, I got:

$ lake exe cache get
Current branch: val_extension_instances
Is git@github.com:mariainesdff/mathlib4.git a remote URL? true
uncaught exception: Failed to run Git to determine Mathlib's repository from git@github.com:mariainesdff/mathlib4.git remote (exit code: 2).
Ensure Git is installed and the 'git@github.com:mariainesdff/mathlib4.git' remote points to its GitHub repository.
Stdout:

Stderr:
error: No such remote 'git@github.com:mariainesdff/mathlib4.git'

[Matthew Ballard]

#26551 didn't deploy the logic itself. It just added the new logic and only printed the outputs to inspect the results in CI. The actual logic is deployed now.

[Matthew Ballard]

That didn't last long. Since we split the logic for determining the repo between the workflow and cache, there is now some mismatch in conventions which needs to be accounted for.