Is Mathlib project creation from VS Code broken?

Stream: new members

[Louis Cabarion]

Using VS Code 1.100.2 with leanprover.lean4 extension 0.0.205 (last released 2025-04-30).

To reproduce:

% code
  Command-Shift-P
  Lean 4: Create Project Using Mathlib...
  Choose "Create project folder" after choosing a project name
…
lake +leanprover-community/mathlib4:lean-toolchain update
✔ [13/13] Built cache
uncaught exception: Failed to run Git to determine project repository (exit code: 2).
Ensure Git is installed and the `origin` remote points to the project's GitHub repository.
Stdout:

Stderr:error: No such remote 'origin'
error: mathlib: failed to fetch cache
=> Operation failed. Exit code: 1.

[Louis Cabarion]

Reproducing from the command-line:

% cd /tmp && lake new test-project math && cd test-project && lake exe cache get
…
info: mathlib: running post-update hooks
uncaught exception: Failed to run Git to determine project repository (exit code: 2).
Ensure Git is installed and the `origin` remote points to the project's GitHub repository.
Stdout:

Stderr:error: No such remote 'origin'

error: mathlib: failed to fetch cache

[Alexander Heckett]

Seems to be the same issue that came up in this thread earlier today: #mathlib4 > `lake update` now slowly tries to download repository cache. There's a proposed fix on GitHub.

[Louis Cabarion]

I'm not sure how to work around this problem while waiting for the fix to be merged into Mathlib.

[Jeremy Avigad]

FWIW, I am having the same problem.

[Eric Wieser]

@Mac Malone

[Mac Malone]

Discussed over in #mathlib4. Fix is at mathlib4#25211.

[Mac Malone]

If you need to fetch the cache, the following can be used as a workaround until the fix is merged:

$ lake exe cache --repo=leanprover-community/mathlib4 get

[Alexander Heckett]

I'm actually still getting the error when I try that command. EDIT: ...apparently running it twice works??

[Alexander Heckett]

Okay, the actual key step seems to be to run lake update before lake exe cache --repo=leanprover-community/mathlib4 get.

[Louis Cabarion]

Isak Colboubrani said:

Reproducing from the command-line:

% cd /tmp && lake new test-project math && cd test-project && lake exe cache get
…
info: mathlib: running post-update hooks
uncaught exception: Failed to run Git to determine project repository (exit code: 2).
…

As of today, this works:

% cd /tmp && lake new test-project math && cd test-project && lake exe cache get
…
info: mathlib: running post-update hooks
…
Completed successfully!
% echo $?
0
%

Thanks @Mac Malone!