Lake exe cache get with other git remote name?

Stream: mathlib4

[Robin Carlier]

Recently, lake exe cache get started complaining because in my local mathlib git directory, the upstream mathlib4 remote was not named origin. This is a sane default for most use cases, but is it mandatory? Is there an environment variable I can set to override this?

[Ruben Van de Velde]

@Mac Malone , is this something you know about?

[Robin Carlier]

More precisely, I get

$ lake exe cache get
uncaught exception: Failed to run Git to determine Mathlib's repository (exit code: 2).
Ensure Git is installed and Mathlib's `origin` remote points to its GitHub repository.
Stdout:

Stderr:
error: No such remote 'origin'

[Robin Carlier]

(This only happens in my mathlib4 local worktrees, downstream projects are of course fine.)

[Eric Wieser]

There is a --repo flag I think

[Robin Carlier]

Both lake exe cache get --repo and lake exe cache --repo get seem to fail, so I don’t think there is.

[Robin Carlier]

Culprit is #25211 I think

[Robin Carlier]

Cache.Requests.getRemoteRepo hardcodes origin and does not seem to allow anything else through an option. I’ll make a PR introducing an environment variable.

[Eric Wieser]

That function is only called if the flag is not set

[Robin Carlier]

$ lake exe cache get --repo=https://github.com/leanprover-community/mathlib4
Invalid argument: non-existing path --repo=https:/github.com/leanprover-community/mathlib4

What am I doing wrong here? (Also of course, lake exe cache get --repo=. does not work).

[Robin Carlier]

(also lake exe cache get --repo "..." seems like invalid syntax. This is not exactly standard command line arguments parsing here. my bad, it in fact is, I thought I knew some CLI that allowed --arg value.)

[Robin Carlier]

(I stand by my proposal to make this configurable by an environment variable: this would save typing --repo=... at every call).

[Eric Wieser]

I think lake exe cache --repo=https://github.com/leanprover-community/mathlib4 get

[Robin Carlier]

Documenting this flag somewhere would be nice. It’s not mentionned in lake exe cache --help, and both lake exe cache get --help and lake exe cache --help get are invalid.

[Robin Carlier]

I confirmed that it works, thanks!

[Kim Morrison]

(It's a bit unfortunate that lake exe cache requires the --repo flag before get. If someone wants to have cache use lean4-cli this could easily be fixed.)

[Eric Wieser]

(but how will I get the cache for my file called --repo? :upside_down:)

[Mac Malone]

Eric Wieser said:

I think lake exe cache --repo=https://github.com/leanprover-community/mathlib4 get

It's lake exe cache --repo=leanprover-community/mathlib4 get.