error with leanproject new

Stream: general

[Floris van Doorn]

Leanproject is great. I tried to use leanproject new for the first time today, and I got this error:

$ git clone git@github.com:fpvandoorn/group-representations.git
[...]
$ cd group-representations/
$ leanproject new
Move existing .lean files into the 'src' folder.
> mkdir src
configuring group-representations 0.1
Adding mathlib
Looking for local mathlib oleans
Looking for remote mathlib oleans
Trying to download https://oleanstorage.azureedge.net/mathlib/66cc29804344de86894d440d10167bb68c2cca83.tar.gz\xa0to C:\Users\Floris\.mathlib\66cc29804344de86894d440d10167bb68c2cca83.tar.gz
100%|##########| 25.5M/25.5M [00:03<00:00, 8.07MiB/s]
Found mathlib oleans at https://oleanstorage.azureedge.net/mathlib/
Cmd('git') failed due to: exit code(128)
  cmdline: git checkout -b master
  stderr: 'fatal: A branch named 'master' already exists.'

Is this not the intended use of leanproject new?

[Floris van Doorn]

It seemed to have done everything that I wanted it to do, so no complaints there.

[Johan Commelin]

@Floris van Doorn leanproject new creates a new lean repo. What kind of repo did you clone? Was it empty?

[Johan Commelin]

Otherwise you should just use leanproject up to move you mathlib dependency to the latest version and download mathlib oleans at the same time. (There is also leanproject get-mathlib-cache)

[Patrick Massot]

No, getting an existing project is not the intended use of leanproject new. The command you wanted to type was:

leanproject get fpvandoorn/group-representations

[Patrick Massot]

I just checked and there is no problem getting your project.

[Floris van Doorn]

Ah cool! So even the cloning itself is done by leanproject :thumbs_up:

[Johan Commelin]

You should try leanproject dishwasher... it's really amazing what happens. I barely recognised my kitchen afterwards.

[Reid Barton]

Hmm, maybe I should check out this leanproject thing after all...

[Floris van Doorn]

feature request: leanproject grade-student-homework